Skip to main content

All Questions

3 votes
0 answers
113 views

Lower bounds in type theory proof assistant with ordinals and universes without axioms

I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024? My ...
Ember Edison's user avatar