Quotient inductive-inductive types

DOI10.1007/978-3-319-89366-2_16MaRDI QIDQ1652995zbMATH OpenOpenAlexDBLPWikidataFDO

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

Publication date 17 July 2018

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1612.02346

Mathematics Subject Classification ID

Type theory (03B38)

Abstract: 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 HoTT (i.e. do not satisfy uniqueness of equality proofs) such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define sets, such as the Cauchy reals, the partiality monad, and the internal, total syntax of type theory. In each of these examples we define several types that depend on each other mutually, i.e. they are inductive-inductive definitions. We call those HITs quotient inductive-inductive types (QIITs). Although there has been recent progress on the general theory of HITs, there isn't yet a theoretical foundation of the combination of equality constructors and induction-induction, despite having many interesting applications. In the present paper we present a first step towards a semantic definition of QIITs. In particular, we give an initial-algebra semantics and show that this is equivalent to the section induction principle, which justifies the intuitively expected elimination rules.

Recommendations

• A syntax for higher inductive-inductive types
• Large and infinitary quotient inductive-inductive types
• Quotients, inductive types, and quotient inductive types
• Semantics of higher inductive types
• Type theory in type theory using quotient inductive types

Cited in

(27)

• The construction of set-truncated higher inductive types
• Constructing infinitary quotient-inductive types
• Type-theoretic approaches to ordinals
• Type theory in type theory using quotient inductive types
• Partiality, Revisited
• Denotational semantics of recursive types in synthetic guarded domain theory
• scientific article; zbMATH DE number 1420793 (Why is no real title available?)
• Semantics of higher inductive types
• Constructing higher inductive types as groupoid quotients
• A syntax for higher inductive-inductive types
• Model structure on the universe of all types in interval type theory
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• Quotients, inductive types, and quotient inductive types
• The integers as a higher inductive type
• Large and infinitary quotient inductive-inductive types
• Constructing higher inductive types as groupoid quotients
• Signatures and induction principles for higher inductive-inductive types
• Quotients over Minimal Type Theory
• Big step normalisation for type theory
• For Finitary Induction-Induction, Induction is Enough
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Two-level type theory and applications
• Constructing initial algebras using inflationary iteration
• Impredicative encodings of inductive-inductive data in Cedille
• Towards constructive hybrid semantics
• A syntax for mutual inductive families
• The equivariant model structure on cartesian cubical sets

This page was built for publication: Quotient inductive-inductive types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1652995)