Description
It's come up before (esp. in discussions with @JacquesCarette ) ... but we have ended up documenting a lot of quite delicate/subtle design/ux decisions in the library either purely 'locally' in modules themselves (but typically lacking much of the detail of the underlying rationale: the definitions are supposed to 'explain themselves'... cf. the 'self-documenting' ideology of dependent type theory), or 'worse', as part of the 'essentially ephemeral' history (sic: you have to be very diligent to trace discussions back through the CHANGELOG and/or the GitHub issue/PR histories, esp. that recorded in commit messages ;-), or the agda mailing list for that matter...).
And/Hence future users/developers of the library don't currently have a 'reasonable' place to consult on such things.
So we should try to develop such a thing, but the prospect of how to lift all of that accumulated design rationale into a reference document... gives me a headache!
Cf the philosophy underlying the main Agda issue agda/agda#7003