This code builds on—and includes a copy of—Martín Escardó et al.'s TypeTopology development (commit aaa462e) and works with Agda 2.7.0.1.

The relevant files for the paper are located at source/Ordinals/Exponentiation/.
In particular, see:

• The paper companion file source/Ordinals/Exponentiation/Paper.lagda
• The overview file source/Ordinals/Exponentiation/index.lagda

To check the results of the paper, download the code and run

cd source
agda Ordinals/Exponentiation/index.lagda

This will also check the file Ordinals/Exponentiation/Paper.lagda as it is included in the index.

A browseable HTML rendering of the relevant files is available at
https://ordinal-exponentiation-hott.github.io/Ordinals.Exponentiation.index.html