Higher inductive types as homotopy-initial algebras

DOI10.1145/2676726.2676983zbMATH Open1345.03017DBLPconf/popl/Sojakova15arXiv1402.0761OpenAlexW2052183597WikidataQ56589041 ScholiaQ56589041MaRDI QIDQ2819787FDOQ2819787

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)

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.

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

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

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)

Cited In (13)

• Title not available (Why is that?)
• What inductive explanations could not be
• Title not available (Why is that?)
• Finitary higher inductive types in the groupoid model
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Title not available (Why is that?)
• Mathesis Universalis and Homotopy Type Theory
• A Syntax for Higher Inductive-Inductive Types
• Construction of the circle in \textit{UniMath}
• The construction of set-truncated higher inductive types
• Partiality, Revisited
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• The compatibility of the minimalist foundation with homotopy type theory

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)