A --gA[t]--> X|           ^i           ||           |v           |B >-gB[0]---*

The data $(A, B, i)$ is said to be a cofibration ( $i$ like an inclusion $A \rightarrow B$) iff given any homotopy $gA[t]: [0, 1] \times A \rightarrow X$, and a map downstairs $gB[0]: B \rightarrow X$ such that $gB[0] \circ i = gA[t](0)$, we can extend $gB[0]$ into $gB[t]$. We see that this is simply the HEP (homotopy extension property), where we have a homotopy of subspace $A$, and a starting homotopy of $B$, which can be extended to a full homotopy.

§ Lemma: Cofibration is always inclusion (Hatcher)

§ Pushouts

A <-i- P -β-> B

The pushout intuitively glues $B$ to $A$ along $A$'s subspace $P$. For this interpretation, let us say that $P$ is a subspace of $A$ (ie, $i$ is an injection). Then the result of the pushout is a space where we identify $\beta(p) \in B$ with $p \in A$. The pushout in Set is $A \cup B/ \sim$ where we generate an equivalence relation from $i(p) \sim \beta(p)$. In groups, the pushout is amalgamated free product.

-- | HoTT defnf :: C -> Ag :: C -> Binl :: Pushout A  B C f ginr ::  Pushout A B C f gglue :: Π(c: C) inl (f(c)) = inr(g(c))

Suspension:

1 <- A -> 1

Suspension can "add homotopies". Example, S1 = Susp(2).

A --f--> P|       ||i      |i'v       vB -----> B Uf P

We want to show that $P \xrightarrow{i'} B \cup_f X$ is a cofibration if $A \xrightarrow{i} B$ is a cofibration.

Reference: F. Faviona, more on HITs