Three Equivalent Ordinal Notation Systems in Cubical Agda

DOI10.1145/3372885.3373835MaRDI QIDQ6317695zbMATH OpenFDO

Authors Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani

Publication date 24 April 2019

Full work available at URL https://doi.org/10.1145/3372885.3373835

Proof theory in general (including proof-theoretic semantics) (03F03)

Abstract: We present three ordinal notation systems representing ordinals below

v a r e p s i l o n_{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.

This page was built for publication: Three Equivalent Ordinal Notation Systems in Cubical Agda

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6317695)