All Questions
1
question
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 ...