Mapping Cylinders

As in topology, the mapping cylinder of a function f : A → B is a way to replace it with an equivalent cofibration (dually to how hfiber replaces it with an equivalent fibration). We can't talk *internally* in type theory about cofibrations, but we can say metatheoretically what they are: functions with the isomorphism extension property. So while we can't literally say "let f be a cofibration" we can do a mostly equivalent thing and say "let f be a map and consider its mapping cylinder". Replacing a map by a cofibration can be useful because it allows us to make more equalities true definitionally.

Definitions

We define the mapping cylinder as the pushout of f and an identity map. Peter Lumsdaine has given a definition of HIT mapping cylinders that are dependent on the codomain, so that the second factor is not just an equivalence but a trivial fibration. However, at the moment we don't have a need for that.

Rather than adjointifying, we give all parts of the equivalence explicitly, so we can be sure of retaining the computational behavior of eissect and eisretr. However, it's easier to prove eisadj on the other side, so we reverse the equivalence first.

The original map f factors definitionally through Cyl f.

Sometimes we have to specify the map explicitly.

Functoriality

The benefit of passing to the mapping cylinder is that it makes a square commute definitionally.

The other square also commutes, though not definitionally.

Here we need eissect pr_cyl (cyl a) to compute.

Coequalizers

A particularly useful application is to replace a map of coequalizers with one where both squares commute definitionally.