It contains the notion of homotopy pullback and pushout, fibers and cofibers, kernels and cokernels. This is what is usually called elementary homotopy theory.

$$\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 (Cospan). The two maps $f,g$ with the same codomain $C$ are called cospan: $$ A \mapright{f} C \mapleft{g} B. $$

Definition (Homotopy Pullback). The homotopy pullback or homotopy limit (denoted as $\mathrm{holim}$) of the cospan diagram is the subspace of $A \times B \times C^I$ defined as $$ \mathrm{holim}(A \rightarrow C \leftarrow B) \\ = \{ (x,y,h) : \Sigma_A\Sigma_B C^I | h(0)=f(x), h(1)=g(y) \} $$

pullback (A B C:U) (f: A -> C) (g: B -> C): U = (a: A) * (b: B) * Path C (f a) (g b)

In other words pullback of cospan together with the projection maps $pb_{1,2,3}$ making the diagram

$$ \begin{array}{ccc} A \times^{h}_{C} B & \mapright{\mathbf{pb_2}} & B \\ \mapdown{\mathbf{pb_1}} & \mapdiagl{\mathbf{pb_3}} & \mapdown{\mathbf{g}} \\ A & \mapright{\mathbf{f}} & C \\ \end{array} $$

commute up to homotopy $H(x,y,h,t) = h(t)$.

Definition (Homotopy Pullback Square). A homotopy pullback or cospan is called a homotopy pullback square if there exists a homotopy equivalence $\phi : Z \rightarrow A \times_C^h B$ satisfying $z_1 : Z \rightarrow A = pb_1 \circ \phi$ and $z_2: Z \rightarrow B = pb_2 \circ \phi$. Map $\phi$ is called induced map.

$$ \begin{array}{ccc} X \times^{h}_{C} Y & \mapright{\mathbf{pb_2}} & B \\ \mapdown{\mathbf{pb_1}} & \square_{(Z,z_1,z_2)} & \mapdown{\mathbf{g}} \\ A & \mapright{\mathbf{f}} & C \\ \end{array} $$
pullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B): U = (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z)) * isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)


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) ]


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


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