Professor THORSTEN ALTENKIRCH's Outputs (2)

Some constructions on ω-groupoids (2014)
Presentation / Conference Contribution
Altenkirch, T., Li, N., & Ondřej, R. (2014, July). Some constructions on ω-groupoids. Presented at LFMTP '14: Theory and Practice, Vienna, Austria

Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the constructive semantics of Homotopy Type Theory [13]. Following up on our previous formalisation [3] and Brunerie's notes [6], we present a ne... Read More about Some constructions on ω-groupoids.

Relative monads formalised (2014)
Journal Article
Altenkirch, T., Chapman, J., & Uustalu, T. (2014). Relative monads formalised. Journal of Formalized Reasoning, 7(1), https://doi.org/10.6092/issn.1972-5787/4389

Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed... Read More about Relative monads formalised.