Professor THORSTEN ALTENKIRCH's Outputs (2)

Martin Hofmann’s Contributions to Type Theory: Groupoids and Univalence (2021)
Journal Article
Altenkirch, T. (2021). Martin Hofmann’s Contributions to Type Theory: Groupoids and Univalence. Mathematical Structures in Computer Science, 31(9), 953-957. https://doi.org/10.1017/S0960129520000316

My goal is to give an accessible introduction to Martin’s work on the groupoid model and how it is related to the recent notion of univalence in Homotopy Type Theory while sharing some memories of Martin.

Constructing a universe for the setoid model (2021)
Presentation / Conference Contribution
Altenkirch, T., Boulier, S., Kaposi, A., Sattler, C., & Sestini, F. (2021, March). Constructing a universe for the setoid model. Presented at 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021), Online

The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent pr... Read More about Constructing a universe for the setoid model.