UPDATE: This repo is deprecated. Please use Egbert's new repo: https://github.com/EgbertRijke/HoTT-Intro
Companion code to CMU course on Homotopy Type Theory, the Spring 2018 version taught by Egbert Rijke http://www.andrew.cmu.edu/user/erijke/hott/
Directory layout TBD.
Languages: Agda, possibly Lean to follow.
For general HoTT info see http://homotopytypetheory.org and https://github.com/HoTT
Agda resources:
- Agda wiki, includes installation info
- Official HoTT-Agda repo
- Agda mode for Atom text editor, for those allergic to emacs
- Martin Escardo Agda tutorial