[im_down_w_otp]

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/VA71gT5nIz...

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.