Was there a reason for the move away from HoTT? I seem to recall looking this up a while ago but didn't find a solid answer. Was there a fork version 2 that continues development with HoTT?
Though, given then above linked discussion, I expect that never to become officially supported. But who knows, I don't think Lean 2 started life intending to handle HoTT either.
There's a somewhat active integration of HoTT into Lean 3 ongoing here: https://github.com/gebner/hott3
Though, given then above linked discussion, I expect that never to become officially supported. But who knows, I don't think Lean 2 started life intending to handle HoTT either.