Proof-theoretic strength of Agda

Agda is a predicative type theory, so has a surprisingly low bound on its proof-theoretic strength. Things are a bit complicated because of some tricky level features, but if we ignore that, then a decent ordinal bound on it is the

References