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\colon 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\colon V\to A$ and a 2-morphism $\alpha\colon f v \to g v$.

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

$Hom(X,V) \to Ins(Hom(X,f),Hom(X,g))$

is an equivalence, where $Ins(Hom(X,f),Hom(X,g))$ denotes the category whose objects are pairs $(u,\beta)$ where $u\colon X\to A$ is a morphism and $\beta\colon f u \to g u$ is a 2-morphism. If this functor is an isomorphism of categories, then we say that $V\xrightarrow{v} 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 Cat$ is the diagram

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.

Examples

Let $C$ denote a category and $F : C \rightarrow C$ denote a functor. Then the notion of an algebra for an endofunctor of $F$ corresponds to the inserter of $F$ and $\mathrm{id}_C$, and the notion of a coalgebra for an endofunctor of $F$ corresponds to the inserter of $\mathrm{id}_C$ and $F$.

Last revised on January 13, 2018 at 00:40:31.
See the history of this page for a list of all contributions to it.