add documentation to the code

[HuStmpHrrr]

I think we don't really have much documentation around. we surely have done some for non-trivial decisions but it could be helpful if we have a bit more documentation illustrating some basic categorical concepts or other useful stuff.

[svenkeidel]

Hello @HuStmpHrrr,

I can help with that. I'm well versed in category theory, but I'm quite a newbie in Agda. I would like to write some documentation for this library, but need some support to understand some of the design decisions.

For the major concepts such as categories, functors and natural transformations I would structure the documentation as follows:

• Mathematical Definition: A definition of the concept in clear mathematical terms. For example, "a category is a collection of objects ..."
• Implementation Details: A discussion of the implementation of the concept. For example, "this library implements categories as a setoid enriched categories because ..."
• Examples: A list of instances of the concept. For example, "the category of sets and functions [link to the set category] ..."

What do you think?

[svenkeidel]

For example like this (https://github.com/svenkeidel/agda-categories/blob/master/src/Categories/Category/Core.agda).

A few beginner questions:

• In which format do I have to write the documentation? I read something about restructured text.
• How do I add hyperlinks to other modules?
• How do I "compile" the documentation?

[HuStmpHrrr]

@svenkeidel thank you for contributing. as of now, we don't really have a standard of how to write documentations. at this moment, we just mark down things that we want to mention in comments. it's usually just a piece of surrounding text, e.g. https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Monoidal/Closed.agda#L6. currently Agda's support for documentation is quite primitive and I don't think rst is involved. regarding hyperlink, to my knowledge, there really isn't a support for that too. you can get the html output by following: https://agda.readthedocs.io/en/v2.6.1/tools/generating-html.html

at this point, documentation in any form is welcome. IMO, we should keep things common in category theory brief. usually it is the implementation that is more interesting. what you have looks quite good to me. @JacquesCarette probably has some opinions on this. we can mention some examples but if it's in comments, then I think just mentioning it is enough. if it's possible, we should actually prove it in the library. we've already got some instances in some *.Properties modules, e.g. Cat is cartesian closed https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Instance/Properties/Cats.agda#L153

[svenkeidel]

Thanks, this clarifies things. I will write some documentation for the most important definitions and then open a PR.

[JacquesCarette]

Sorry for the slow answer.

I quite like the sample documentation for Category.Core.

@HuStmpHrrr we could consider moving some of the files to literate Agda. Also, there is a restructured text version of Agda, so that is indeed possible, but that seems like too big a step to take just now.

Definitely I agree that "documentation in any form is welcome". And that the background category theory should be kept quite brief. When there is a choice made that appears in some online form, I add a link to that. [So I've put in quite a few URLs pointing to the nLab].

Examples are a slightly different matter. Too many examples and things will get bloated; that's why I started https://github.com/agda/categories-examples/. It is quite small now, but I'm hoping to grow it. Of course, some examples belong in the core library, because category itself builds on top of those examples. That Cat is CCC is one of those. So there are actual design decisions to be made that.

What you describe in your first message I would call a "literate textbook", and that would be super-cool to have. But I don't know if we currently have the technology to do that. agda-categories is a library, and that it can be used as such is extremely important. I would be very keen to see a "literate textbook" overlay on top of it, but less keen to see the library aspect disrupted by that. [Doing 'literate programming' properly, the way Knuth envisioned it, would actually help; unfortunately, there are missing features around 'chunks' that make that currently not possible.]

Having said all of that: in the current code base, the most important thing to document would be the design choices, and commentary around that. That would be extremely useful. Please feel free to pester us with questions on that. [There's also a Slack channel that we sometimes use, I can send you an invite]

[svenkeidel]

Ok, so brief on the category theory background and mainly focus on the design decisions. Got it.

Please feel free to pester us with questions on that. [There's also a Slack channel that we sometimes use, I can send you an invite]

Thanks for the offer, but I think it is better that we have these discussions on Github. This way other users can find the discussions and participate.

[HuStmpHrrr]

which part of the code would be better made into literate agda? is it a good practice to include some literate agda in a library?

[JacquesCarette]

1. Any code where we'd like to have more extensive documentation that displays well (with extra links, nice formatting, etc in the comments)
2. I think that's still evolving. I do believe that @WolframKahl's RATH-Agda library code is all literate, which ends up producing nice documents.