Reference. Semantics of higher inductive types

Peter LeFanu Lumsdaine, Michael Shulman · Math. Proc. Camb. Phil. Soc. · 2019 · higher-inductive-types homotopy-type-theory · DOI · arXiv
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the “synthetic” development of homotopy theory within type theory, as well as in formalising ordinary set-level mathematics in type theory. In this paper, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters : a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has weakly stable typal initial algebras for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specialises to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed (∞, 1)-category is presented by some model category to which our results apply.

Cite
Cite as @lumsdaine-2019-semantics (helia, typst) · \cite{lumsdaine-2019-semantics} (LaTeX)
BibTeX
bibtex · 1 line
@article{lumsdaine-2019-semantics, title={Semantics of higher inductive types}, volume={169}, ISSN={1469-8064}, url={http://dx.doi.org/10.1017/s030500411900015x}, DOI={10.1017/s030500411900015x}, number={1}, journal={Mathematical Proceedings of the Cambridge Philosophical Society}, publisher={Cambridge University Press (CUP)}, author={LUMSDAINE, PETER LEFANU and SHULMAN, MICHAEL}, year={2019}, month=June, pages={159–208} }
hayagriva YAML (typst)
yaml · 16 lines
lumsdaine-2019-semantics:
  type: article
  title: Semantics of higher inductive types
  author:
  - Lumsdaine, Peter LeFanu
  - Shulman, Michael
  date: 2019-06
  page-range: 159-208
  serial-number:
    doi: 10.1017/s030500411900015x
  parent:
    type: periodical
    title: Mathematical Proceedings of the Cambridge Philosophical Society
    publisher: Cambridge University Press (CUP)
    issue: 1
    volume: 169
Download: lumsdaine-2019-semantics.bib · lumsdaine-2019-semantics.yml
Cited by (16)

Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda chen_etal_2026CPP · 2026
We present an intrinsic representation of type theory in the proof assistant Cubical Agda, inspired by Awodey’s natural models of type theory. The initial natural model is defined as quotient inductive-inductive-recursive types, leading us to a syntax accepted by Cubical Agda without using any transports, postulates, or custom rewrite rules. We formalise some meta-properties such as the standard model, normalisation by evaluation for typed terms, and strictification constructions. Since our formalisation is carried out using Cubical Agda’s native support for quotient inductive types, all our constructions compute at a reasonable speed. When we try to develop more sophisticated metatheory, however, the ‘transport hell’ problem reappears. Ultimately, it remains a considerable struggle to develop the metatheory of type theory using an intrinsic representation that lacks strict equations. The effort required is about the same whether or not the notion of natural model is used.
PDF · DOI · pldb

The Yoneda embedding in simplicial type theory gratzer-2025-theLICS · 2025
DOI · arXiv

The Univalence Principle ahrens-2021-theMem. AMS · 2025
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk’s completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai’s First-Order Logic with Dependent Sorts, but is expressed in Voevodsky’s Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.
DOI · arXiv

Directed univalence in simplicial homotopy type theory gratzer-2024-directedarXiv · 2024
Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics – where it allows for synthetic (higher) category theory – and programming languages – where it leads to a directed version of the structure identity principle. In this work, we construct the first types in simplicial type theory with non-trivial homomorphisms. We extend simplicial type theory with modalities and new reasoning principles to obtain triangulated type theory in order to construct the universe of discrete types 𝒮︀. We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that 𝒮︀ is directed univalent. The construction of 𝒮︀ is foundational for both of the aforementioned applications of simplicial type theory. We are able to define several crucial examples of categories and to recover important results from category theory. Using 𝒮︀, we are also able to define various types whose usage is guaranteed to be functorial. These provide the first complete examples of the proposed directed structure identity principle.
arXiv

Semantics of multimodal adjoint type theory shulman-2023-semanticsENTCS · 2023
We show that contrary to appearances, Multimodal Type Theory (MTT) over a 2-category M can be interpreted in any M-shaped diagram of categories having, and functors preserving, M-sized limits, without the need for extra left adjoints. This is achieved by a construction called “co-dextrification” that co-freely adds left adjoints to any such diagram, which can then be used to interpret the “context lock” functors of MTT. Furthermore, if any of the functors in the diagram have right adjoints, these can also be internalized in type theory as negative modalities in the style of FitchTT. We introduce the name Multimodal Adjoint Type Theory (MATT) for the resulting combined general modal type theory. In particular, we can interpret MATT in any finite diagram of toposes and geometric morphisms, with positive modalities for inverse image functors and negative modalities for direct image functors.
DOI · arXiv

Quotients, inductive types, and quotient inductive types fiore-2022-quotientsLMCS · 2022
This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.
DOI · arXiv

Quantitative Polynomial Functors nakov_quantitative_2022TYPES · 2022
We investigate containers and polynomial functors in Quantitative Type Theory, and give initial algebra semantics of inductive data types in the presence of linearity. We show that reasoning by induction is supported, and equivalent to initiality, also in the linear setting.
DOI

Construction of the Circle in UniMath bezem-2019-constructionJPAA · 2021
We show that the type Tℤ of ℤ-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky’s Univalence Axiom and propositional truncation, yielding a stand-alone construction of the circle not using higher inductive types.
DOI · arXiv

Internalizing representation independence with univalence angiuli-2021-internalizingPOPL · 2021
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky’s univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.
PDF · DOI · pldb

Modalities in homotopy type theory rijke-2020-modalitiesLMCS · 2020
Univalent homotopy type theory (HoTT) may be seen as a language for the category of ∞-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a “localization” higher inductive type. This produces in particular the (𝑛-connected, 𝑛-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
DOI · arXiv

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types VezzosiMortbergAbel2019ICFP · 2019
Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.
PDF · DOI · pldb

All (∞,1)-toposes have strict univalent universes shulman-2019-allarXiv · 2019
We prove the conjecture that any Grothendieck (∞,1)-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to (∞,1)-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.
arXiv

Cubical Syntax for Reflection-Free Extensional Equality sterling-2019-cubicalFSCD · 2019
We contribute XTT, a cubical reconstruction of Observational Type Theory [Altenkirch et al., 2007] which extends Martin-Löf’s intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel extension of the logical families or categorical gluing argument inspired by Coquand and Shulman [Coquand, 2018; Shulman, 2015]: every closed element of boolean type is derivably equal to either true or false.
DOI · arXiv

The RedPRL Proof Assistant (Invited Paper) angiuli-2018-theEPTCS · 2018
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths.
DOI · arXiv

Quotient Inductive-Inductive Types altenkirch_etal_2018FoSSaCS · 2018
Higher inductive types (HITs) in Homotopy Type Theory allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types, and allow to define types with non-trivial higher equality types, such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define types satisfying uniqueness of equality proofs, such as the Cauchy reals, the partiality monad, and the well-typed 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 a general theory of HITs, there is not yet a theoretical foundation for the combination of equality constructors and induction-induction, despite 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. We further derive a section induction principle, stating that every algebra morphism into the algebra in question has a section, which is close to the intuitively expected elimination rules.
DOI

Brouwer’s fixed-point theorem in real-cohesive homotopy type theory shulman-2017-brouwerMSCS · 2017
We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental ∞-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer’s fixed-point theorem.
DOI · arXiv
Cites 41 works (3 here)
With notes (3)

Modalities in homotopy type theory rijke-2020-modalitiesLMCS · 2020
Univalent homotopy type theory (HoTT) may be seen as a language for the category of ∞-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a “localization” higher inductive type. This produces in particular the (𝑛-connected, 𝑛-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
DOI · arXiv

Quotient Inductive-Inductive Types altenkirch_etal_2018FoSSaCS · 2018
Higher inductive types (HITs) in Homotopy Type Theory allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types, and allow to define types with non-trivial higher equality types, such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define types satisfying uniqueness of equality proofs, such as the Cauchy reals, the partiality monad, and the well-typed 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 a general theory of HITs, there is not yet a theoretical foundation for the combination of equality constructors and induction-induction, despite 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. We further derive a section induction principle, stating that every algebra morphism into the algebra in question has a section, which is close to the intuitively expected elimination rules.
DOI

Homotopy Type Theory: Univalent Foundations of Mathematics hottbookarXiv · 2013
Web · arXiv
External (38)
lumsdaine-2019-semantics reference entries/refs/lumsdaine-2019-semantics/lumsdaine-2019-semantics.hel