Agda development of the paper "Set-Theoretic and Type-Theoretic Ordinals Coincide"

All the Agda files are tested with Agda version 2.6.2.2 and

• Section II is building on Escardó's TypeTopology library (commit: 318d913c878c1f3cbcfd03c911ed6c1461bf1d9f), and
• Section III is building on the Cubical Agda library (version 0.4).

An html rendering of the Agda code is available here.