Homotopy type theory is a mathematical foundation, like set theory, or Martin Lof's type theory. This is different from a proof assistant like Coq or Lean. In f

Homotopy type theory is a mathematical foundation, like set theory, or Martin Lof's type theory. This is different from a proof assistant like Coq or Lean. In fact, Lean has a library which implements part of HoTT (see https://github.com/leanprover/lean2/blob/master/hott/hott.md https://github.com/leanprover/lean2/blob/master/hott/hott.md). In short, there is no comparison between Lean and HoTT.