Contents

category theory

# Contents

## Idea

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.

## Definition

###### Definition

A strict functor between two strict categories $A$ and $B$ is called bijective-on-objects, or bo, if it is a bijection on objects, if its underlying object function $F_{ob}: ob(A) \to ob(B)$ is a bijection $F_{ob}: ob(A) \simeq ob(B)$.

## Principle of equivalence

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 $Cat$.

## Properties

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.

### Relation to equivalent-on-objects functors

Every bijective-on-objects functor between two strict categories is an equivalent-on-objects functor between two strict categories.

### Relation to identity-on-objects functors

In the context of type theory, if both strict categories live in a univalent universe $\mathcal{U}$, 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 $A:\mathcal{U}$ and $B:\mathcal{U}$, there is an identity type $A =_\mathcal{U} B$, a type of equivalences between $A$ and $B$, $A \simeq_\mathcal{U} B$, and a type of bijections between $A$ and $B$, $A \cong_\mathcal{U} B$, as well as canonical canonical functions $\mathrm{IdtoEquiv}:A =_\mathcal{U} B \to A \simeq_\mathcal{U} B$ and $\mathrm{IdtoBij}:A =_\mathcal{U} B \to A \cong_\mathcal{U} B$.

Since between equivalences between sets are equivalent to bijections between sets, there is a function $\mathrm{EquivtoBij}:A \simeq_\mathcal{U} B \simeq A \cong_\mathcal{U} B$ which is an equivalence of types.

Since $\mathcal{U}$ is univalent, $\mathrm{IdtoEquiv}$ is an equivalence of types $\mathrm{IdtoEquiv}:A =_\mathcal{U} B \simeq A \simeq_\mathcal{U} B$. By the properties of equivalences, the function $\mathrm{IdtoBij}$ is also an equivalence of types $\mathrm{IdtoBij}:A =_\mathcal{U} B \simeq A \cong_\mathcal{U} B$. Thus there is a homotopy inverse $\mathrm{BijtoId}:A \simeq_\mathcal{U} B \to A =_\mathcal{U} B$.

Thus, in an univalent universe, bijective-on-objects functors and identity-on-objects functors are the same:

###### Definition

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

Last revised on August 24, 2022 at 11:44:48. See the history of this page for a list of all contributions to it.