Dr NICOLAI KRAUS NICOLAI.KRAUS@NOTTINGHAM.AC.UK
Professor of Theoretical Computerscience
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.
Citation
KRAUS, N., de Jong, T., Nordvall Forsberg, F., & Xu, C. (2023, June). Set-Theoretic and Type-Theoretic Ordinals Coincide. Paper presented at Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, USA
Presentation Conference Type | Conference Paper (unpublished) |
---|---|
Conference Name | Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
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
Apartness, sharp elements, and the Scott topology of domains
(2023)
Journal Article
On Small Types in Univalent Foundations
(2023)
Journal Article
Two-level type theory and applications
(2023)
Journal Article
Type-theoretic approaches to ordinals
(2023)
Journal Article
A rewriting coherence theorem with applications in homotopy type theory
(2022)
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