Inductive types in homotopy type theory

DOI10.1109/LICS.2012.21MaRDI QIDQ2986785zbMATH OpenOpenAlexWikidataFDO

Authors Nicola Gambino, Kristina Sojakova, Steve Awodey

Publication date 16 May 2017

Published in 2012 27th Annual IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

homotopy theoryinitial algebrastype theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10) Topological categories, foundations of homotopy theory (55U40)

Abstract: Homotopy type theory is an interpretation of Martin-L"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.

Recommendations

• Homotopy-initial algebras in type theory
• Higher inductive types as homotopy-initial algebras
• Non-wellfounded trees in homotopy type theory
• Homotopy Type Theory
• On higher inductive types in cubical type theory

Cited in

(31)

• A construction method for induced types and its application to G₂
• Homotopy type theory in Lean
• The construction of set-truncated higher inductive types
• What inductive explanations could not be
• Constructing inductive-inductive types in cubical type theory
• From signatures to monads in \textsf{UniMath}
• Some Wellfounded Trees in UniMath
• Homotopical patch theory
• Higher inductive types as homotopy-initial algebras
• Type theory in type theory using quotient inductive types
• Partiality, Revisited
• scientific article; zbMATH DE number 5994829 (Why is no real title available?)
• Homotopy-initial algebras in type theory
• Data types with symmetries and polynomial functors over groupoids
• Mathesis Universalis and Homotopy Type Theory
• Inductive Type Schemas as Functors
• scientific article; zbMATH DE number 2061701 (Why is no real title available?)
• scientific article; zbMATH DE number 2182487 (Why is no real title available?)
• Constructing higher inductive types as groupoid quotients
• The integers as a higher inductive type
• Sequential colimits in homotopy type theory
• Injective types in univalent mathematics
• Bar induction is compatible with constructive type theory
• Non-wellfounded trees in homotopy type theory
• Homotopy limits in type theory
• Topological quantum gates in homotopy type theory
• Path spaces of higher inductive types in homotopy type theory
• Conservativity of type theory over higher-order arithmetic
• Universal algebra in UniMath
• A unifying logical foundation for initial algebra semantics and induction
• A 2-categorical approach to the semantics of dependent type theory with computation axioms

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Inductive types in homotopy type theory

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