ZZZZ: 16p

Thank you for this development of homotopy type theory basics. I cannot give you
the full point scores because you have only definitions, no proofs, and Lean is
about proofs, but on the other hand some of your definitions are quite
sophisticated, which is nice. If you're interested in HoTT in Lean, you might
find this paper interesting:

    https://florisvandoorn.com/papers/leanhott.pdf
