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