Homotopy Type Theory in Agda. Brunerie, G., Hou (Favonia), K., Cavallo, E., & others .
Homotopy Type Theory in Agda [link]Paper  bibtex   
@online{hott-in:agda,
  title        = {{Homotopy Type Theory in Agda}},
  author       = {
    Guillaume Brunerie and Kuen-Bang {Hou (Favonia)} and Evan Cavallo and
    others
  },
  url          = {https://github.com/HoTT/HoTT-Agda},
}

Downloads: 0