Semantics of higher inductive types

DOI10.1017/S030500411900015XzbMATH Open1470.18007arXiv1705.07088WikidataQ127661505 ScholiaQ127661505MaRDI QIDQ4958656FDOQ4958656

Authors: Peter Lefanu Lumsdaine, Michael Shulman 

Publication date: 14 September 2021

Published in: Mathematical Proceedings of the Cambridge Philosophical Society (Search for Journal in Brave)

Abstract: 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 formalizing ordinary set-level mathematics in type theory. In this article, 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 specializes 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 $(infty,1)$-category is presented by some model category to which our results apply.

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

Recommendations

• Higher inductive types as homotopy-initial algebras
• On higher inductive types in cubical type theory
• Homotopy-theoretic models of type theory
• Constructing higher inductive types as groupoid quotients
• Constructing higher inductive types as groupoid quotients

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Homotopical algebra, Quillen model categories, derivators (18N40) Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Cites Work

• Title not available (Why is that?)
• Higher Topos Theory (AM-170)
• Algebraic model structures
• Understanding the small object argument
• Univalence in locally Cartesian closed categories
• Generalized algebraic theories and contextual categories
• Homotopy theoretic models of identity types
• Title not available (Why is that?)
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Title not available (Why is that?)
• Natural weak factorization systems.
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Presheaves as models for homotopy types
• Théories homotopiques dans les topos. (Homotopy theories in topoi)
• W-types in homotopy type theory
• All uncountable cardinals can be singular
• The Local Universes Model
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves
• Monoidal algebraic model structures
• Words, free algebras, and coequalizers
• The homotopy theory of type theories
• Constructions with Non-Recursive Higher Inductive Types
• Quotient inductive-inductive types
• Univalence for inverse EI diagrams
• Modalities in homotopy type theory
• Type theory in type theory using quotient inductive types
• On Higher Inductive Types in Cubical Type Theory
• Homotopy-Initial Algebras in Type Theory

Cited In (24)

• Type-theoretic approaches to ordinals
• Title not available (Why is that?)
• Towards a homotopy domain theory
• Refining inductive types
• Non-accessible localizations
• Interpreting higher computations as types with totality
• Canonicity and homotopy canonicity for cubical type theory
• On the ∞$\infty$‐topos semantics of homotopy type theory
• Univalent categories of modules
• The long exact sequence of homotopy n-groups
• Characterizations of modalities and lex modalities
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Title not available (Why is that?)
• Construction of the circle in \textit{UniMath}
• Semantically Inactive Multiplicatives and Words as Types
• Denotational cost semantics for functional languages with inductive types
• Modal fracture of higher groups
• The construction of set-truncated higher inductive types
• Title not available (Why is that?)
• The Hurewicz theorem in homotopy type theory
• Localization in Homotopy Type Theory
• Modalities in homotopy type theory
• Inductive Type Schemas as Functors
• Title not available (Why is that?)

Uses Software

• HoTT
• MathOverflow
• GitHub

This page was built for publication: Semantics of higher inductive types

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