Higher inductive types as homotopy-initial algebras

DOI10.1145/2676726.2676983MaRDI QIDQ2819787zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Kristina Sojakova

Publication date 29 September 2016

Published in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

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

zbMATH Keywords

homotopy type theoryhigher inductive typehomotopy-initial algebraW-suspension

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Abstract: Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs. A crucial ingredient in this new system are higher inductive types, which allow us to represent objects such as spheres, tori, pushouts, and quotients. We investigate a variant of higher inductive types whose computational behavior is determined up to a higher path. We show that in this setting, higher inductive types are characterized by the universal property of being a homotopy-initial algebra.

Recommendations

• Homotopy-initial algebras in type theory
• Inductive types in homotopy type theory
• Higher Structures in Homotopy Type Theory
• Towards Constructive Homological Algebra in Type Theory
• Homotopy Type Theory: A synthetic approach to higher equalities
• The homotopy theory of type theories
• Pro-algebraic homotopy types
• Higher groups in homotopy type theory
• Homotopy type theory and Voevodsky's univalent foundations
• Homotopy type theory

Cited in

(21)

• What inductive explanations could not be
• Finitary higher inductive types in the groupoid model
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Mathesis Universalis and Homotopy Type Theory
• scientific article; zbMATH DE number 7168146 (Why is no real title available?)
• Semantics of higher inductive types
• Construction of the circle in \textit{UniMath}
• Quotients, inductive types, and quotient inductive types
• Inductive types in homotopy type theory
• Constructing higher inductive types as groupoid quotients
• Constructing higher inductive types as groupoid quotients
• The construction of set-truncated higher inductive types
• Partiality, Revisited
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Coslice colimits in homotopy type theory
• Sequential colimits in homotopy type theory
• A unifying logical foundation for initial algebra semantics and induction
• A syntax for higher inductive-inductive types
• Homotopy-initial algebras in type theory
• Non-wellfounded trees in homotopy type theory
• The compatibility of the minimalist foundation with homotopy type theory

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Higher inductive types as homotopy-initial algebras

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