HoTT exercises in Lean

Stream: Type theory

[Ken Lee]

Hi, I've been reading some homotopy type theory and want to try out some exercises in a proof assistant. I heard that there is some sort of 'HoTT mode' in Lean 3, but I'm not sure how to install/use it.

[Scott Morrison]

https://github.com/gebner/hott3

[Scott Morrison]

(I can't tell you anything more than that! :-)

[Jannis Limperg]

Note that this is a giant hack. If you want a system with proper HoTT support, use Coq or Agda with postulated univalence or Cubical Agda with builtin univalence.

[Ken Lee]

Jannis Limperg said:

Note that this is a giant hack. If you want a system with proper HoTT support, use Coq or Agda with postulated univalence or Cubical Agda with builtin univalence.

I'm not doing anything serious, but noted!

[Brandon Brown]

Or Arend