# 2.9 $\Pi$-types and the function extensionality axiom

Given a type $A$ and a type family $B:A\to\mathcal{U}$, consider the dependent function type $\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)}}}B(x)$. We expect the type $f=g$ of paths from $f$ to $g$ in $\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)}}}B(x)$ to be equivalent      to the type of pointwise paths:

 $(f=g)\;\simeq\;\Bigl{(}\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)}}}(f(x)=_{B(x)}g(x))\Bigr{)}.$ (2.9.1)
 $\mathsf{happly}:(f=g)\to\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)}}}(f(x)=_{B(x)}g(x))$ (2.9.2)

which is easily defined by path induction  . For the moment, therefore, we will assume:

###### Axiom 2.9.3 (Function extensionality).

For any $A$, $B$, $f$, and $g$, the function (2.9.2) is an equivalence.

We will see in later chapters that this axiom follows both from univalence (see §2.10 (http://planetmath.org/210universesandtheunivalenceaxiom),§4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality)) and from an interval type (see §6.3 (http://planetmath.org/63theinterval)).

In particular, Axiom 2.9.3 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmaxiom1) implies that (2.9.2) has a quasi-inverse

 $\mathsf{funext}:\Bigl{(}\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)}}}(f(x)=g(x))\Bigr{)}\to{(f=g)}.$

This function is also referred to as “function extensionality”. As we did with $\mathsf{pair}^{\mathord{=}}$ in §2.6 (http://planetmath.org/26cartesianproducttypes), we can regard $\mathsf{funext}$ as an introduction rule for the type $f=g$. From this point of view, $\mathsf{happly}$ is the elimination rule, while the homotopies witnessing $\mathsf{funext}$ as quasi-inverse to $\mathsf{happly}$ become a propositional computation rule

 $\mathsf{happly}({\mathsf{funext}{(h)}},x)=h(x)\qquad\text{for }h:\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)}}}(f(x)=g(x))$

and a propositional uniqueness principle:

 $p=\mathsf{funext}(x\mapsto\mathsf{happly}(p,{x}))\qquad\text{for }p:(f=g).$

We can also compute the identity  , inverses  , and composition in $\Pi$-types; they are simply given by pointwise operations:.

 $\displaystyle\mathsf{refl}_{f}$ $\displaystyle=\mathsf{funext}(x\mapsto\mathsf{refl}_{f(x)})$ $\displaystyle\mathord{{\alpha}^{-1}}$ $\displaystyle=\mathsf{funext}(x\mapsto\mathord{{\mathsf{happly}(\alpha,x)}^{-1% }})$ $\displaystyle{\alpha}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\beta$ $\displaystyle=\mathsf{funext}(x\mapsto{\mathsf{happly}({\alpha},x)\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{% happly}({\beta},x)}).$

The first of these equalities follows from the definition of $\mathsf{happly}$, while the second and third are easy path inductions.

Since the non-dependent function type $A\to B$ is a special case of the dependent function type $\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)}}}B(x)$ when $B$ is independent of $x$, everything we have said above applies in non-dependent cases as well. The rules for transport, however, are somewhat simpler in the non-dependent case. Given a type $X$, a path $p:x_{1}=_{X}x_{2}$, type families $A,B:X\to\mathcal{U}$, and a function $f:A(x_{1})\to B(x_{1})$, we have

 $\displaystyle\mathsf{transport}^{A\to B}(p,f)$ $\displaystyle=\Big{(}x\mapsto\mathsf{transport}^{B}(p,f(\mathsf{transport}^{A}% (\mathord{{p}^{-1}},x)))\Big{)}$ (2.9.4)

where $A\to B$ denotes abusively the type family $X\to\mathcal{U}$ defined by

 $(A\to B)(x):\!\!\equiv(A(x)\to B(x)).$

In other words, when we transport a function $f:A(x_{1})\to B(x_{1})$ along a path $p:x_{1}=x_{2}$, we obtain the function $A(x_{2})\to B(x_{2})$ which transports its argument backwards along $p$ (in the type family $A$), applies $f$, and then transports the result forwards along $p$ (in the type family $B$). This can be proven easily by path induction.

