PUSHOUT

$$ \def\mapright#1{\xrightarrow{{#1}}} \def\mapleft#1{\xleftarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$

Definition (Span). The two maps $f,g$ with the same domain $C$ are called span: $$ A \mapleft{f} C \mapright{g} B. $$

Definition (Homotopy Pushout). The homotopy pushout or homotopy colimit (denoted as $\mathrm{hocolim}$) of the span diagram: $$ \mathrm{hocolim}(A \mapleft{f} C \mapright{g} B) = A \sqcup B \sqcup C \times I\ / \sim, $$ where $\sim$ is an equivalence relation $f(c) \sim (w,0)$ and $g(w) \sim (w,1)$ for $w \in C$. If $C$ is a based space with basepoint $w_0$, we add the relation $(w_0,t) ~ (w_1,s)$ for all $s,t \in I$.

data pushout (A B C: U) (f: C -> A) (g: C -> B)
   = po1 (_: A)
   | po2 (_: B)
   | po3 (c: C) <i> [ (i = 0) -> po1 (f c) ,
                      (i = 1) -> po2 (g c) ]

EXAMPLES

Definition (Homotopy Fibers).

hofiber (A B: U) (f: A -> B) (y: B): U
  = pullback A unit B f (\(x: unit) -> y)

Definition (Fiber Pullback).

fiberPullback (A B: U) (f: A -> B) (y: B)
  : pullbackSq (hofiber A B f y)

Definition (Homotopy Cofiber).

cofiber (A B: U) (f: B -> A): U
  = pushout A unit B f (\(x: B) -> tt)

Defintion (Kernel).

kernel (A B: U) (f: A -> B): U
  = pullback A A B f f

Definition (Cokernel).

cokernel (A B: U) (f: B -> A): U
  = pushout A A B f f

LITERATURE

[1]. Brian Munson and Ismar Volić. Cubical Homotopy Theory