Connecting constructive notions of ordinals in homotopy type theory

Fredrik Nordvall Forsberg, Chuangjie Xu, Nicolai Kraus

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

1 Downloads (Pure)

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.
Original languageEnglish
Title of host publication46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
EditorsNicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
Place of PublicationWadern, Germany
Pages42:1-42:16
Number of pages16
Volume202
DOIs
Publication statusPublished - 27 Aug 2021
Event46th International Symposium on Mathematical Foundations of Computer Science - Tallinn, Estonia
Duration: 23 Aug 202127 Aug 2021
Conference number: 46
https://compose.ioc.ee/mfcs/cfp.php

Conference

Conference46th International Symposium on Mathematical Foundations of Computer Science
Abbreviated titleMFCS 2021
Country/TerritoryEstonia
CityTallinn
Period23/08/2127/08/21
Internet address

Keywords

  • constructive ordinals
  • cantor normal forms
  • browser trees

Fingerprint

Dive into the research topics of 'Connecting constructive notions of ordinals in homotopy type theory'. Together they form a unique fingerprint.

Cite this