nLab equivalent-on-objects functor

Contents

Contents

Idea

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.

 Definition

A function f:ABf:A \to B between two types AA and BB is an equivalence if for all elements b:Bb:B the fiber of ff at bb is a singleton. This suggests the following definition of an identity-on-objects functor:

Definition

An identity-on-objects functor F:ABF: A\to B between categories AA and BB is a functor whose underlying object function F ob:ob(A)ob(B)F_{ob}: ob(A) \to ob(B) is an equivalence of types F ob:ob(A)ob(B)F_{ob}: ob(A) \simeq ob(B).

Properties

Relation to identity-on-objects functors

If both categories live in a univalent universe 𝒰\mathcal{U}, an equivalent-on-objects functor also becomes an identity-on-objects functor due to the univalence axiom:

For types A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U}, there is an identity type A= 𝒰BA =_\mathcal{U} B and a type of equivalences between AA and BB, A 𝒰BA \simeq_\mathcal{U} B, as well as a canonical function IdtoEquiv:A= 𝒰BA 𝒰B\mathrm{IdtoEquiv}:A =_\mathcal{U} B \to A \simeq_\mathcal{U} B. Since 𝒰\mathcal{U} is univalent, IdtoEquiv\mathrm{IdtoEquiv} is an equivalence of types IdtoEquiv:A= 𝒰BA 𝒰B\mathrm{IdtoEquiv}:A =_\mathcal{U} B \simeq A \simeq_\mathcal{U} B and thus there is a homotopy inverse EquivtoId:A 𝒰BA= 𝒰B\mathrm{EquivtoId}:A \simeq_\mathcal{U} B \to A =_\mathcal{U} B. Thus, in an univalent universe, equivalent-on-objects functors and identity-on-objects functors are the same:

Definition

An identity-on-objects functor F:ABF: A\to B between categories AA and BB in a univalent universe 𝒰\mathcal{U} is a functor with an identification EquivtoId(F ob):ob(A)= 𝒰ob(B)\mathrm{EquivtoId}(F_{ob}):ob(A) =_\mathcal{U} ob(B), where F ob:ob(A)ob(B)F_{ob}: ob(A) \to ob(B) is the underlying object function of the functor FF.

Relation to bijective-on-objects functors

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.

Relation to essentially surjective functors.

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.

See also

References

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.