3 ms·

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 con

• im_down_w_otp 8y ago
  This was a discussion I remember coming across not long ago when I had the same question: https://groups.google.com/forum/#!topic/lean-user/VA71gT5nIzM https://groups.google.com/forum/#!topic/lean-user/VA71gT5nIz... There's a somewhat active integration of HoTT into Lean 3 ongoing here: https://github.com/gebner/hott3 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.