[dqpb]

Wonder why they didn’t do it in Lean?

[scapp]

Lean 3 introduced singleton-elimination which is inconsistent with HoTT. There's a project [0] that uses an attribute to restrict uses of that rule, but it isn't really ergonomic to use.

[0] https://github.com/gebner/hott3