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 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 .
In the strict 2-category Cat of categories, inserters can be concretely described as follows.
The input data is two categories, and , and two functors, . The objects of the inserter are pairs , where and . Morphisms are morphisms such that . The functor from the inserter to discards the data of .
The inserter in 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.
G.J. Bird, G.M. Kelly, A.J. Power, R.H. Street, Flexible limits for 2-categories, J. Pure and Applied Algebra 61:1, 1-27, 1989, doi:10.1016/0022-4049(89)90065-0
Fernando Lucatelli Nunes, Freely generated -categories, coinserters and presentations of low dimensional categories, arxiv/1704.04474
Last revised on December 17, 2022 at 10:42:56. See the history of this page for a list of all contributions to it.