Predicativity
Backlinks
Proof-theoretic strength of Agda
Topos