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
Profiles

Fredrik Nordvall Forsberg
 Computer And Information Sciences  Lecturer B
 SICSA
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