Dr NICOLAI KRAUS NICOLAI.KRAUS@NOTTINGHAM.AC.UK
Research Fellow
Set-Theoretic and Type-Theoretic Ordinals Coincide
KRAUS, NICOLAI; de Jong, Tom; Nordvall Forsberg, Fredrik; Xu, Chuangjie
Authors
TOM DE JONG Tom.DeJong@nottingham.ac.uk
Research Fellow
Fredrik Nordvall Forsberg
Chuangjie Xu
Abstract
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.
Presentation Conference Type | Conference Paper (unpublished) |
---|---|
Conference Name | Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Conference Location | Boston, USA |
Start Date | Jun 26, 2023 |
End Date | Jun 29, 2023 |
Deposit Date | Jul 4, 2023 |
Publicly Available Date | Jul 14, 2023 |
Public URL | https://nottingham-repository.worktribe.com/output/22715787 |
Files
Set-Theoretic and Type-Theoretic Ordinals Coincide
(482 Kb)
PDF
You might also like
Type-theoretic approaches to ordinals
(2023)
Journal Article
A rewriting coherence theorem with applications in homotopy type theory
(2022)
Journal Article
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
(2020)
Conference Proceeding
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
(2019)
Presentation / Conference
Univalent higher categories via complete semi-segal types
(2017)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search