Homotopy-initial algebras in type theory

Steve Awodey, Nicola Gambino, Kristina Sojakova

Research output: Contribution to journalArticlepeer-review


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 that replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterizes the types that are equivalent to W-types as homotopy-initial algebras.
Original languageEnglish
Article number51
Pages (from-to)1-45
Number of pages45
JournalAssociation for Computing Machinery. Journal
Issue number6
Publication statusPublished - Feb 2017


  • Proof theory
  • Categorical semantics
  • Homotopy type theory
  • initial algebra
  • induction
  • recursion
  • W-types


Dive into the research topics of 'Homotopy-initial algebras in type theory'. Together they form a unique fingerprint.

Cite this