Homotopy-initial algebras in type theory

2015/04/21 by Awodey, Steve, Gambino, Nicola, Sojakova, Kristina
#Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1504.05531

Abstract

We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.

Related

• Higher Inductive Types as Homotopy-Initial Algebras
• Inductive types in homotopy type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Classifying Types
• Introduction to Homotopy Type Theory