Let be a pair of parallel 1-morphisms in a 2-category. The iso-inserter of and is a universal object equipped with a morphism and an invertible 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 an invertible 2-morphism. If this functor is an isomorphism of categories, then we say that is a strict iso-inserter.
Iso-inserters and strict iso-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
Any strict iso-inserter is, in particular, an iso-inserter. (This is not true for all strict 2-limits.)
Since is equivalent to , iso-inserters (but not strict iso-inserters) can equivalently be described as the conical limit of a diagram of shape , which might be called a (non-strict) pseudo-equalizer. A strict pseudo-equalizer—that is, a strict pseudolimit of a diagram of shape —is not the same as a strict isoinserter, but if it exists, a strict pseudo-equalizer is also, in particular, a (non-strict) iso-inserter. The relationship between isoinserters and pseudoequalizers is analogous to the relationship between iso-comma-objects and pseudo-pullbacks.
Iso-inserters can be constructed as an inserter followed by an inverter (for both the strict and non-strict versions). In particular, it follows that strict iso-inserters are a type of PIE-limit.
Revised on December 14, 2010 06:05:20
by Mike Shulman