12

[1201.3898] Inductive types in homotopy type theory

 4 years ago
source link: https://arxiv.org/abs/1201.3898
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

[Submitted on 18 Jan 2012 (v1), last revised 2 May 2012 (this version, v2)]

Inductive types in homotopy type theory

Download PDF

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.

Comments: 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 Subjects: Logic (math.LO); Logic in Computer Science (cs.LO) MSC classes: 03B15, 03B70, 03F50 Cite as: arXiv:1201.3898 [math.LO]   (or arXiv:1201.3898v2 [math.LO] for this version)

report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK