In type theory, the concept of a bijective-on-objects functor is only valid for categories whose type forms a set, i.e. strict categories. However, we would want a similar notion for general categories. Thus, comes the concept of equivalent-on-objects functor.
A function between two types and is an equivalence if for all elements the fiber of at is a singleton. This suggests the following definition of an identity-on-objects functor:
An identity-on-objects functor between categories and is a functor whose underlying object function is an equivalence of types .
If both categories live in a univalent universe , an equivalent-on-objects functor also becomes an identity-on-objects functor due to the univalence axiom:
For types and , there is an identity type and a type of equivalences between and , , as well as a canonical function . Since is univalent, is an equivalence of types and thus there is a homotopy inverse . Thus, in an univalent universe, equivalent-on-objects functors and identity-on-objects functors are the same:
An identity-on-objects functor between categories and in a univalent universe is a functor with an identification , where is the underlying object function of the functor .
For strict categories, an equivalent-on-objects functor is a bijective-on-objects functor, as equivalence of sets is bijection of sets, and the type of objects for strict categories is a set.
For univalent categories, an equivalent-on-objects functor is a essentially surjective functor. This is because the type of objects of every univalent category is a groupoid/1-truncated, which means that equivalence of the object types is equivalence of groupoids and thus essentially surjective.
An isomorphism of categories is a fully faithful equivalent-on-objects functor. As a result, every adjoint equivalence of univalent categories is an isomorphism of univalent categories, since every adjoint equivalence is essentially surjective.
For the definition of isomorphism of categories and adjoint equivalence of univalent categories, and equivalence of the two definitions for functors between univalent categories:
Last revised on August 24, 2022 at 14:59:00. See the history of this page for a list of all contributions to it.