Contents

Idea

An inserter is a particular kind of 2-limit in a 2-category, which universally inserts a 2-morphism between a pair of parallel 1-morphisms.

Definition

Let $f,g:A\rightrightarrows B$ be a pair of parallel 1-morphisms in a 2-category. The inserter of $f$ and $g$ is a universal object $V$ equipped with a morphism $v:V\to A$ and a 2-morphism $\alpha :fv\to gv$.

More precisely, universality means that for any object $X$, the induced functor

is an equivalence, where $\mathrm{Ins}(\mathrm{Hom}(X,f),\mathrm{Hom}(X,g))$ denotes the category whose objects are pairs $(u,\beta )$ where $u:X\to A$ is a morphism and $\beta :fu\to gu$ is a 2-morphism. If this functor is an isomorphism of categories, then we say that $V\stackrel{v}{\to }A$ is a strict inserter.

Inserters and strict inserters can be described as a certain sort of weighted 2-limit, where the diagram shape is the walking parallel pair $P=(\cdot \rightrightarrows \cdot )$ and the weight $P\to \mathrm{Cat}$ is the diagram

where $1$ is the terminal category and $I$ is the interval category. Note that inserters are not equivalent to any sort of conical 2-limit.

An inserter in $K^{\mathrm{op}}$ (see opposite 2-category) is called a coinserter in $K$.

Properties

• Any inserter is a faithful morphism, and also a conservative morphism, but not in general a fully faithful morphism.

• Any strict inserter is, in particular, an inserter. (This is not true for all strict 2-limits.)

• Strict inserters are (by definition) a particular class of PIE-limits.