Three Equivalent Ordinal Notation Systems in Cubical Agda

POPL 2020