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)

From a traditional perspective, this would say that two functions which are equal at each point are equal as functions. From a topological perspective, it would say that a path in a function space is the same as a continuous homotopy. And from a categorical perspective, it would say that an isomorphism in a functor category is a natural family of isomorphisms.

Unlike the case in the previous sections, however, the basic type theory presented in http://planetmath.org/node/87533Chapter 1 is insufficient to prove (2.9.1). All we can say is that there is a certain function

$\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
\metatable

2.9 Π<math id="m1" class="ltx_Math" alttext="\Pi" display="inline"><mi mathvariant="normal">Π</mi></math>-types and the function extensionality axiom

Axiom 2.9.3 (Function extensionality).

Lemma 2.9.6.

Proof.

Lemma 2.9.7.

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