2-Category is in fact Bicategory about agda-categories HOT 5 CLOSED

I was thinking that that may have been the case. And it would sort of be if Cats as a monoidal category had completely trivial associator and unitors. And you are likely correct that strict equality of functors requires K.

I guess the issue here is that Cats is not strict. To define 2-Category, one would have to define things over a strict version of Cats.

But note that https://ncatlab.org/nlab/show/1-category and https://ncatlab.org/nlab/show/strict+category seem to be inconsistent! 1-category has talks about 'equality' on Morphisms as the source of strictness, while the latter talks about equality on objects.

from agda-categories.

yeah at this point I won't rely on nLab for all explanations. I suppose it is good to find out what the literature says. that being said, since bicategory is a more accurate concept for the definition, the renaming can at least prevent further confusion.

from agda-categories.

Yes, please rename.

Also, I think it would make sense to create a PropCategory (better name? StrictCategory would be misleading) where we don't have Hom-Setoids but Hom sets with propositional equality. Then 2-Category could be defined to be Enriched over that. I can try to start formalizing that.

from agda-categories.

There's useful discussion at https://ncatlab.org/nlab/show/type-theoretic+definition+of+category

from agda-categories.

This particular issue is taken care of. Remaining issues are documented elsewhere.

from agda-categories.