> Isn't Lean HoTT? No. Lean is good old fashioned Martin-Löf type theory. HoTT is that type theory + univalence + higher inductive types. Lean actually has pro

> Isn't Lean HoTT? No. Lean is good old fashioned Martin-Löf type theory. HoTT is that type theory + univalence + higher inductive types. Lean actually has proof irrelevance, which is incompatible with HoTT. But the good news is you don't need HoTT to verify software. Type theory is already quite capable of it, despite what others in this thread would like you to believe.