HoTT
- Introductions:
- Rijke: book: [[@Rijk2022]]
- Escardo: book: Introduction to Univalent Foundations of Mathematics with Agda
- Grayson: paper: [An introduction to univalent foundations for mathematicians]; book: Symmetry
- Alterkirch: paper: [Na ̈ıve Type Theory]; chaper of: [Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts] | book: Tao of Types
- agda-unimath
- 1lab.dev github