More Web Proxy on the site http://driver.im/

research-article

On Higher Inductive Types in Cubical Type Theory

Authors:

Thierry Coquand,

Anders MörtbergAuthors Info & Claims

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 255 - 264

https://doi.org/10.1145/3209108.3209197

Published: 09 July 2018 Publication History

Abstract

Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.

References

[1]

Peter Aczel. 1999. On Relating Type Theories and Set Theories. In Types for Proofs and Programs. LNCS, Vol. 1657. Springer, 1--18.

Digital Library

[2]

Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. 2017. Cartesian Cubical Type Theory. (2017). Draft available at https://www.cs.cmu.edu/~rwh/papers/uniform/uniform.pdf.

[3]

Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. 2017. Computational Higher Type Theory III: Univalent Universes and Exact Equality. (2017). Preprint arXiv:1712.01800v1.

[4]

Carlo Angiuli, Robert Harper, and Todd Wilson. 2017. Computational Higher-dimensional Type Theory. In POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. ACM, 680--693.

Digital Library

[5]

Steve Awodey and Michael A. Warren. 2009. Homotopy theoretic models of identity types. Math. Proc. Cambridge Philos. Soc. 146, 1 (2009), 45--55.

[6]

Guillaume Brunerie. 2016. On the homotopy groups of spheres in homotopy type theory. Ph.D. Dissertation. Université de Nice.

[7]

Evan Cavallo and Robert Harper. 2018. Computational Higher Type Theory IV: Inductive Types. (2018). Preprint arXiv:1801.01568v1.

[8]

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Types for Proofs and Programs (TYPES 2015) (LIPIcs), Vol. 69. 5:1--5:34.

[9]

Floris van Doorn. 2016. Constructing the Propositional Truncation Using Non-recursive HITs. In CPP '16: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. ACM, 122--129.

Digital Library

[10]

Peter Dybjer and Hugo Moeneclaey. 2018. Finitary Higher Inductive Types in the Groupoid Model. Electronic Notes in Theoretical Computer Science 336 (April 2018), 119--134.

[11]

Samuel Eilenberg. 1939. On the relation between the fundamental group on a space and the higher homotopy groups. Fund. Math. 32, 1 (1939), 167--175.

[12]

Richard Garner. 2009. Understanding the small object argument. Applied Categorical Structures 17, 3 (2009), 247--285.

[13]

Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. 2016. A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16. ACM, 565--574.

Digital Library

[14]

Simon Huber. 2016. Canonicity for Cubical Type Theory. (2016). Preprint arXiv:1607.04156.

[15]

Chris Kapulkin and Peter LeFanu Lumsdaine. 2012. The Simplicial Model of Univalent Foundations (after Voevodsky). (Nov. 2012). Preprint arXiv:1211.2851v4.

[16]

Nicolai Kraus. 2016. Constructions with Non-Recursive Higher Inductive Types. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'16. ACM, 595--604.

Digital Library

[17]

Daniel R. Licata and Guillaume Brunerie. 2015. A Cubical Approach to Synthetic Homotopy Theory. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'15. ACM, 92--103.

Digital Library

[18]

Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. 2018. Internal Universes in Models of Homotopy Type Theory. (2018). Preprint arXiv:1801.07664.

[19]

Peter LeFanu Lumsdaine and Michael Shulman. 2017. Semantics of higher inductive types. (May 2017). Preprint arXiv:1705.07088.

[20]

Ian Orton and Andrew M. Pitts. 2016. Axioms for Modelling Cubical Type Theory in a Topos. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) (LIPIcs), Vol. 62. 24:1--24:19.

[21]

Emily Riehl and Michael Shulman. 2017. A type theory for synthetic ∞-categories. Higher Structures 1, 1 (2017), 147--224.

[22]

Egbert Rijke. 2017. The join construction. (2017). Preprint arXiv:1701.07538v1.

[23]

Christian Sattler. 2017. The Equivalence Extension Property and Model Structures. (2017). Preprint arXiv:1704.06911v1.

[24]

