Awesome
Learning Material for Univalent Mathematics and the UniMath library
Lecture 4: Tactics in Coq (by Benedikt Ahrens)
Lecture 5: Set-Level Mathematics (by Carlo Angiuli)
Lecture 6: Univalent Category Theory (by Niels van der Weide)
Lecture 7: Synthetic Homotopy Theory (by Favonia)
Lecture 2: Fundamentals of Coq (by Marco Maggesi)
Lecture 4: Tactics in UniMath (by Ralph Matthes)
Lecture 5: Set-Level Mathematics (by Benedikt Ahrens)
Lecture 6: Univalent Category Theory (by Niels van der Weide)
Coq and UniMath Installation Instructions
Lecture 1: Spartan Type Theory by Andrej Bauer
Lecture 2: Fundamentals of Coq by Anders Mörtberg
Lecture 5: Set-Level Mathematics by Joj Helfer
Lecture 6: Category Theory in UniMath by Niels van der Weide
Lecture 8: UniMath: its origins, present, and future by Benedikt Ahrens