nLab (infinity,1)-coequalizer

Context

(∞,1)(\infty,1)-Category theory

Internal (∞,1)(\infty,1)-Categories

Directed homotopy type theory

Limits and colimits

\tableofcontents

Idea

An (∞,1)(\infty,1)-coequalizer is a colimit in an (∞,1)-category 𝒞\mathcal{C} over a diagram of shape

{a⇉b}→𝒞. \{ a \rightrightarrows b\} \to \mathcal{C} \,.

In other words it is a cocone

{a⇉b→coeq(a,b)}→𝒞. \{ a \rightrightarrows b \to \mathrm{coeq}(a, b)\} \to \mathcal{C} \,.

which is universal among all such cocones in the (∞,1)(\infty,1)-categorical sense.

This is the analog in (∞,1)-category theory of the notion of coequalizer in category theory.

Incarnations

In model categories

In simplicial type theory

For Segal types

In simplicial type theory, the Segal types are the types that represent (infinity,1)-precategories. Let AA be a Segal type in simplicial type theory, and let x:Ax:A and y:Ay:A be two elements in AA and let f:hom A(x,y)f:\mathrm{hom}_A(x, y) and g:hom A(x,y)g:\mathrm{hom}_A(x, y) be two morphisms from xx to yy. The (∞,1)(\infty,1)-coequalizer of ff and gg is an tuple consisting of

such that

in(f,g)∘f=compin(f,g)andin(f,g)∘g=compin(f,g)\mathrm{in}(f, g) \circ f = \mathrm{compin}(f, g) \qquad \mathrm{and} \qquad \mathrm{in}(f, g) \circ g = \mathrm{compin}(f, g)

For arbitrary types

The notion of an (∞,1)(\infty,1)-coequalizer can be generalised from Segal types to arbitrary types in simplicial type theory, which represent simplicial infinity-groupoids. In a Segal type AA, given morphisms f:hom A(x,y)f:\mathrm{hom}_A(x, y), g:hom A(y,z)g:\mathrm{hom}_A(y, z), and h:hom A(x,z)h:\mathrm{hom}_A(x, z), g∘f=hg \circ f = h if and only if hh is the unique composite of ff and gg. This means that we can use the latter condition in the definition of an (∞,1)(\infty,1)-coequalizer in types which are not Segal and thus do not have a composition function on morphisms.

Thus, let AA be a type in simplicial type theory, and let x:Ax:A and y:Ay:A be two elements in AA and let f:hom A(x,y)f:\mathrm{hom}_A(x, y) and g:hom A(x,y)g:\mathrm{hom}_A(x, y) be two morphisms from xx to yy. The (∞,1)(\infty,1)-coequalizer of ff and gg is an tuple consisting of

such that

The fact that this definition works for any type AA implies that (∞,1)(\infty,1)-coequalizers should be definable in any simplicial infinity-groupoid or simplicial object in an (infinity,1)-category, not just the (∞,1)(\infty,1)-categories or category objects in an (infinity,1)-category.

References

(∞,1)(\infty,1)-coequalizers are defined in: