2.9 Π-types and the function extensionality axiom


Given a type A and a type family B:A𝒰, consider the dependent function type (x:A)B(x). We expect the type f=g of paths from f to g in (x:A)B(x) to be equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to the type of pointwise paths:

(f=g)(x:A(f(x)=B(x)g(x))). (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 continuousPlanetmathPlanetmath homotopy. And from a categoricalPlanetmathPlanetmath perspective, it would say that an isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath in a functor categoryPlanetmathPlanetmath is a natural family of isomorphisms.

Unlike the case in the previous sectionsMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, however, the basic type theoryPlanetmathPlanetmath 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

𝗁𝖺𝗉𝗉𝗅𝗒:(f=g)x:A(f(x)=B(x)g(x)) (2.9.2)

which is easily defined by path inductionMathworldPlanetmath. 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

𝖿𝗎𝗇𝖾𝗑𝗍:(x:A(f(x)=g(x)))(f=g).

This function is also referred to as “function extensionality”. As we did with 𝗉𝖺𝗂𝗋= in §2.6 (http://planetmath.org/26cartesianproducttypes), we can regard 𝖿𝗎𝗇𝖾𝗑𝗍 as an introduction rule for the type f=g. From this point of view, 𝗁𝖺𝗉𝗉𝗅𝗒 is the elimination rule, while the homotopies witnessing 𝖿𝗎𝗇𝖾𝗑𝗍 as quasi-inverse to 𝗁𝖺𝗉𝗉𝗅𝗒 become a propositional computation rule

𝗁𝖺𝗉𝗉𝗅𝗒(𝖿𝗎𝗇𝖾𝗑𝗍(h),x)=h(x)  for h:x:A(f(x)=g(x))

and a propositional uniqueness principle:

p=𝖿𝗎𝗇𝖾𝗑𝗍(x𝗁𝖺𝗉𝗉𝗅𝗒(p,x))  for p:(f=g).

We can also compute the identityPlanetmathPlanetmath, inversesPlanetmathPlanetmath, and composition in Π-types; they are simply given by pointwise operations:.

𝗋𝖾𝖿𝗅f =𝖿𝗎𝗇𝖾𝗑𝗍(x𝗋𝖾𝖿𝗅f(x))
α-1 =𝖿𝗎𝗇𝖾𝗑𝗍(x𝗁𝖺𝗉𝗉𝗅𝗒(α,x)-1)
α\centerdotβ =𝖿𝗎𝗇𝖾𝗑𝗍(x𝗁𝖺𝗉𝗉𝗅𝗒(α,x)\centerdot𝗁𝖺𝗉𝗉𝗅𝗒(β,x)).

The first of these equalities follows from the definition of 𝗁𝖺𝗉𝗉𝗅𝗒, while the second and third are easy path inductions.

Since the non-dependent function type AB is a special case of the dependent function type (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:x1=Xx2, type families A,B:X𝒰, and a function f:A(x1)B(x1), we have

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍AB(p,f) =(x𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍B(p,f(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍A(p-1,x)))) (2.9.4)

where AB denotes abusively the type family X𝒰 defined by

(AB)(x):(A(x)B(x)).

In other words, when we transport a function f:A(x1)B(x1) along a path p:x1=x2, we obtain the function A(x2)B(x2) 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 similarMathworldPlanetmath, but more complicated. Suppose given X and p as before, type families A:X𝒰 and B:(x:X)(A(x)𝒰), and also a dependent function f:(a:A(x1))B(x1,a). Then for a:A(x2), we have

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍ΠA(B)(p,f)(a)=𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍B^((𝗉𝖺𝗂𝗋=(p-1,𝗋𝖾𝖿𝗅p-1*(a)))-1,f(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍A(p-1,a)))

where ΠA(B) and B^ denote respectively the type families

ΠA(B):(xa:A(x)B(x,a)):X𝒰B^:(wB(𝗉𝗋1w,𝗉𝗋2w)):(x:XA(x))𝒰. (2.9.5)

If these formulasMathworldPlanetmathPlanetmath 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𝒰, in §2.2 (http://planetmath.org/22functionsarefunctors) we defined the type of dependent paths over p:x=Xy from u:P(x) to v:P(y) to be p*(u)=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:XU and p:x=Xy, and also f:A(x)B(x) and g:A(y)B(y), we have an equivalence

(p*(f)=g)a:A(x)(p*(f(a))=g(p*(a))).

Moreover, if q:p*(f)=g corresponds under this equivalence to q^, then for a:A(x), the path

𝗁𝖺𝗉𝗉𝗅𝗒(q,p*(a)):(p*(f))(p*(a))=g(p*(a))

is equal to the composite

(p*(f))(p*(a)) =p*(f(p-1*(p*(a)))) (by \eqref{eq:transport-arrow})
=p*(f(a))
=g(p*(a)). (by $\widehat{q}$)
Proof.

By path induction, we may assume p is reflexivityMathworldPlanetmath, 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:XU and B:(x:X)A(x)U and p:x=Xy, and also f:(a:A(x))B(x,a) and g:(a:A(y))B(y,a), we have an equivalence

(p*(f)=g)(a:A(x)𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍B^(𝗉𝖺𝗂𝗋=(p,𝗋𝖾𝖿𝗅p*(a)),f(a))=g(p*(a)))

with 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 Π-types and the function extensionality axiom
\metatable