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://

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.