A dependent type theory following the lecture notes in the (pi-forall)[https://github.com/sweirich/pi-forall] repository.
This project was written trying to follow the notes as close as possible and implementing them "by hand". While the original repository was used as a "cheat-sheet" for when some modelling issues ocasionally arose.