Higher Inductive Types as Homotopy-Initial Algebras

DOI10.1145/2676726.2676983zbMath1345.03017DBLPconf/popl/Sojakova15arXiv1402.0761OpenAlexW2052183597WikidataQ56589041 ScholiaQ56589041MaRDI QIDQ2819787

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)

Related Items (12)

Finitary higher inductive types in the groupoid model ⋮ The construction of set-truncated higher inductive types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A class of higher inductive types in Zermelo‐Fraenkel set theory ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ What inductive explanations could not be ⋮ Partiality, Revisited ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Unnamed Item ⋮ Construction of the circle in \textit{UniMath}

Uses Software

• Coq

This page was built for publication: Higher Inductive Types as Homotopy-Initial Algebras