Definitions
Transfors between 2-categories
Morphisms in 2-categories
Structures in 2-categories
Limits in 2-categories
Structures on 2-categories
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.
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
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
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^{op}$ (see opposite 2-category) is called a coinserter in $K$.
In the strict 2-category Cat of categories, inserters can be concretely described as follows.
The input data is two categories, $A$ and $B$, and two functors, $F,G\colon A\to B$. The objects of the inserter are pairs $(X,b)$, where $X\in A$ and $b\colon F(X)\to G(X)$. Morphisms $(X,b)\to(X',b')$ are morphisms $f\colon X\to X'$ such that $b'\circ F(f)=G(f)\circ b$. The functor from the inserter to $A$ discards the data of $b$.
The inserter in $Cat$ is also called the category of dialgebras.
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.
Last revised on November 22, 2022 at 10:23:54. See the history of this page for a list of all contributions to it.