Quotient inductive-inductive types

Altenkirch, Thorsten; Capriotti, Paolo; Dijkstra, Gabe; Kraus, Nicolai; Nordvall Forsberg, Fredrik

doi:10.1007/978-3-319-89366-2_16

All Outputs (2)

Naive Type Theory (2019)
Book Chapter

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

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.