# nLab cocylinder

### Context

#### Limits and colimits

limits and colimits

# Cocylinders and mapping cocylinders

## Ideas

In algebraic topology and homotopy theory, a cocylinder is a dual construction to a cylinder. In contexts where spatial intuition is involved, it is perhaps more often called a path space ${X}^{I}$ or a path space object. In general, however, a cocylinder, ${X}^{I}$, may not involve any object $I$ nor use a mapping space in its construction, see cylinder functor for the discussion of the dual point.

## Definition (cocylinders and cocylinder functors)

These are the duals of cylinders and cylinder functors? so can safely be left as an exercise.

## Ideas continued

Similarly, the mapping cocylinder, which is dual to the mapping cylinder, is equally called the mapping path space or mapping path fibration. It provides a canonical way to factor any map as a homotopy equivalence followed by a fibration.

## Definition (mapping cocylinders)

### In category theory

For a topological space $X$, its cocylinder is simply the path space ${X}^{\left[0,1\right]}$. More generally, in a cartesian closed category with an interval object $I$, the cocylinder of an object $X$ is the exponential object ${X}^{I}$. Even more generally, in a model category the cocylinder of any object is the path space object — the factorization of the diagonal morphism $X\to X×X$ as an acyclic cofibration followed by a fibration.

In any of these cases:

###### Definition

Given a morphism $f:X\to Y$, its mapping cocylinder (or mapping path space or mapping path fibration) is the pullback

$\begin{array}{ccc}\mathrm{Cocyl}\left(f\right)& \to & X\\ ↓& & ↓f\\ {Y}^{I}& \stackrel{{\mathrm{ev}}_{0}}{\to }& Y\\ {↓}^{{\mathrm{ev}}_{1}}\\ Y\end{array}$\array{ Cocyl(f)&\to& X\\ \downarrow&&\downarrow f \\ Y^I&\stackrel{ev_0}{\to}&Y \\ \downarrow^{\mathrlap{ev_1}} \\ Y }

where ${Y}^{I}$ is the cocylinder.

The mapping cocylinder is sometimes denoted ${M}_{f}Y$ or $Nf$.

###### Remark

If we interchange ${\mathrm{ev}}_{0}$ and ${\mathrm{ev}}_{1}$ then we have an upside-down version of a cylinder, sometimes called inverse (or inverted) mapping cocylinder; but usually it is clear just from the context which version is used. They are homotopy equivalent, so usually it does not matter.

### In type theory

In homotopy type theory the mapping cocylinder $\mathrm{Cocyl}\left(f\right)\to Y$ is expressed as

$y:Y⊢\sum _{x\in X}\left(f\left(x\right)=y\right)$y : Y \vdash \sum_{x \in X} (f(x) = y)

being the dependent sum over $x$ of the substitution of $f\left(x\right)$ for ${y}_{1}$ in the dependent identity type $\left({y}_{1}=y\right)$. Equivalently this is the $y$-dependent homotopy fiber of $f$ at $y$

$y:Y⊢\mathrm{hfiber}\left(f,y\right)\phantom{\rule{thinmathspace}{0ex}}.$y : Y \vdash hfiber(f,y) \,.

## Examples

• In the case of topological spaces, the mapping cocylinder is the subspace $\mathrm{Cocyl}\left(f\right)\subset {Y}^{I}×X$ whose elements are pairs $\left(s,x\right)$ such that $s\left(0\right)=f\left(x\right)$.

• In homotopy type theory, cocylinders represent identity types, and the mapping cocylinder represents the dependent type $y:Y⊢\mathrm{hfiber}\left(f,y\right):\mathrm{Type}$. This is used crucially in the definition of equivalence in homotopy type theory.

## References

(This uses the terminology mapping path space.)

Revised on May 16, 2012 15:27:27 by Tim Porter (150.214.204.37)