Will lean support HoTT in the future?

Stream: general

[Keyao Peng]

I find HoTT or CuTT would be more convenient to the mathematicians, would Lean support this in the future?
And I heard of another new language Arend that supports CuTT, would this be a potential proof assistant?

[Johan Commelin]

@Keyao Peng you might be interested in reading through previous discussions on the topic. See https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020/topic/Previous.20discussions.20on.20Lean.20and.20HoTT/near/204191082 and the posts below it for a bunch of links.

[Johan Commelin]

Summary:

1. Lean 2 supported HoTT
2. Lean 3 has a HoTT mode
3. Several mathematicians on this chat are completely unconvinced that HoTT brings useful features
4. Several other mathematicians have played a bit with HoTT and think it looks very cool and has a lot of promise, but in practice it currently, right now doesn't seem to help with actual formalisation of mathematics. This could change in the future, but it requires fundamental improvements of the proof assistents.

[Johan Commelin]

Finally, yes, Arend looks cool.

[Thomas Eckl]

@Johan Commelin How do you activate the HoTT mode in Lean 3?

[Bryan Gin-ge Chen]

Lean 3 doesn't have a HoTT mode built in. The Lean 3 HoTT repository uses some tricks to "disable" singleton elimination which is inconsistent with HoTT.