2.7 -- Functoriality of ap under $\sum$-types

(I won't start with the introduction of HOTT, as it very well explained here http://homotopytypetheory.org/book/ . Instead, I'll present what was lately on my scratchpad.)

2.7 -- Functoriality of ap under $\sum$-types

The statement of this theorem and its proof was left to the reader and it gave me some trouble to state it right.

First, let's recall what happens for a cartesian product. To build a function $f : A \times B \rightarrow A' \times B'$ we can join two functions $g : A \rightarrow A'$ and $h : B \rightarrow B'$ in the following way : for every $x \in A \times B$ we set $f(x) :\equiv (g(pr_1(x)), h(pr_2(y)))$. What is done is a split of $x$ into its components on which we apply separately $g$ and $h$.

To extend this definition to $\sum$-type, given two type families $P : A \rightarrow \mathcal{U}$ and $P' : A' \rightarrow \mathcal{U}'$, we want to build a function $f : \sum_{x : A} P(x) \rightarrow \sum_{x' : A'} P'(x')$ by joining two functions applied component-wise. The first function is straightforward to type : we reuse $g : A \rightarrow A'$. But, for the second function we can't take one unrelated to $g$. The reason for this lies in the result of $f$, as it will make a dependent pair of the form $( g(pr_1(x)), h(pr_2(x)))$ for it to inhabit the type $\sum_{x':A'} P'(x')$ we must have the typing $h(pr_2(x)) : P'(g(pr_1(x)))$, Therefore, the type of $h$ must depend on $g(pr_1(x))$! Then to get this dependency, the simplest approach is to have $h(a,a') : P(a) \rightarrow P'(a')$ but we could have taken $h(a,g) : P(a) \rightarrow P'(g(a))$. I think the first type is more general, but the second one makes a stronger theorem because it's easier to build this kind of $h$ as it doesn't need to provide functions when $a' \neq g(a)$.

Our definition of $f$ is then like this : take $g : A \rightarrow A'$ and $h : \prod_{a : A} P(a) \rightarrow P'(g(a))$, we can then define
\[
f(x) :\equiv (g(pr_1(x)), h(pr_1(x), pr_2(x)))
\]
(Note here that I'm unsure of the type of $h$, one could argue that $h : \prod_{g : A' \rightarrow A} \prod_{a : A} P(a) \rightarrow P'(g(a))$ would be clearer as it removes the explicit dependency of $h$ over $g$. But, for me, it means that such $h$ is infinitely harder to build because it needs to be defined for every possible $g$!)

It remains to state the equivalent of theorem 2.6.5 in this context. Recall that the equality $q : pr_2(x) = pr_2(y)$ needs to be transported in the right space as $pr_2(x) : P(pr_1(x))$ and $pr_2(y) : P(pr_1(y))$. We can set it to happen in $P(pr_1(y))$ but we have to transport $pr_2(x)$ there using $transport^P(p,pr_2(x)) = p_*(pr_2(x))$ where $p : pr_1(x) = pr_1(y)$.

Theorem 2.7.5 : In the above situation, given $x, y : \sum_{a:A} P(a)$ and $p : pr_1(x) = pr_1(y)$ and $q : p_*(pr_2(x)) = pr_2(y)$, we have
\[
f(pair^=(p,q)) =_{(f(x)=f(y))} pair^=(g(p), h(pr_1(y), q))
\]

Proof.By induction we can assume that $x \equiv (a,b)$ and $y \equiv (a',b')$. Then $p : a = a'$ and we can assume that $p \equiv refl_a$ by path induction. We now have $p_* \equiv id_{P(a)}$ and $q : b = b'$. We can assume that $q \equiv refl_b$ by path induction. At this point the left member of the equality is
\[
f(pair^=(refl_a, refl_b)) \equiv f(refl_{(a,b)} \equiv refl_{f(a,b)}
\]
and the right member is
\[
pair^=( g(refl_a), h(a, refl_b) ) \equiv pair^=(refl_{g(a)}, refl_{h(a, b)})  \equiv refl_{(g(a), h(a,b))} \equiv refl_{f(a,b)}
\]
So we now need a proof of the theorem in this case, but we already have one : $refl_{refl_{f(a,b)}}$.