Tl; dr: The category Cat is defined "incorrectly", in particular its setoid hom equivalence relation is wrong (it does not agree with the ZFC definition of equality between functors). I propose that we redefine the category Cat with the "correct" setoid hom equivalence relation defined in StrictCat. This would be a long term project as obviously the category Cat is used in many places in the library.
Longer version:
As it stands, most of the library is consistent with ZFC-style classical mathematics. It does not use the law of excluded middle or UIP, so it admits interpretations in other theories such as homotopy type theory, etc. (Although due to technical issues with the propositional erasure in the extraction backend, the univalence axiom is not compatible with use of the sort Prop, so it would require a substantial and fairly unrealistic rewrite of the library to assume that axiom.)
In interpreting this library in the context of ZFC, you would generally quotient out by the setoid relation on the homsets of a category, because ZFC can prove function extensionality. This is why we want to use setoid homs, because Coq lacks function extensionality. Thus, when defining any concrete category whose objects are types with additional structure and whose morphisms are functions, we would generally want the setoid equivalence relationship on morphisms to be given by f \approx g := \forall x. f x = g x.
Indeed this is the case for most concrete categories in the library. An exception is the category Cat, where we identify two functors if they are naturally isomorphic. This is inconsistent with equality of functors in ZFC. The ZFC definition of equality between functors would be that two functors F, G are equal if Fx = Gx for all objects and F(f) = G(f) for all morphisms, appropriately transported along equalities.
In homotopy type theory this would be an acceptable definition for univalent categories but because we are not assuming the univalence axiom we do not get any benefits from defining things this way, so there is no good reason to appeal to homotopy type theory principles here. The downside is that it becomes impossible to define functors from the category Cat into any other category if it does not send naturally isomorphic functors to setoid-equivalent morphisms.
In a previous PR I gave an example of such a functor, namely the functor Cat -> Graph which sends each category to its underlying directed graph and sends each functor to its graph isomorphism. This is a well defined functor in ZFC but is not a well-defined functor in the current library, because it does not respect natural isomorphism of functors, which is why I created the alternative category StrictCat of categories and functors satisfying strict equality.
jwiegley
commented
2 months ago
Tl; dr: The category Cat is defined "incorrectly", in particular its setoid hom equivalence relation is wrong (it does not agree with the ZFC definition of equality between functors). I propose that we redefine the category Cat with the "correct" setoid hom equivalence relation defined in StrictCat. This would be a long term project as obviously the category Cat is used in many places in the library.
Longer version: As it stands, most of the library is consistent with ZFC-style classical mathematics. It does not use the law of excluded middle or UIP, so it admits interpretations in other theories such as homotopy type theory, etc. (Although due to technical issues with the propositional erasure in the extraction backend, the univalence axiom is not compatible with use of the sort Prop, so it would require a substantial and fairly unrealistic rewrite of the library to assume that axiom.)
In interpreting this library in the context of ZFC, you would generally quotient out by the setoid relation on the homsets of a category, because ZFC can prove function extensionality. This is why we want to use setoid homs, because Coq lacks function extensionality. Thus, when defining any concrete category whose objects are types with additional structure and whose morphisms are functions, we would generally want the setoid equivalence relationship on morphisms to be given by
f \approx g := \forall x. f x = g x. Indeed this is the case for most concrete categories in the library. An exception is the category Cat, where we identify two functors if they are naturally isomorphic. This is inconsistent with equality of functors in ZFC. The ZFC definition of equality between functors would be that two functors F, G are equal if Fx = Gx for all objects and F(f) = G(f) for all morphisms, appropriately transported along equalities. In homotopy type theory this would be an acceptable definition for univalent categories but because we are not assuming the univalence axiom we do not get any benefits from defining things this way, so there is no good reason to appeal to homotopy type theory principles here. The downside is that it becomes impossible to define functors from the category Cat into any other category if it does not send naturally isomorphic functors to setoid-equivalent morphisms. In a previous PR I gave an example of such a functor, namely the functor Cat -> Graph which sends each category to its underlying directed graph and sends each functor to its graph isomorphism. This is a well defined functor in ZFC but is not a well-defined functor in the current library, because it does not respect natural isomorphism of functors, which is why I created the alternative category StrictCat of categories and functors satisfying strict equality.