Type Theory in Lean

To get this repository:

    git clone https://github.com/riccardobrasca/TypeTheory.git

    cd TypeTheory/
    
    lake exe cache get

    code .

The files are TypeTheory/*/name.lean.

If you want to work with a file make a copy and work on it, not on the original version.

Each folder contains a file pres.pdf with the slides I used during the talk. For example, the slides for the first lecture are in TypeTheory/L1/pres.pdf.

In the folder TypeTheory/Exercises you will find the exercises sheets and in TypeTheory/Exercises/Solutions the answers.