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 be a pair of parallel 1-morphisms in a 2-category. The inserter of and is a universal object equipped with a morphism and a 2-morphism .
More precisely, universality means that for any object , the induced functor
is an equivalence, where denotes the category whose objects are pairs where is a morphism and is a 2-morphism. If this functor is an isomorphism of categories, then we say that 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 and the weight is the diagram
where is the terminal category and is the interval category. Note that inserters are not equivalent to any sort of conical 2-limit.
An inserter in (see opposite 2-category) is called a coinserter in .
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 January 13, 2018 at 00:40:31. See the history of this page for a list of all contributions to it.