All Outputs (2)

Some constructions on ?-groupoids (2014)
Conference Proceeding
Altenkirch, T., Li, N., & Ond?ej, R. (2014). Some constructions on ?-groupoids. . https://doi.org/10.1145/2631172.2631176

Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the construc- tive semantics of Homotopy Type Theory [10]. Following up on our previous formalisation [3] and Brunerie’s notes [5], we present a... 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.