AgdaHoTT This is some work I did while thumbing through the HoTT book. https://homotopytypetheory.org/book/ Update: Nice hyperlinked version now included on my personal website at https://shaunharker.com/portfolio/agda!