Transporting dependent functions is similar  , but more complicated. Suppose given $X$ and $p$ as before, type families $A:X\to\mathcal{U}$ and $B:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:% X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}(A(x)\to\mathcal{U})$, and also a dependent function $f:\mathchoice{\prod_{a:A(x_{1})}\,}{\mathchoice{{\textstyle\prod_{(a:A(x_{1}))% }}}{\prod_{(a:A(x_{1}))}}{\prod_{(a:A(x_{1}))}}{\prod_{(a:A(x_{1}))}}}{% \mathchoice{{\textstyle\prod_{(a:A(x_{1}))}}}{\prod_{(a:A(x_{1}))}}{\prod_{(a:% A(x_{1}))}}{\prod_{(a:A(x_{1}))}}}{\mathchoice{{\textstyle\prod_{(a:A(x_{1}))}% }}{\prod_{(a:A(x_{1}))}}{\prod_{(a:A(x_{1}))}}{\prod_{(a:A(x_{1}))}}}B(x_{1},a)$. Then for $a:A(x_{2})$, we have

 $\mathsf{transport}^{\Pi_{A}(B)}(p,f)(a)=\mathsf{transport}^{\widehat{B}}\Big{(% }\mathord{{(\mathsf{pair}^{\mathord{=}}(\mathord{{p}^{-1}},\mathsf{refl}_{{% \mathord{{p}^{-1}}}_{*}\mathopen{}\left({a}\right)\mathclose{}}))}^{-1}},\,f(% \mathsf{transport}^{A}(\mathord{{p}^{-1}},a))\Big{)}$

