HoTT Notes 11

Morphism

We define the type $A$ morphism from $f$ to $g$ over $X$ as:

$$ hom_X(f, g) := Σ_{(h:A → B)} f \sim g ∘ h $$

$$ (h, H) : hom_X(f, g) $$

We define composition of morphisms as:

$$ \begin{align} (k, K) ∘ (h, H) & : hom_X(f, i) \\ (k, K) ∘ (h, H) & := (k ∘ h, H ⋅ (K ⋅ h)) \end{align} $$

Universal property of the image

We say i satisfies the universal property of the image of f if:

$$ -∘(q,H) : hom_X(i, m) → hom_X(f, m) $$

is an equivalence for every imbedding $m : B ↪ X$.

For any $f : A → X$ and $m : B ↪ X$, $hom_X(f, m)$ is a proposition.

Image

The image of a map $f : A → X$ is a type which contains all $X$ which $f$ can map to, paired with the evidence that its preimage exists:

$$ \text{im}(f) := Σ_{(x:X)}||fib_f(x)|| $$

$\text{im}(f)$ is an embedding.

We can drop the evidence to get the "proof-irreverent" image part:

$$ \begin{align} i_f &: \text{im}(f) → X \\ i_f &:= proj_1 \end{align} $$

We can provide an element of $A$ and get the corresponding image of $f$:

$$ \begin{align} q_f &: A → \text{im}(f) \\ q_f &:= (f(x), 𝜂(x , refl_{f(x)})) \end{align} $$

Where $𝜂$ is the unit truncation function.

And $f \sim i_f ◦ q_f$, we call this homotopy $I_f$.