Kristina Sojakova. 2016. The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory. ACM Transactions on Computational Logic 17, 4 (Nov. 2016), 29:1--29:19.

Digital Library

[25]

Andrew Swan. 2014. An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof. (2014). Preprint arXiv:1409.1829.

[26]

The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.

[27]

Vladimir Voevodsky. 2014. The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010). (2014). Preprint arXiv:1402.5556.

[28]

Vladimir Voevodsky. 2015. An experimental library of formalized Mathematics based on the univalent foundations. Mathematical Structures in Computer Science 25(2015), 1278--1294.

Cited By

Contente MMaietti M(2024)The Compatibility of the Minimalist Foundation with Homotopy Type TheoryTheoretical Computer Science10.1016/j.tcs.2024.114421(114421)Online publication date: Feb-2024
https://doi.org/10.1016/j.tcs.2024.114421
Myers DSati HSchreiber U(2024)Topological Quantum Gates in Homotopy Type TheoryCommunications in Mathematical Physics10.1007/s00220-024-05020-8405:7Online publication date: 8-Jul-2024
https://doi.org/10.1007/s00220-024-05020-8
Lamiaux TLjungström AMörtberg AKrebbers RTraytel DPientka BZdancewic S(2023)Computing Cohomology Rings in Cubical AgdaProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575677(239-252)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575677
Show More Cited By

Recommendations

Higher inductive types in cubical computational type theory

Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the ...
Cubical agda: a dependently typed programming language with univalence and higher inductive types

Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as ...
Type theory in type theory using quotient inductive types
POPL '16

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 2018

960 pages

ISBN:9781450355834

DOI:10.1145/3209108

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

LICS '18

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 9 - 12, 2018

Oxford, United Kingdom

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
273
Total Downloads

Downloads (Last 12 months)23
Downloads (Last 6 weeks)3

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Contente MMaietti M(2024)The Compatibility of the Minimalist Foundation with Homotopy Type TheoryTheoretical Computer Science10.1016/j.tcs.2024.114421(114421)Online publication date: Feb-2024
https://doi.org/10.1016/j.tcs.2024.114421
Myers DSati HSchreiber U(2024)Topological Quantum Gates in Homotopy Type TheoryCommunications in Mathematical Physics10.1007/s00220-024-05020-8405:7Online publication date: 8-Jul-2024
https://doi.org/10.1007/s00220-024-05020-8
Lamiaux TLjungström AMörtberg AKrebbers RTraytel DPientka BZdancewic S(2023)Computing Cohomology Rings in Cubical AgdaProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575677(239-252)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575677
Ljungström AMörtberg A(2023) Formalizing π 4 (S 3 ) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175833(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175833
Annenkov DCapriotti PKraus NSattler C(2023)Two-level type theory and applicationsMathematical Structures in Computer Science10.1017/S0960129523000130(1-56)Online publication date: 30-May-2023
https://doi.org/10.1017/S0960129523000130
Kiiskinen S(2023)Curiously Empty Intersection of Proof Engineering and Computational SciencesImpact of Scientific Computing on Science and Society10.1007/978-3-031-29082-4_3(45-73)Online publication date: 8-Jul-2023
https://doi.org/10.1007/978-3-031-29082-4_3
Baunsgaard Kristensen MMogelberg RVezzosi A(2022)Greatest HITs: Higher inductive types in coinductive definitions via induction under clocksProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533359(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533359
Pujet LTabareau N(2022)Observational equality: now for goodProceedings of the ACM on Programming Languages10.1145/34986936:POPL(1-27)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498693
Bentzen B(2022)Naive cubical type theoryMathematical Structures in Computer Science10.1017/S096012952200007X31:10(1205-1231)Online publication date: 15-Mar-2022
https://doi.org/10.1017/S096012952200007X
Swan AUemura T(2022)On Church’s thesis in cubical assembliesMathematical Structures in Computer Science10.1017/S096012952200006831:10(1185-1204)Online publication date: 21-Mar-2022
https://doi.org/10.1017/S0960129522000068
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents