Visible to the public Inductive types in homotopy type theoryConflict Detection Enabled

TitleInductive types in homotopy type theory
Publication TypeConference Proceedings
Year of Publication2012
AuthorsSteve Awodey, Nicola Gambino, Kristina Sojakova
Conference NameLICS '12 Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science
Date Published06/2012
PublisherIEEE Computer Society Washington, DC, USA ©2012
Conference LocationNew Orleans, LA
KeywordsCMU, homotopy theory, initial algebras., Type theory

Homotopy type theory is an interpretation of Martin-L"of'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.

Citation Keynode-30139

Other available formats:

Awodey_Inductive_Types.pdfPDF document246.99 KBDownloadPreview