Professor THORSTEN ALTENKIRCH's Outputs (3)

Free Higher Groups in Homotopy Type Theory (2018)
Presentation / Conference Contribution
Kraus, N., & Altenkirch, T. (2018, July). Free Higher Groups in Homotopy Type Theory. Presented at LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford United Kingdom

© 2018 ACM. Given a type A in homotopy type theory (HoTT), we can define the free∞-group onA as the loop space of the suspension ofA+1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit : F(A),... Read More about Free Higher Groups in Homotopy Type Theory.

Quotient inductive-inductive types (2018)
Presentation / Conference Contribution
Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Forsberg, F. (2018, April). Quotient inductive-inductive types. Presented at 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece

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.

Towards a cubical type theory without an interval (2018)
Journal Article
Altenkirch, T., & Kaposi, A. (2018). Towards a cubical type theory without an interval. LIPIcs, 3:1-3:27. https://doi.org/10.4230/LIPIcs.TYPES.2015.3

Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof... Read More about Towards a cubical type theory without an interval.