# Three equivalent ordinal notation systems in cubical Agda.

POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages New Orleans LA USA January, 2020（2020）

Abstract

We present three ordinal notation systems representing ordinals below ε0 in type theory, using recent type-theoretical innovations such as mutual inductive-inductive 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.

MoreTranslated text

Key words

Ordinal notation, Cantor normal form, inductive-inductive definitions, higher inductive types, cubical Agda

AI Read Science

Must-Reading Tree

Example

Generate MRT to find the research sequence of this paper

Chat Paper

Summary is being generated by the instructions you defined