3 ms·

Wonder why they didn’t do it in Lean?

• scapp 5y ago
  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 https://github.com/gebner/hott3