The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2021.70
URN: urn:nbn:de:0030-drops-145100
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14510/
Go to the corresponding LIPIcs Volume Portal

Kraus, Nicolai ; Nordvall Forsberg, Fredrik ; Xu, Chuangjie

Connecting Constructive Notions of Ordinals in Homotopy Type Theory

pdf-format:
LIPIcs-MFCS-2021-70.pdf (0.8 MB)

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.

BibTeX - Entry

@InProceedings{kraus_et_al:LIPIcs.MFCS.2021.70,
  author =	{Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
  title =	{{Connecting Constructive Notions of Ordinals in Homotopy Type Theory}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{70:1--70:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14510},
  URN =		{urn:nbn:de:0030-drops-145100},
  doi =		{10.4230/LIPIcs.MFCS.2021.70},
  annote =	{Keywords: Constructive ordinals, Cantor normal forms, Brouwer trees}
}

Keywords: Constructive ordinals, Cantor normal forms, Brouwer trees
Collection: 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
Issue Date: 2021
Date of publication: 18.08.2021
Supplementary Material: A formalisation is available:
Software (Agda source code): https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott/src archived at: https://archive.softwareheritage.org/swh:1:dir:8f62d289d51a35a3f22fab3b9def1e1dbfcaf909
Software (Agda as html): https://cj-xu.github.io/agda/constructive-ordinals-in-hott/index.html

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI