The concept of an identity-on-objects functor is important for defining various structures in category theory, such as Freyd categories and dagger categories. However, in a structural set theory such as ETCS or SEAR, there is no concept of equality of sets, and thus, an identity-on-objects functor cannot be defined via the usual definition. Instead, equality of sets is expressed through bijection of sets, which, when applied to the definition of identity-on-objects functor, yields a bijective-on-objects functor.
In foundations where categories are weak by default and thus the collection of objects do not form a set, the concept of a bijective-on-objects functor still makes sense for strict categories, where the functor is a strict functor by definition.
Another motivation for bijective-on-objects functors is that they together with full and faithful strict functors form an orthogonal factorization system on StrCat; see bo-ff factorization system. This factorization system can also be constructed using a generalized kernel.
A strict functor between two strict categories and is called bijective-on-objects, or bo, if it is a bijection on objects, if its underlying object function is a bijection .
To be more in accord with the principle of equivalence, one could require that the functor be bijective on objects only up to isomorphism; that is, it is essentially surjective and full on isomorphisms. However, from the point of view of factorization systems, the version of the concept of a bo functor which is in accord with the principle of equivalence is nothing more or less than an essentially surjective functor, since essentially surjective functors and ff functors form a bicategorical factorization system on the bicategory .
R. Street in Categorical and combinatorial aspects of descent theory proves
Proposition. A functor is bijective on objects if and only if it exhibits its codomain as the (2-categorical) codescent object of some simplicial category.
This can be generalized to any regular 2-category.
Every bijective-on-objects functor between two strict categories is an equivalent-on-objects functor between two strict categories.
In the context of type theory, if both strict categories live in a univalent universe , a bijective-on-objects functor also becomes an identity-on-objects functor due to the univalence axiom and the fact that equivalences between sets are equivalent to bijections of sets:
For sets and , there is an identity type , a type of equivalences between and , , and a type of bijections between and , , as well as canonical canonical functions and .
Since between equivalences between sets are equivalent to bijections between sets, there is a function which is an equivalence of types.
Since is univalent, is an equivalence of types . By the properties of equivalences, the function is also an equivalence of types . Thus there is a homotopy inverse .
Thus, in an univalent universe, bijective-on-objects functors and identity-on-objects functors are the same:
An identity-on-objects functor between strict categories and in a univalent universe is a strict functor with an identification , where is the underlying object function of the functor .
basic properties ofโฆ
Last revised on August 24, 2022 at 11:44:48. See the history of this page for a list of all contributions to it.