Inductive types in homotopy type theory

Steve Awodey; Nicola Gambino; Kristina Sojakova

doi:10.1109/LICS.2012.21

Inductive types in homotopy type theory

Steve Awodey, Nicola Gambino, Kristina Sojakova

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

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. © 2012 IEEE.

Original language	English
Title of host publication	Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012
Pages	95-104
DOIs	https://doi.org/10.1109/LICS.2012.21
Publication status	Published - 2012
Externally published	Yes
Event	2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012 - , Croatia Duration: 25 Jun 2012 → 28 Jun 2012

Conference

Conference	2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012
Country/Territory	Croatia
Period	25/06/12 → 28/06/12

Access to Document

10.1109/LICS.2012.21

Persistent URL (handle)

Persistent link

Cite this

@inproceedings{553a1af456964809b7ca9ee8f2ed0780,

title = "Inductive types in homotopy type theory",

abstract = "Homotopy type theory is an interpretation of Martin-L{\"o}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. {\textcopyright} 2012 IEEE.",

author = "Steve Awodey and Nicola Gambino and Kristina Sojakova",

year = "2012",

doi = "10.1109/LICS.2012.21",

language = "English",

pages = "95--104",

booktitle = "Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012",

note = "2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012 ; Conference date: 25-06-2012 Through 28-06-2012",

}

TY - GEN

T1 - Inductive types in homotopy type theory

AU - Awodey, Steve

AU - Gambino, Nicola

AU - Sojakova, Kristina

PY - 2012

Y1 - 2012

N2 - 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. © 2012 IEEE.

AB - 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. © 2012 IEEE.

UR - http://www.scopus.com/inward/record.url?scp=84867179352&partnerID=8YFLogxK

U2 - 10.1109/LICS.2012.21

DO - 10.1109/LICS.2012.21

M3 - Conference contribution

SP - 95

EP - 104

BT - Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012

T2 - 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012

Y2 - 25 June 2012 through 28 June 2012

ER -

Inductive types in homotopy type theory

Abstract

Conference

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this