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
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…
1
3
has a project like this for cubical
2
1
Yeah I don't think it uses the agda HTML thingy - it's something custom
2
2
2