# 2.2 Functions are functors

Now we wish to establish that functions $f:A\to B$ behave functorially on paths. In traditional type theory  , this is equivalently the statement that functions respect equality. Topologically, this corresponds to saying that every function is “continuous”, i.e. preserves paths.

###### Lemma 2.2.1.

Suppose that $f:A\to B$ is a function. Then for any $x,y:A$ there is an operation  $\mathsf{ap}_{f}:(x=_{A}y)\to(f(x)=_{B}f(y)).$

Moreover, for each $x:A$ we have $\mathsf{ap}_{f}(\mathsf{refl}_{x})\equiv\mathsf{refl}_{f(x)}$.

The notation $\mathsf{ap}_{f}$ can be read either as the application of $f$ to a path, or as the action on paths of $f$.

###### First proof.

Let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family defined by

 $D(x,y,p):\!\!\equiv(f(x)=f(y)).$

Then we have

 $d:\!\!\equiv{\lambda}x.\,\mathsf{refl}_{f(x)}:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x}).$

By path induction  , we obtain $\mathsf{ap}_{f}:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(% x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}(f(x)=g(x))$. The computation rule implies $\mathsf{ap}_{f}({\mathsf{refl}_{x}})\equiv\mathsf{refl}_{f(x)}$ for each $x:A$. ∎

###### Second proof.

By induction, it suffices to assume $p$ is $\mathsf{refl}_{x}$. In this case, we may define $\mathsf{ap}_{f}(p):\!\!\equiv\mathsf{refl}_{f(x)}:f(x)=f(x)$. ∎

We note that $\mathsf{ap}$ behaves functorially, in all the ways that one might expect.

###### Lemma 2.2.2.

For functions $f:A\to B$ and $g:B\to C$ and paths $p:x=_{A}y$ and $q:y=_{A}z$, we have:

1. 1.

$\mathsf{ap}_{f}(p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}q)=\mathsf{ap}_{f}(p)\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{f% }(q)$.

2. 2.

$\mathsf{ap}_{f}(\mathord{{p}^{-1}})=\mathord{{\mathsf{ap}_{f}(p)}^{-1}}$.

3. 3.

$\mathsf{ap}_{g}(\mathsf{ap}_{f}(p))=\mathsf{ap}_{g\circ f}(p)$.

4. 4.

$\mathsf{ap}_{\mathsf{id}_{A}}(p)=p$.

###### Proof.

Left to the reader. ∎

Now we wish to establish that functions $f:A\to B$ behave functorially on paths. In traditional type theory, this is equivalently the statement that functions respect equality. Topologically, this corresponds to saying that every function is “continuous”, i.e. preserves paths.

###### Lemma 2.2.3.

Suppose that $f:A\to B$ is a function. Then for any $x,y:A$ there is an operation

 $\mathsf{ap}_{f}:(x=_{A}y)\to(f(x)=_{B}f(y)).$

Moreover, for each $x:A$ we have $\mathsf{ap}_{f}(\mathsf{refl}_{x})\equiv\mathsf{refl}_{f(x)}$.

The notation $\mathsf{ap}_{f}$ can be read either as the application of $f$ to a path, or as the action on paths of $f$.

###### First proof.

Let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family defined by

 $D(x,y,p):\!\!\equiv(f(x)=f(y)).$

Then we have

 $d:\!\!\equiv{\lambda}x.\,\mathsf{refl}_{f(x)}:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x}).$

By path induction, we obtain $\mathsf{ap}_{f}:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(% x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}(f(x)=g(x))$. The computation rule implies $\mathsf{ap}_{f}({\mathsf{refl}_{x}})\equiv\mathsf{refl}_{f(x)}$ for each $x:A$. ∎

###### Second proof.

By induction, it suffices to assume $p$ is $\mathsf{refl}_{x}$. In this case, we may define $\mathsf{ap}_{f}(p):\!\!\equiv\mathsf{refl}_{f(x)}:f(x)=f(x)$. ∎

We will often write $\mathsf{ap}_{f}(p)$ as simply ${f}\mathopen{}\left({p}\right)\mathclose{}$. This is strictly speaking ambiguous, but generally no confusion arises. It matches the common convention in category theory of using the same symbol for the application of a functor to objects and to morphisms.

We note that $\mathsf{ap}$ behaves functorially, in all the ways that one might expect.

###### Lemma 2.2.4.

For functions $f:A\to B$ and $g:B\to C$ and paths $p:x=_{A}y$ and $q:y=_{A}z$, we have:

1. 1.

$\mathsf{ap}_{f}(p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}q)=\mathsf{ap}_{f}(p)\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{f% }(q)$.

2. 2.

$\mathsf{ap}_{f}(\mathord{{p}^{-1}})=\mathord{{\mathsf{ap}_{f}(p)}^{-1}}$.

3. 3.

$\mathsf{ap}_{g}(\mathsf{ap}_{f}(p))=\mathsf{ap}_{g\circ f}(p)$.

4. 4.

$\mathsf{ap}_{\mathsf{id}_{A}}(p)=p$.

###### Proof.

Left to the reader. ∎

As was the case for the equalities in Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmlem3), those in Lemma 2.2.2 (http://planetmath.org/22functionsarefunctors#Thmlem2) are themselves paths, which satisfy their own coherence laws (which can be proved in the same way), and so on.

Title 2.2 Functions are functors
\metatable