where $\Pi_{A}(B)$ and $\widehat{B}$ denote respectively the type families

 $\begin{array}[]{rclcl}\Pi_{A}(B)&:\!\!\equiv&\big{(}x\mapsto\mathchoice{\prod_% {a:A(x)}\,}{\mathchoice{{\textstyle\prod_{(a:A(x))}}}{\prod_{(a:A(x))}}{\prod_% {(a:A(x))}}{\prod_{(a:A(x))}}}{\mathchoice{{\textstyle\prod_{(a:A(x))}}}{\prod% _{(a:A(x))}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}}{\mathchoice{{\textstyle\prod% _{(a:A(x))}}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}}B(x,a)\big% {)}&:&X\to\mathcal{U}\\ \widehat{B}&:\!\!\equiv&\big{(}w\mapsto B(\mathsf{pr}_{1}w,\mathsf{pr}_{2}w)% \big{)}&:&\big{(}\mathchoice{\sum_{x:X}\,}{\mathchoice{{\textstyle\sum_{(x:X)}% }}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:% X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{% (x:X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}A(x)\big{)}\to\mathcal{U}.% \end{array}$ (2.9.5)

If these formulas   look a bit intimidating, don’t worry about the details. The basic idea is just the same as for the non-dependent function type: we transport the argument backwards, apply the function, and then transport the result forwards again.

Now recall that for a general type family $P:X\to\mathcal{U}$, in §2.2 (http://planetmath.org/22functionsarefunctors) we defined the type of dependent paths over $p:x=_{X}y$ from $u:P(x)$ to $v:P(y)$ to be ${p}_{*}\mathopen{}\left({u}\right)\mathclose{}=_{P(y)}v$. When $P$ is a family of function types, there is an equivalent way to represent this which is often more convenient.

###### Lemma 2.9.6.

Given type families $A,B:X\to\mathcal{U}$ and $p:x=_{X}y$, and also $f:A(x)\to B(x)$ and $g:A(y)\to B(y)$, we have an equivalence

 $\big{(}{p}_{*}\mathopen{}\left({f}\right)\mathclose{}={g}\big{)}\;\simeq\;% \mathchoice{\prod_{a:A(x)}\,}{\mathchoice{{\textstyle\prod_{(a:A(x))}}}{\prod_% {(a:A(x))}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}}{\mathchoice{{\textstyle\prod_% {(a:A(x))}}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}}{% \mathchoice{{\textstyle\prod_{(a:A(x))}}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}{% \prod_{(a:A(x))}}}({p}_{*}\mathopen{}\left({f(a)}\right)\mathclose{}=g({p}_{*}% \mathopen{}\left({a}\right)\mathclose{})).$

Moreover, if $q:{p}_{*}\mathopen{}\left({f}\right)\mathclose{}={g}$ corresponds under this equivalence to $\widehat{q}$, then for $a:A(x)$, the path

 $\mathsf{happly}(q,{p}_{*}\mathopen{}\left({a}\right)\mathclose{}):({p}_{*}% \mathopen{}\left({f}\right)\mathclose{})({p}_{*}\mathopen{}\left({a}\right)% \mathclose{})=g({p}_{*}\mathopen{}\left({a}\right)\mathclose{})$

is equal to the composite

 $\displaystyle({p}_{*}\mathopen{}\left({f}\right)\mathclose{})({p}_{*}\mathopen% {}\left({a}\right)\mathclose{})$ $\displaystyle={p}_{*}\mathopen{}\left({f({\mathord{{p}^{-1}}}_{*}\mathopen{}% \left({{p}_{*}\mathopen{}\left({a}\right)\mathclose{}}\right)\mathclose{})}% \right)\mathclose{}{}$ (by \eqref{eq:transport-arrow}) $\displaystyle={p}_{*}\mathopen{}\left({f(a)}\right)\mathclose{}$ $\displaystyle=g({p}_{*}\mathopen{}\left({a}\right)\mathclose{}).{}$ (by $\widehat{q}$)
###### Proof.

By path induction, we may assume $p$ is reflexivity  , in which case the desired equivalence reduces to function extensionality. The second statement then follows by the computation rule for function extensionality. ∎

As usual, the case of dependent functions is similar, but more complicated.

###### Lemma 2.9.7.

Given type families $A:X\to\mathcal{U}$ and $B:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:% X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x)\to\mathcal{U}$ and $p:x=_{X}y$, and also $f:\mathchoice{\prod_{a:A(x)}\,}{\mathchoice{{\textstyle\prod_{(a:A(x))}}}{% \prod_{(a:A(x))}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}}{\mathchoice{{\textstyle% \prod_{(a:A(x))}}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}}{% \mathchoice{{\textstyle\prod_{(a:A(x))}}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}{% \prod_{(a:A(x))}}}B(x,a)$ and $g:\mathchoice{\prod_{a:A(y)}\,}{\mathchoice{{\textstyle\prod_{(a:A(y))}}}{% \prod_{(a:A(y))}}{\prod_{(a:A(y))}}{\prod_{(a:A(y))}}}{\mathchoice{{\textstyle% \prod_{(a:A(y))}}}{\prod_{(a:A(y))}}{\prod_{(a:A(y))}}{\prod_{(a:A(y))}}}{% \mathchoice{{\textstyle\prod_{(a:A(y))}}}{\prod_{(a:A(y))}}{\prod_{(a:A(y))}}{% \prod_{(a:A(y))}}}B(y,a)$, we have an equivalence

 $\big{(}{p}_{*}\mathopen{}\left({f}\right)\mathclose{}={g}\big{)}\;\simeq\;% \Bigl{(}\mathchoice{\prod_{a:A(x)}\,}{\mathchoice{{\textstyle\prod_{(a:A(x))}}% }{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}}{\mathchoice{{% \textstyle\prod_{(a:A(x))}}}{\prod_{(a:A(x))}}{\prod_{(a:A(x))}}{\prod_{(a:A(x% ))}}}{\mathchoice{{\textstyle\prod_{(a:A(x))}}}{\prod_{(a:A(x))}}{\prod_{(a:A(% x))}}{\prod_{(a:A(x))}}}\mathsf{transport}^{\widehat{B}}(\mathsf{pair}^{% \mathord{=}}(p,\mathsf{refl}_{{p}_{*}\mathopen{}\left({a}\right)\mathclose{}})% ,f(a))=g({p}_{*}\mathopen{}\left({a}\right)\mathclose{})\Bigr{)}$

with $\widehat{B}$ as in (2.9.5).

We leave it to the reader to prove this and to formulate a suitable computation rule.

Title 2.9 $\Pi$-types and the function extensionality axiom