@VictorTaelin I disagree on the consistency is enough to do mathematics, you can very weird stuff to MLTT like Nat iso Nat -> Nat and still be consistent.

Source

• URL: https://x.com/KleeneAlgebra/status/2073769031467766029
• Author: Alecs, B.P.Ed. (@KleeneAlgebra)
• Posted: 2026-07-05 14:00:40

Branch

1/ @KleeneAlgebra

@VictorTaelin

I disagree on the consistency is enough to do mathematics, you can very weird stuff to MLTT like Nat iso Nat -> Nat and still be consistent. I would like to see you convincing a mathematician to do math in that system.

Related

• Spine: 2026-07-04-sighs