All Questions
Tagged with agda axiom-free
2
questions
3
votes
2
answers
156
views
Can Hyperreal exist a axiom-free implementation in HoTT?
The main current implementations of hyperreal numbers are model-theoretic and set-theoretic approaches. Most of these implementations are strongly non-constructive, and many require a very deep ...
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 ...