Two categories with the same collection of objects with an identity-on-objects functor is a category enriched in the arrow category of Set.
See also M-category and F-category.
First, we distinguish between a category, and a category structure on a collection of objects, in the same way one does between a proset and a preorder, the equivalence relation structure on a collection of objects, in (0, 1)-category theory.
A category structure on a collection of objects is a family of sets whose elements are called morphisms, indexed by objects and , such that
such that
A category is a collection with a category structure indexed by objects and .
Two categories with the same collection of objects and is a collection with two category structures and indexed by objects and . The categories and are defined to be and respectively.
An identity-on-objects functor between two categories with the same collection of objects and is a family of functions which preserve the category structure on the type families:
composition of morphisms is preserved: for all morphisms and , ,
identity morphisms are preserved: .
What does it mean for two categories to have the same collection of objects?
The current definition defines such a structure as having one collection of object and two category structures. In type theory, this could equivalently be defined as actually two categories and whose collections of objects are judgmentally equal to each other: .
Historically, authors have tried to use propositional equality to define two categories with the same collection of objects. However, this runs into a number of problems:
In material set theories, one could postulate the condition that . However, it mentions equality of sets, which means that the definition violates the principle of equivalence.
In structural set theory such as SEAR or ETCS with elements, one can’t use equality of sets to define “having the same object”, since where there is no notion of equality of sets, only equality of functions, relations, and elements. One could instead use bijection, but that leads to a different concept, the notion of bijective-on-objects functor.
In type theory, propositional equality is represented by the identity type or the path type, but doesn’t actually have to be valued in propositions. One postulates the existence of identifications and , resulting in an identification . But this is additional structure in type theory which results in a different mathematical object than the current definition of an identity-on-objects functor. Additionally, the definition is only valid if the categories are in a type universe. For categories which don’t belong to any universe, one could instead use equivalence, but that leads to a different concept, the notion of equivalent-on-objects functor.
Hence, the notion of “two categories with the same collection of objects” is somewhat of a red herring, because it is defined as an object with two category structures, rather than two categories with the same collection of objects.
Historically, the notion of identity-on-objects functor in between two categories with the same collection of objects was defined to be an actual functor, additionally having a function on the objects which is the identity function on . This was where the original name “identity-on-objects functor” comes from. The problem with this definition is twofold:
In a material set theory or structural set theory or a type theory with axiom K, the above definition violates the principle of equivalence if one were to use it to define concrete dagger categories such as Rel, Hilb or concrete groupoids such as the permutation category, since in those cases the definition explicitly refers to propositional equality of sets.
In a univalent type theory, identity functions do not necessarily violate the principle of equivalence, because the identity type for object is not necessarily a proposition, and in the presence of univalence, is necessarily required to satisfy the principle of equivalence. However, the identifications are additional structure on the mathematical object, and thus does not result in the same object as the definitions above do.
As a result, the current definition of an identity-on-objects functor, valid in all foundations and respecting the principle of equivalence, was adopted, which doesn’t have such an identity function on the objects. However, the name “identity-on-objects functor” then becomes a red herring, since it is not actually a functor between the two objects collections.
Sometimes we want an identity-on-objects functor which behaves like a contravariant endofunctor. In this case, one does not need the notion of “two categories with the same collection of objects”.
A contravariant endofunctor which is the identity-on-objects on a category is a family of functions such that
composition of morphisms is reversed: for all morphisms and , ,
identity morphisms are preserved: .
This is used in particular for defining dagger categories and groupoids.
A dagger category is a category with an identity-on-objects contravariant endofunctor , such that for all objects and and morphisms , .
A groupoid is a category with an identity-on-objects contravariant endofunctor such that for all objects and and morphisms , and .
Last revised on June 8, 2023 at 18:50:49. See the history of this page for a list of all contributions to it.