Homotopy Type Theory

type theory notes: https://news.ycombinator.com/item?id=42440016#42444882

HoTT in Lean 4: https://github.com/forked-from-1kasper/ground_zero