Hello! This is part of my independent "LEANrning experience" project of formalizing the initial chapters of the HoTT book. Here you should find (alternatives?) definitions and proofs of theorems and solutions to exercises of the HoTT book using the LEAN theorem prover.

Disclaimer: Most definitions and proofs formalized here are already present in the HoTT library of Lean found here. This project is mainly of a self-learning nature.

Some proofs and definitions found here are constructed independently, though.