Cartesian cubical computational type theory: Constructive reasoning with paths and equalities

Carlo Angiuli; Kuen Bang Hou; Robert Harper

doi:10.4230/LIPIcs.CSL.2018.6

Cartesian cubical computational type theory: Constructive reasoning with paths and equalities

Carlo Angiuli, Kuen Bang Hou, Robert Harper

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

16 Scopus citations

Abstract

We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.

Original language	English (US)
Title of host publication	Computer Science Logic 2018, CSL 2018
Editors	Dan R. Ghica, Achim Jung
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Print)	9783959770880
DOIs	https://doi.org/10.4230/LIPIcs.CSL.2018.6
State	Published - Aug 1 2018
Externally published	Yes
Event	27th Annual EACSL Conference Computer Science Logic, CSL 2018 - Birmingham, United Kingdom Duration: Sep 4 2018 → Sep 7 2018

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	119
ISSN (Print)	1868-8969

Conference

Conference	27th Annual EACSL Conference Computer Science Logic, CSL 2018
Country/Territory	United Kingdom
City	Birmingham
Period	9/4/18 → 9/7/18

Bibliographical note

Funding Information:
Funding This research was supported by the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053 and the National Science Foundation through grant DMS-1638352. Any opinions, findings and conclusions or recommendations expressed here are those of the authors and do not necessarily reflect the views of any sponsoring institution, the U.S. government or any other entity.

Funding Information:
This author thanks the Isaac Newton Institute for Mathematical Sciences for its support and hospitality during the program “Big Proof” when part of work on this paper was undertaken. The program was supported by EPSRC grant number EP/K032208/1.

Publisher Copyright:
© Carlo Angiuli, Kuen-Bang Hou, and Robert Harper; licensed under Creative Commons License CC-BY.

Keywords

Computational type theory
Cubical sets
Homotopy type theory
Two-level type theory

Access

10.4230/LIPIcs.CSL.2018.6

OpenUrl availability

Full text

Cite this

Angiuli, C., Hou, K. B., & Harper, R. (2018). Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. In D. R. Ghica, & A. Jung (Eds.), Computer Science Logic 2018, CSL 2018 Article 6 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 119). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2018.6

Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. / Angiuli, Carlo; Hou, Kuen Bang; Harper, Robert.
Computer Science Logic 2018, CSL 2018. ed. / Dan R. Ghica; Achim Jung. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018. 6 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 119).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Angiuli, C, Hou, KB & Harper, R 2018, Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. in DR Ghica & A Jung (eds), Computer Science Logic 2018, CSL 2018., 6, Leibniz International Proceedings in Informatics, LIPIcs, vol. 119, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 27th Annual EACSL Conference Computer Science Logic, CSL 2018, Birmingham, United Kingdom, 9/4/18. https://doi.org/10.4230/LIPIcs.CSL.2018.6

@inproceedings{2ee0512d1f014f69ac2bee8ee284be09,

title = "Cartesian cubical computational type theory: Constructive reasoning with paths and equalities",

abstract = "We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.",

keywords = "Computational type theory, Cubical sets, Homotopy type theory, Two-level type theory",

author = "Carlo Angiuli and Hou, {Kuen Bang} and Robert Harper",

note = "Funding Information: Funding This research was supported by the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053 and the National Science Foundation through grant DMS-1638352. Any opinions, findings and conclusions or recommendations expressed here are those of the authors and do not necessarily reflect the views of any sponsoring institution, the U.S. government or any other entity. Funding Information: This author thanks the Isaac Newton Institute for Mathematical Sciences for its support and hospitality during the program “Big Proof” when part of work on this paper was undertaken. The program was supported by EPSRC grant number EP/K032208/1. Publisher Copyright: {\textcopyright} Carlo Angiuli, Kuen-Bang Hou, and Robert Harper; licensed under Creative Commons License CC-BY.; 27th Annual EACSL Conference Computer Science Logic, CSL 2018 ; Conference date: 04-09-2018 Through 07-09-2018",

year = "2018",

month = aug,

day = "1",

doi = "10.4230/LIPIcs.CSL.2018.6",

language = "English (US)",

isbn = "9783959770880",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

editor = "Ghica, {Dan R.} and Achim Jung",

booktitle = "Computer Science Logic 2018, CSL 2018",

}

TY - GEN

T1 - Cartesian cubical computational type theory

T2 - 27th Annual EACSL Conference Computer Science Logic, CSL 2018

AU - Angiuli, Carlo

AU - Hou, Kuen Bang

AU - Harper, Robert

N1 - Funding Information: Funding This research was supported by the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053 and the National Science Foundation through grant DMS-1638352. Any opinions, findings and conclusions or recommendations expressed here are those of the authors and do not necessarily reflect the views of any sponsoring institution, the U.S. government or any other entity. Funding Information: This author thanks the Isaac Newton Institute for Mathematical Sciences for its support and hospitality during the program “Big Proof” when part of work on this paper was undertaken. The program was supported by EPSRC grant number EP/K032208/1. Publisher Copyright: © Carlo Angiuli, Kuen-Bang Hou, and Robert Harper; licensed under Creative Commons License CC-BY.

PY - 2018/8/1

Y1 - 2018/8/1

N2 - We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.

AB - We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.

KW - Computational type theory

KW - Cubical sets

KW - Homotopy type theory

KW - Two-level type theory

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

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

U2 - 10.4230/LIPIcs.CSL.2018.6

DO - 10.4230/LIPIcs.CSL.2018.6

M3 - Conference contribution

AN - SCOPUS:85053043370

SN - 9783959770880

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - Computer Science Logic 2018, CSL 2018

A2 - Ghica, Dan R.

A2 - Jung, Achim

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Y2 - 4 September 2018 through 7 September 2018

ER -

Cartesian cubical computational type theory: Constructive reasoning with paths and equalities

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this