Use Literate Agda?

[HarrisonGrodin]

So far, we have .agda files. However, it might be worth using Literate Agda files .lagda.md, which lets us:

• include prose describing our constructions, in Markdown (allowing for bold, math, links, etc.)
• default-hide boring details

[jonsterling]

this sounds like a pretty good idea!

[HarrisonGrodin]

I've been thinking about it more, and it seems almost obvious in retrospect! Especially as we formalize more, using Literate Agda will mean we'll not only end up with formalizations of algorithms, but a readable (hopefully!) textbook with inline code snippets.