Semantics of higher inductive types

DOI10.1017/S030500411900015XzbMath1470.18007arXiv1705.07088WikidataQ127661505 ScholiaQ127661505MaRDI QIDQ4958656

Peter LeFanu Lumsdaine, Michael Shulman

Publication date: 14 September 2021

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

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

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)

Related Items (15)

Modalities in homotopy type theory ⋮ Localization in Homotopy Type Theory ⋮ The construction of set-truncated higher inductive types ⋮ Unnamed Item ⋮ A class of higher inductive types in Zermelo‐Fraenkel set theory ⋮ The Hurewicz theorem in homotopy type theory ⋮ Univalent categories of modules ⋮ The long exact sequence of homotopy n-groups ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Type-theoretic approaches to ordinals ⋮ Towards a homotopy domain theory ⋮ Characterizations of modalities and lex modalities ⋮ Unnamed Item ⋮ Construction of the circle in \textit{UniMath}

Uses Software

• HoTT
• GitHub
• MathOverflow

Cites Work

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

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