2.9 -types and the function extensionality axiom
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
which is easily defined by path induction. For the moment, therefore, we will assume:
Axiom 2.9.3 (Function extensionality).
For any , , , and , 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)).
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 . From this point of view, is the elimination rule, while the homotopies witnessing as quasi-inverse to become a propositional computation rule
and a propositional uniqueness principle:
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 is a special case of the dependent function type when is independent of , 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 , a path , type families , and a function , we have
where denotes abusively the type family defined by
In other words, when we transport a function along a path , we obtain the function which transports its argument backwards along (in the type family ), applies , and then transports the result forwards along (in the type family ). This can be proven easily by path induction.
Transporting dependent functions is similar, but more complicated. Suppose given and as before, type families and , and also a dependent function . Then for , we have
where and denote respectively the type families
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 , in §2.2 (http://planetmath.org/22functionsarefunctors) we defined the type of dependent paths over from to to be . When is a family of function types, there is an equivalent way to represent this which is often more convenient.
Given type families and , and also and , we have an equivalence
Moreover, if corresponds under this equivalence to , then for , the path
is equal to the composite
By path induction, we may assume 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.
Given type families and and , and also and , we have an equivalence
with 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|