Semantics of higher inductive types
From MaRDI portal
Publication:4958656
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)
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 -category is presented by some model category to which our results apply.
Recommendations
Cites work
- scientific article; zbMATH DE number 3522182 (Why is no real title available?)
- scientific article; zbMATH DE number 1302059 (Why is no real title available?)
- scientific article; zbMATH DE number 226803 (Why is no real title available?)
- A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
- Algebraic model structures
- All uncountable cardinals can be singular
- Constructions with non-recursive higher inductive types
- Generalized algebraic theories and contextual categories
- Higher Topos Theory (AM-170)
- Homotopy theoretic models of identity types
- Homotopy type theory. Univalent foundations of mathematics
- Homotopy-initial algebras in type theory
- Modalities in homotopy type theory
- Monoidal algebraic model structures
- Natural weak factorization systems.
- On higher inductive types in cubical type theory
- Presheaves as models for homotopy types
- Quotient inductive-inductive types
- The homotopy theory of type theories
- The local universes model: an overlooked coherence construction for dependent type theories
- The univalence axiom for elegant Reedy presheaves
- Théories homotopiques dans les topos. (Homotopy theories in topoi)
- Type theory in type theory using quotient inductive types
- Understanding the small object argument
- Univalence for inverse EI diagrams
- Univalence for inverse diagrams and homotopy canonicity
- Univalence in locally Cartesian closed categories
- W-types in homotopy type theory
- Words, free algebras, and coequalizers
Cited in
(33)- Type-theoretic approaches to ordinals
- Impredicative encodings of (higher) inductive types
- Towards a homotopy domain theory
- Refining inductive types
- Non-accessible localizations
- Interpreting higher computations as types with totality
- Functions out of higher truncations
- Canonicity and homotopy canonicity for cubical type theory
- Characterizations of modalities and lex modalities
- On the ∞$\infty$‐topos semantics of homotopy type theory
- Univalent categories of modules
- The long exact sequence of homotopy n-groups
- A class of higher inductive types in Zermelo‐Fraenkel set theory
- scientific article; zbMATH DE number 7168146 (Why is no real title available?)
- Construction of the circle in \textit{UniMath}
- Quotients, inductive types, and quotient inductive types
- Semantically Inactive Multiplicatives and Words as Types
- Denotational cost semantics for functional languages with inductive types
- Constructions with non-recursive higher inductive types
- Quotient inductive-inductive types
- Constructing higher inductive types as groupoid quotients
- Constructing higher inductive types as groupoid quotients
- Modal fracture of higher groups
- The construction of set-truncated higher inductive types
- scientific article; zbMATH DE number 7756115 (Why is no real title available?)
- The Hurewicz theorem in homotopy type theory
- Localization in Homotopy Type Theory
- Sequential colimits in homotopy type theory
- Modalities in homotopy type theory
- Inductive Type Schemas as Functors
- A syntax for higher inductive-inductive types
- Homotopy-initial algebras in type theory
- scientific article; zbMATH DE number 1927416 (Why is no real title available?)
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)
