Inductive Types in Homotopy Type Theory

DOI10.1109/LICS.2012.21zbMath1364.03014arXiv1201.3898OpenAlexW1978777279WikidataQ61834693 ScholiaQ61834693MaRDI QIDQ2986785

Nicola Gambino, Kristina Sojakova, Steven 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

type theoryhomotopy theoryinitial algebras

Mathematics Subject Classification ID

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

Related Items

The construction of set-truncated higher inductive types, Data Types with Symmetries and Polynomial Functors over Groupoids, Unnamed Item, What inductive explanations could not be, Partiality, Revisited, Mathesis Universalis and Homotopy Type Theory, Some Wellfounded Trees in UniMath, From signatures to monads in \textsf{UniMath}

Uses Software

• Coq