All Outputs (2)

Naive Type Theory (2019)
Book Chapter
Altenkirch, T. (2019). Naive Type Theory. In S. Centrone, D. Kant, & D. Sarikaya (Eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts (101-136). Springer

We introduce Type Theory, including Homotopy Type Theory, as an alternative to set theory as a foundation of Mathematics emphasising the intuitive and naive understanding of its concepts.

Quotient inductive-inductive types (2018)
Book Chapter
Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Forsberg, F. (2018). Quotient inductive-inductive types. In C. Baier, & U. Dal Lago (Eds.), FoSSaCS 2018: Foundations of Software Science and Computation Structures (293-310). Cham: Springer Publishing Company. https://doi.org/10.1007/978-3-319-89366-2_16

Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the sense of H... Read More about Quotient inductive-inductive types.