Lean 4 HoTT Library

Stream: lean4

[Uranus Testing]

If anyone interested, I recently finished switching to Lean 4 in my HoTT library. It “disables” large elimination using checker ported from Gabriel Ebner’s library. My library is smaller comparing to hott3 or library from Lean 2, so contributions are always welcome, if you want to port some things from Lean 2 HoTT Library. Besides that, I also implemented “calc” based on parser written by Mario Carneiro allowing to use arbirary relations (i.e. something like calc 1 = 2 : sorry ... < 3 : sorry) and variant of reflexivity/symmetry/transitivity tactics. Feel free to use these things, if someone wants.
Compared to Lean 3, Lean 4’s ability to extend syntax is pure fun: it allows us to write things like λ n m, ∥Sⁿ∥ₘ, λ n, πₙ(Sⁿ), or even λ abc, Sᵃᵇᶜ without breaking anything.