Homotopy-Initial Algebras in Type Theory

DOI10.1145/3006383zbMath1426.03016arXiv1504.05531OpenAlexW2963024429WikidataQ59890116 ScholiaQ59890116MaRDI QIDQ3177878

Kristina Sojakova, Nicola Gambino, Steven Awodey

Publication date: 2 August 2018

Published in: Journal of the ACM (Search for Journal in Brave)

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

zbMATH Keywords

recursioninductionhomotopy type theoryinitial algebraW-types

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Theories (e.g., algebraic theories), structure, and semantics (18C10) Type theory (03B38)

Related Items (4)

Every Elementary Higher Topos has a Natural Number Object ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Semantics of higher inductive types ⋮ W-types in setoids

This page was built for publication: Homotopy-Initial Algebras in Type Theory