Library design discussion about agda-categories HOT 6 CLOSED

After doing part of #1 and getting used to the library, I agree with the above design for the naming conventions. [Though see some of the issues I added recently.]

A lot of the things under Square right now really are not about 'commutative squares' (which is kind of what I expected from the name), but really various things about 'morphism reasoning'. I therefore suggest that all of these be moved to be under Morphism.Reasoning.

Lastly, I think we need to find a better home for "Examples of categories" than under Category (and some of them are scattered about too). It could be Category.Examples, though I'm not that happy with that suggestion. Nor with top-level Examples. I kind of like Category.Of as a kind of pun (category of sets, category of categories, etc).

from agda-categories.

I think it makes sense to name Morphism.Reasoning instead. Square is how the previous library calls it.

for the special categories, I think Category.Instance(s) looks better.

my next step is to deal with CCC and related concepts, but I am busy with a deadline this few days so I will join you once I get over it.

from agda-categories.

We have a (small) window of opportunity to improve the naming, we should grab it!

No worries about the timing - I happened to have a window now. Next week, I'm at a conference in Europe, so it's unclear where my time will be spent.

from agda-categories.

One more thing: I would like to minimize the use of rewrite. I prefer explicit proofs, and some of the proofs using rewrite seem too magical.

from agda-categories.

there isn't really an opportunity for rewrite in the raw category theoretic part in this library. the part I did in Isomorphism is kind of a meta-argument to formalize a general argument people usually make informally.

from agda-categories.

As an issue, I think everything here is agreed to. I'll link to this issue in the README, to remember it, but there's no point in keeping it open.

from agda-categories.