I'm really glad this exists! Homotopy type theory and category theory seem really fascinating, and this hyperlinked, formalised version is going to be a really useful learning resource. Thanks for your work!
Quote Tweet
I've posted about it before, but I'm formally announcing it now:
The 1lab is an open-source project with the goal of making formalised homotopy type theory open and accessible to as wide as audience as possible.
cubical.1lab.dev/index.html#abo
Show this thread