Document

# Connecting Constructive Notions of Ordinals in Homotopy Type Theory

## File

LIPIcs.MFCS.2021.70.pdf
• Filesize: 0.78 MB
• 16 pages

## Acknowledgements

We thank the participants of the conferences Developments in Computer Science and TYPES, as well as Helmut Schwichtenberg and Thorsten Altenkirch for fruitful discussions on this work. We are also grateful to the anonymous reviewers, whose remarks helped us improve the paper.

## Cite As

Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting Constructive Notions of Ordinals in Homotopy Type Theory. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 70:1-70:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.70

## Abstract

In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Type theory
##### Keywords
• Constructive ordinals
• Cantor normal forms
• Brouwer trees

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Peter Aczel. An introduction to inductive definitions. In Studies in Logic and the Foundations of Mathematics, volume 90, pages 739-782. Elsevier, 1977.
2. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, FoSSaCS '18, pages 293-310. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_16.
3. Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus. Partiality, revisited. In Javier Esparza and Andrzej S. Murawski, editors, FoSSaCS '17, pages 534-549. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_31.
4. Heinz Bachmann. Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordnungszahlen. Vierteljahrsschrift der Naturforschenden Gesellschaft in Zürich, 2:115-147, 1950.
5. Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. The Burali-Forti argument in HoTT/UF in Agda notation, 2020. Available at URL: https://www.cs.bham.ac.uk/~mhe/TypeTopology/BuraliForti.html.
6. Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. In Dale Miller, editor, FSCD '17, volume 84 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:18, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
7. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In G. Klein and R. Gamboa, editors, ITP '14, volume 8558 of Lecture Notes in Computer Science, pages 111-127, 2014.
8. L. E. J. Brouwer. Zur begründung der intuitionistische mathematik III. Mathematische Annalen, 96:451-488, 1926.
9. Wilfried Buchholz. A new system of proof-theoretic ordinal functions. Annals of Pure and Applied Logic, 32:195-207, 1986. URL: https://doi.org/10.1016/0168-0072(86)90052-7.
10. Wilfried Buchholz. Notation systems for infinitary derivations. Archive for Mathematical Logic, 30:227-296, 1991.
11. Cesare Burali-Forti. Una questione sui numeri transfiniti. Rendiconti del Circolo Matematico di Palermo (1884-1940), 11(1):154-164, 1897.
12. Pierre Castéran and Evelyne Contejean. On ordinal notations. Available at http://coq.inria.fr/V8.2pl1/contribs/Cantor.html, 2006.
13. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the delay monad by weak bisimilarity. Mathematical Structures in Computer Science, 29(1):67-92, 2019.
14. Alonzo Church. The constructive second number class. Bulletin of the American Mathematical Society, 44:224-232, 1938.
15. The Coq Development Team. The Coq proof assistant reference manual, 2021. URL: http://coq.inria.fr.
16. Thierry Coquand, Peter Hancock, and Anton Setzer. Ordinals in type theory. Invited talk at Computer Science Logic (CSL), http://www.cse.chalmers.se/~coquand/ordinal.ps, 1997.
17. Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. LICS '18, 2018.
18. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
19. Nachum Dershowitz. Trees, ordinals and termination. In M. C. Gaudel and J. P. Jouannaud, editors, TAPSOFT '93, pages 243-250. Springer, 1993.
20. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465-476, 1979.
21. Gabe Dijkstra. Quotient inductive-inductive definitions. PhD thesis, University of Nottingham, 2017.
22. Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124(1):1-47, 2003. URL: https://doi.org/10.1016/S0168-0072(02)00096-9.
23. Martín Escardó. Compact ordinals, discrete ordinals and their relationships, Since 2010-2021. Available at https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.html.
24. Robert W. Floyd. Assigning meanings to programs. In J.T. Schwartz, editor, Symposium on Applied Mathematics, volume 19, pages 19-32, 1967.
25. José Grimm. Implementation of three types of ordinals in Coq. Technical Report RR-8407, INRIA, 2013. Available at URL: https://hal.inria.fr/hal-00911710.
26. Peter Hancock. Ordinals and Interactive Programs. PhD thesis, University of Edinburgh, 2000.
27. W Charles Holland, Salma Kuhlmann, and Stephen H McCleary. Lexicographic exponentiation of chains. Journal of Symbolic Logic, pages 389-409, 2005.
28. S. C. Kleene. On notation for ordinal numbers. The Journal of Symbolic Logic, 3(4):150-155, 1938.
29. Daniel Licata and Michael Shulman. Calculating the fundamental group of the circle in homotopy type theory. In LICS '13, pages 223-232, 2013. URL: https://doi.org/10.1109/LICS.2013.28.
30. Peter Lefanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159-208, 2020.
31. Panagiotis Manolios and Daron Vroon. Ordinal arithmetic: algorithms and mechanization. Journal of Automated Reasoning, 34(4):387-423, 2005.
32. Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani. Three equivalent ordinal notation systems in cubical Agda. In CPP '20, pages 172-185. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373835.
33. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.
34. Peter H. Schmitt. A mechanizable first-order theory of ordinals. In R. Schmidt and C. Nalon, editors, TABLEAUX '17, volume 10501 of Lecture Notes in Computer Science, pages 331-346, 2017.
35. Kurt Schütte. Kennzeichnung von Ordinalzahlen durch rekursiv erklärte Funktionen. Mathematische Annalen, 127:15-32, 1954.
36. Kurt Schütte. Proof Theory. Springer, 1977.
37. Michael Shulman. The surreals contain the plump ordinals. Blog post at https://homotopytypetheory.org/2014/02/22/surreals-plump-ordinals/, 2014.
38. Gaisi Takeuti. Proof Theory. North-Holland, 2 edition, 1987.
39. Paul Taylor. Intuitionistic sets and ordinals. Journal of Symbolic Logic, 61(3):705-744, 1996.
40. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/, Institute for Advanced Study, 2013.
41. Oswald Veblen. Continuous increasing functions of finite and transfinite ordinals. Transactions of the American Mathematical Society, 9(3):280-292, 1908.
42. Niccolò Veltri. A type-theoretical study of nontermination. PhD thesis, Tallinn University of Technology, 2017.
43. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: a dependently typed programming language with univalence and higher inductive types. In ICFP '19, volume 3, pages 87:1-87:29. ACM, 2019.