Inductive types in homotopy type theory

Steve Awodey, Nicola Gambino, Kristina Sojakova

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.
Original languageEnglish
Title of host publicationProceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25--28, 2012
Place of PublicationDubrovnik, Croatia
PublisherIEEE Computer Society
Number of pages10
ISBN (Print)9780769547695, 9781467322638
Publication statusPublished - Jun 2012

Publication series

NameAnnual Institute of Electrical and Electronics Engineers Symposium on Logic in Computer Science
PublisherInstitute of Electrical and Electronics Engineers
ISSN (Print)1043-6871


  • 03B15
  • 03G30
  • 18C10
  • 55U40
  • 68T15


Dive into the research topics of 'Inductive types in homotopy type theory'. Together they form a unique fingerprint.

Cite this