Document Open Access Logo

Homotopy Canonicity for Cubical Type Theory

Authors Thierry Coquand, Simon Huber, Christian Sattler

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.11.pdf
  • Filesize: 0.63 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Proof theory
  • Theory of computation → Computability
Keywords
  • cubical type theory
  • univalence
  • canonicity
  • sconing
  • Artin glueing

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this paper we show by a sconing argument that if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral.

Cite As Get BibTex

Thierry Coquand, Simon Huber, and Christian Sattler. Homotopy Canonicity for Cubical Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.11

Author Details

Thierry Coquand
  • Department of Computer Science and Engineering, University of Gothenburg, Sweden
Simon Huber
  • Department of Computer Science and Engineering, University of Gothenburg, Sweden
Christian Sattler
  • Department of Computer Science and Engineering, University of Gothenburg, Sweden

Funding

  • Huber, Simon: I acknowledge the support of the Centre for Advanced Study (CAS) in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the academic year 2018/19.

References

  1. P. Aczel. On Relating Type Theories and Set Theories. In T. Altenkirch, B. Reus, and W. Naraschewski, editors, Types for Proofs and Programs, volume 1657 of Lecture Notes in Computer Science, pages 1-18. Springer Verlag, Berlin, Heidelberg, New York, 1999. Google Scholar
  2. C. Angiuli, G. Brunerie, T. Coquand, K.-B. Hou (Favonia), B. Harper, and D. Licata. Cartesian cubical type theory. preprint available from the home page of D. Licata, 2017. Google Scholar
  3. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Parametricity and Dependent Types. In ICFP '10, pages 345-356, 2010. Google Scholar
  4. M. Bezem, T. Coquand, and S. Huber. A Model of Type Theory in Cubical Sets. In R. Matthes and A. Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107-128. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2014. Google Scholar
  5. John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic, 32:209-243, 1986. URL: http://dx.doi.org/10.1016/0168-0072(86)90053-9.
  6. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In T. Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  7. T. Coquand, S. Huber, and A. Mörtberg. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 255-264, New York, NY, USA, 2018. ACM. Google Scholar
  8. Thierry Coquand. Canonicity and normalization for dependent type theory. Theoretical Computer Science, 2019. Google Scholar
  9. P. Dybjer. Internal Type Theory. In Lecture Notes in Computer Science, pages 120-134. Springer Verlag, Berlin, Heidelberg, New York, 1996. Google Scholar
  10. S. Eilenberg. On the relation between the fundamental group of a space and the higher homotopy groups. Fundamenta Mathematicae, 32(1):169-175, 1939. Google Scholar
  11. P. Gabriel and M. Zisman. Calculus of fractions and homotopy theory, volume 35 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer, 1967. Google Scholar
  12. N. Gambino and J. Kock. Polynomial functors and polynomial monads. In Mathematical Proceedings of the Cambridge Philosophical Society, volume 154, pages 153-192. Cambridge University Press, 2013. Google Scholar
  13. N. Gambino and C. Sattler. The Frobenius condition, right properness, and uniform fibrations. Journal of Pure and Applied Algebra, 221(12):3027-3068, 2017. Google Scholar
  14. K. Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunkts. Dialectica, 12:280-287, 1958. Google Scholar
  15. M. Hofmann. Syntax and semantics of dependent types. In A.M. Pitts and P. Dybjer, editors, Semantics and logics of computation, volume 14 of Publ. Newton Inst., pages 79-130. Cambridge University Press, Cambridge, 1997. Google Scholar
  16. S. Huber. Canonicity for Cubical Type Theory. Journal of Automated Reasoning, 2018. Google Scholar
  17. A. Joyal. Notes on clans and tribes, 2017. URL: http://arxiv.org/abs/1710.10238.
  18. C. Kapulkin and P. LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky). arXiv preprint, 2012. URL: http://arxiv.org/abs/1211.2851.
  19. K. Kapulkin and V. Voevodsky. Cubical approach to straightening. preprint available from the home page of K. Kapulkin, 2018. Google Scholar
  20. G.M. Kelly. A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bulletin of the Australian Mathematical Society, 22(1):1–83, 1980. Google Scholar
  21. D. R. Licata, I. Orton, A. M. Pitts, and B. Spitters. Internal Universes in Models of Homotopy Type Theory. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  22. P. LeFanu Lumsdaine and M. Shulman. Semantics of higher inductive types. arXiv preprint, 2017. URL: http://arxiv.org/abs/1705.07088.
  23. I. Orton and A. M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:19, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  24. E. Palmgren and S.J. Vickers. Partial Horn logic and cartesian categories. Annals of Pure and Applied Logic, 145(3):314-353, 2007. Google Scholar
  25. Erik Palmgren and Steven J Vickers. Partial Horn logic and cartesian categories. Annals of Pure and Applied Logic, 145(3):314-353, 2007. Google Scholar
  26. E. Riehl and M. Shulman. A type theory for synthetic ∞-categories. Higher Structures, 1(1), 2018. Google Scholar
  27. M. Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25(5):1203-1277, 2015. Google Scholar
  28. Jonathan Sterling. Algebraic type theory and universe hierarchies. arXiv preprint, 2019. URL: http://arxiv.org/abs/1902.08848.
  29. T. Streicher. Semantics of Type Theory. Progress in Theoretical Computer Science. Birkhäuser Basel, 1991. Google Scholar
  30. A. Swan. An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof. Journal of Logic &Analysis, 8(1):1-35, 2016. Google Scholar
  31. A. Swan. Semantics of higher inductive types, 2017. On the HoTT mailing list. Google Scholar
  32. W. W. Tait. Intensional Interpretations of Functionals of Finite Type I. Journal of Symbolic Logic, 32(2):198-212, 1967. Google Scholar
  33. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  34. V. Voevodsky. The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010). Preprint arXiv:1402.5556 [math.LO], 2014. URL: http://arxiv.org/abs/1402.5556.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact