A Universe of Sorts

§ Cofibration

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.

A <-i- P -β-> B

The pushout intuitively glues

B

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 defn
f :: C -> A
g :: C -> B
inl :: Pushout A  B C f g
inr ::  Pushout A B C f g
glue :: Π(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       v
B -----> 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