There was a version of Lean that supported HoTT, and I think it helped in making Lean popular. But that support has been dropped in Lean 3, and Lean 4 does not

There was a version of Lean that supported HoTT, and I think it helped in making Lean popular. But that support has been dropped in Lean 3, and Lean 4 does not support it either. Lean 4 itself seems to be a radical rewrite, and libraries written for Lean 3 do not work in Lean 4.