`Instance.X.Properties` instead of many `Instance` about agda-categories HOT 10 CLOSED

Give in to the temptation 😃 . I agree with the proposal to create .Properties for this purpose, and moving previous code to that location.

from agda-categories.

it turns out the universe level are inconsistent. I will leave it for now.

from agda-categories.

The universe levels of what exactly are inconsistent? Up to now, I've found that all non-trivial level issues were quite informative [like the problem of Homs in Adjoint, which has now convinced me that the unit-counit definition is the right one, and the Hom-set one is a special case that only works when size issues are ignored.]

from agda-categories.

the problem is that Cats is incapable of internalizing the Functors category of categories in it, because Functors lifts universe levels to much bigger one, so I guess in Agda it is not possible to show Cats is a CCC.

from agda-categories.

https://ncatlab.org/nlab/show/Cat does warn of size issues.

And I just checked -- Functors does not have a suc in it. It does however basically insist that all levels in both input categories be equal. So for Category o o o, that should be able to internalize Functors.

from agda-categories.

that is true indeed. it is a very special case though.

from agda-categories.

It might be the only case provable in Agda. In some ways, it might also be the only 'true' case... Those size issues are real. Agda Levels are a very good proxy for them.

from agda-categories.

It feels like there are two issues here -- one about Cats being a CCC, and the other where to put certain properties. Both should be looked at, but shouldn't be linked. What should this issue be about?

from agda-categories.

this issue should be about the latter. I think in general it's a good idea to place properties close to where a concept is defined.

from agda-categories.

This issue seems obsolete, in the sense that the library now does have quite a few .Properties files. And I've trained myself to look there, and it works. I will articulate a 'design' of that, and put it somewhere.

from agda-categories.