Inductive Types in Homotopy Type Theory
Inductive Types in Homotopy Type Theory
Homotopy type theory is an interpretation of Martin-Löf'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.
19 pages; v2: added references and acknowledgements, removed appendix with Coq README file, updated URL for Coq files. To appear in the proceedings of LICS 2012
- University of Manchester United Kingdom
- University of Manchester United Kingdom
- Institute for Advanced Study United States
- University of Palermo Italy
- Carnegie Mellon University United States
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Type theory, inductive types, homotopy-initial algebra, 18C10, Mathematics - Category Theory, 03B15, 03B70, 03F50, Mathematics - Logic, 68T15, Logic in Computer Science (cs.LO), 03B15, 03G30, FOS: Mathematics, Category Theory (math.CT), 55U40, Logic (math.LO)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Type theory, inductive types, homotopy-initial algebra, 18C10, Mathematics - Category Theory, 03B15, 03B70, 03F50, Mathematics - Logic, 68T15, Logic in Computer Science (cs.LO), 03B15, 03G30, FOS: Mathematics, Category Theory (math.CT), 55U40, Logic (math.LO)
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).21 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 10% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 10% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!