Projects per year
Abstract
We present three ordinal notation systems representing ordinals below epsilon zero in type theory, using recent typetheoretical innovations such as mutual inductiveinductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.
Original language  English 

Title of host publication  CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs 
Editors  Jasmin Blanchette, Catalin Hritcu 
Place of Publication  New York 
Pages  172–185 
Number of pages  14 
DOIs  
Publication status  Published  24 Jan 2020 
Keywords
 theory of computation
 proof theory
 type theory
 ordinal notation
 cantor normal form
 inductiveinductive definitions
 higher inductive types
 cubical Agda
 programming
Fingerprint
Dive into the research topics of 'Three equivalent ordinal notation systems in cubical Agda'. Together they form a unique fingerprint.Profiles

Fredrik Nordvall Forsberg
Person: Academic, Research Only
Projects
 1 Finished

Homotopy Type Theory: Programming and Verification
EPSRC (Engineering and Physical Sciences Research Council)
1/04/15 → 30/09/19
Project: Research
Datasets

Cubical Agda formalization of Three equivalent ordinal notation systems
Xu, C. (Creator) & Nordvall Forsberg, F. (Creator), Zenodo, 5 Apr 2023
Dataset