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
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more