One thing I very strongly appreciate about Agda is how incredibly easy it is to generate HTML from proofs. Here's the generated HTML for the exercise I wrote yesterday, updated to account for some feedback: dependenttyp.es/classes/artifa
Conversation
Replying to
It's so nice! When I like to click around the stdlib (agda.github.io/agda-stdlib/RE) sometimes when I am bored. Hoping that they publish cubical one day…
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