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\mathrm{:}A\mathrm{\to }B$ is a function. Then for any $x\mathrm{,}y\mathrm{:}A$ there is an operation

$${\mathrm{𝖺𝗉}}_f:(x{=}_{A}y)\to (f(x){=}_{B}f(y)).$$

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

The notation ${\mathrm{𝖺𝗉}}_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:{\prod }_{(x,y:A)}{\prod }_{(p:x=y)}𝒰$ be the type family defined by

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

Then we have

$$d:\equiv \lambda x.{\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}:\prod _{x:A}D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x).$$

By path induction, we obtain ${\mathrm{𝖺𝗉}}_f:{\prod }_{(x,y:A)}{\prod }_{(p:x=y)}(f(x)=g(x))$. The computation rule implies ${\mathrm{𝖺𝗉}}_f({\mathrm{𝗋𝖾𝖿𝗅}}_x)\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}$ for each $x:A$. ∎

Second proof.

By induction, it suffices to assume $p$ is ${\mathrm{𝗋𝖾𝖿𝗅}}_x$. In this case, we may define ${\mathrm{𝖺𝗉}}_f(p):\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}:f(x)=f(x)$. ∎

We will often write ${\mathrm{𝖺𝗉}}_f(p)$ as simply $f\left(p\right)$. 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 $\mathrm{𝖺𝗉}$ behaves functorially, in all the ways that one might expect.

Lemma 2.2.2.

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

1. ${\mathrm{𝖺𝗉}}_f(pq)={\mathrm{𝖺𝗉}}_f(p){\mathrm{𝖺𝗉}}_f(q)$.

2. ${\mathrm{𝖺𝗉}}_f(p^{-1})={\mathrm{𝖺𝗉}}_f{(p)}^{-1}$.

3. ${\mathrm{𝖺𝗉}}_g({\mathrm{𝖺𝗉}}_f(p))={\mathrm{𝖺𝗉}}_{g\circ f}(p)$.

4. ${\mathrm{𝖺𝗉}}_{{\mathrm{𝗂𝖽}}_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\mathrm{:}A\mathrm{\to }B$ is a function. Then for any $x\mathrm{,}y\mathrm{:}A$ there is an operation

$${\mathrm{𝖺𝗉}}_f:(x{=}_{A}y)\to (f(x){=}_{B}f(y)).$$

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

The notation ${\mathrm{𝖺𝗉}}_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:{\prod }_{(x,y:A)}{\prod }_{(p:x=y)}𝒰$ be the type family defined by

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

Then we have

$$d:\equiv \lambda x.{\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}:\prod _{x:A}D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x).$$

By path induction, we obtain ${\mathrm{𝖺𝗉}}_f:{\prod }_{(x,y:A)}{\prod }_{(p:x=y)}(f(x)=g(x))$. The computation rule implies ${\mathrm{𝖺𝗉}}_f({\mathrm{𝗋𝖾𝖿𝗅}}_x)\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}$ for each $x:A$. ∎

Second proof.

By induction, it suffices to assume $p$ is ${\mathrm{𝗋𝖾𝖿𝗅}}_x$. In this case, we may define ${\mathrm{𝖺𝗉}}_f(p):\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}:f(x)=f(x)$. ∎

We will often write ${\mathrm{𝖺𝗉}}_f(p)$ as simply $f\left(p\right)$. 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 $\mathrm{𝖺𝗉}$ behaves functorially, in all the ways that one might expect.

Lemma 2.2.4.

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

1. ${\mathrm{𝖺𝗉}}_f(pq)={\mathrm{𝖺𝗉}}_f(p){\mathrm{𝖺𝗉}}_f(q)$.

2. ${\mathrm{𝖺𝗉}}_f(p^{-1})={\mathrm{𝖺𝗉}}_f{(p)}^{-1}$.

3. ${\mathrm{𝖺𝗉}}_g({\mathrm{𝖺𝗉}}_f(p))={\mathrm{𝖺𝗉}}_{g\circ f}(p)$.

4. ${\mathrm{𝖺𝗉}}_{{\mathrm{𝗂𝖽}}_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