The fact, due to Voevodsky, that univalence implies function extensionality, has always been a bit mysterious to me—the proofs that I have seen have all seemed a bit non-obvious, and I have trouble re-inventing or explaining them.  Moreover, there are questions about how it fits into a general conception of type theory: Why does adding an axiom about one type (the universe) change what is true about another type (functions)? How does this relate to other instances of this phenomenon, such as the fact that a universe is necessary to prove injectivity/disjointness of datatype constructors, or that univalence is necessary to calculate path spaces of higher inductives?  In this post, I will describe a proof that univalence implies function extensionality that is less mysterious to me.  The proof uses many of the same ingredients as the existing proofs, but requires definitional eta rules for both function and product types.  It works for simple function types, and would work for dependent function types if we had the beta-reduction rule for transporting along univalence as a definitional equality.  

The proof

Relative to something like simplicial sets, one of the surprising things about the HoTT axiomatization of ∞-groupoids is that what looks like a statement about the points of a type often will determine what happens at higher dimensions. For example, for product types A * B, the point-level pairing and projection functions determine the path-level structure (a path in a product is a pair of paths), and the path-between-path-level structure (a path between pairs-of-paths is a pair of paths-between-paths), and so on. Function extensionality is another example of the same phenomenon: with univalence, the point-level abstraction and application determine the path-level structure (for any two functions, the type of paths between them is the same as the type of homotopies/pointwise equalities), and the path-between-path structure (a path between homotopies is again given pointwise), and so on.  For simplicity, let’s consider non-dependent functions, and by function extensionality I mean the fact that

funext : {A B : Type} (f g : A → B) → (f == g) == ((x : A) → f x == g x)

where == is the identity type.  See the note at the end on matching the formulation/proof in the book.

funext says that the paths in a function type are (equivalent to) a function type, so there are “λ” and “application” operations on paths in a function type. The “λ” operation, which goes from (x : A) → f x == g x to (f == g), is the direction that is not present in standard intensional type theory. Univalence-implies-funext says that this fact is somehow a consequence of the point-level operations on function types (λ-abstraction and application), together with univalence: we don’t need to put in a new path-level “λ” and “application”; they’re already there.

To see why, it helps to focus not on the identity type x == y, but the total path space

Paths A = Σ ((x,y) : A × A). x == y

One of the consequences of path induction is that there is an equivalence (hence equality) between the total path space of A and A itself:

contract-Paths : Paths A == A

From left-to-right, we can send ((x,y),p) to x. From right-to-left, we can send x to ((x,x),id). One round-trip is definitionally the identity, and the other is the identity by path induction. Then univalence says that this equivalence determines an equality. Intuitively, up to homotopy, having two points connected by a path is the same as just having one point.

contract-Paths helps explain why point-level operations determine path-level operations: all constructions respect equality (by transport/ap), so whatever operations we have on A can be translated, by contract-Paths, to operations on Paths A. For example, define

Homotopies A B = Σ (fg : (A -> B) × (A → B)). (x : A) → fst fg x == snd fg x


Then here is a back-of-the-envelope calculation of function extensionality:

 Paths (A -> B)
== A -> B           [by contract-Paths at A -> B]
== A -> (Paths B)   [by contract-Paths at B,
                        applied in the context (A -> -)]
== Homotopies A B   [this equivalence can be proved using eta]

First, what does this have to do with function extensionality? The first line is the type of pairs ((f : A -> B, g : A -> B),p: f == g). The bottom line is the type of pairs ((f,g),h) where h : (x :A) -> f x == g x. Thus, this calculation says that, when packaged together with their endpoints, the type of pointwise homotopies between functions is the same as the type of paths between functions. I say that it is a “back-of-the-envelope” calculation because we also need to know that the dependency works out correctly, which we will discuss below.

Read from bottom to top (which is the direction of function extensionality that doesn’t exist in raw intensional type theory), this calculation says that a pointwise homotopy can be translated, through A -> B, to a path between functions. So the “λ” for Paths (A -> B), which lets you turn a pointwise homotopy into a path, is really coming from the point-level λ in A -> B, translated along contract-Paths.  The first step, the equivalence between A -> (Paths B) and Homotopies A B can be defined directly, without using univalence, if you have η for function and Σ types (without η you’d need function extensionality to prove it! But with η the composites are definitionally the identity.)—it’s just commuting some Σ’s and Π’s.

What does univalence have to do with this? Without univalence, one can show that A and Paths A are equivalent, but not that they are equal. I am fond of saying that the reason univalence is a sensible principle to add to type theory is that any transport/ap along a use of univalence in a known fibration/function can be reduced; but without function extensionality, this is not actually true. In particular, without univalence or function extensionality, you can’t prove that if A is equivalent to B then X -> A is equivalent to X -> B—that the function type preserves equivalence in its codomain (Lemma 4.9.2 in the book). With univalence (but without funext), an equivalence e : Equiv A B determines a path

ap (\ A' -> (X -> A')) (ua e) : (X -> A) == (X -> B)

and therefore an equivalence between X -> A and X -> B (moreover, the forward direction is post-composition with p, as in the book.). This is exactly the justification for the “applied in context A -> -” part of the above calculation. The -> type is a map out of the universe, and thus, univalence “adds” a new fact about function types that is not present in non-univalent type theory: that -> preserves equivalences. (This is why I’ve changed my mind from an my initial reaction that univalence should be “orthogonal” to function types: the function types in question involve the universe that univalence is asserting something about.) The proofs of UA-implies-funext that I have seen have all used this lemma (Lemma 4.9.2 in the book), but it has always been a bit mysterious to me why it comes up, or how you would think to consider it. For me, at least, the idea of translating operations on A to and from operations on Paths A is a nice way to motivate it.

To finish the proof, we need to check that the above equivalence sends ((f,g),p) to ((f,g),h) for the same (f,g)—i.e. that it commutes with first projection. This can be proved by a path induction, followed by a short calculation; see here.

Finally, to match the formulation of function extensionality in Section 2.9 of the HoTT book, we should also ask for the computation rule

funext-ap= : {A B : Type} {f g : A → B} (α : f == g)
→ coe (funext f g) α == \ x -> ap= α {x}


which says that the “top-to-bottom” direction of the equivalence is the map that one would write by path induction. This can also be proved by a path induction and then a little calculation; see the linked Agda file.

The same proof works for dependent functions, except you’d need the beta-reduction for transporting along univalence as a definitional equality; see
here.

Coproducts

It is also instructive to look at whether the same proof applies to other types. For coproducts, first define the “codes” family as follows:

C : (x y : Either A B) → Type
C (Inl a) (Inl a') = a == a'
C (Inr b) (Inr b') = b == b'
C _ _ = Void


Then we can calculate
Paths (Either A B)
== Either A B                              [contract-Paths at Either A B]
== Either (Paths A) (Paths B)              [contract-Paths at A and B, plus univalence]
== Σ (x:Either A B,y : Either A B). C(x,y) [proved directly]


The equivalence between the third and fourth lines just involves commuting some Σ’s and coproducts, and can be proved without using path induction or univalence. As above, one can check that this commutes with first projection and that the map from top to bottom is what you would expect; see here.

However, the key difference between coproducts and functions, and the reason why we don’t need univalence to prove this theorem, is that one can also prove the equivalence

Either A B == Either (Paths A) (Paths B)


directly, without using univalence. I would explain this difference using polarity. Path induction treats the identity type as a positive/left-invertible type: whenever you have an assumption of Paths A on the left, like

x : Paths A |- c : C(x)


you can immediately switch to proving

x' : A |- c' : C((x',x'),refl)


Coproducts are also positive/left invertible.  A general fact about polarity is that like-polarity connectives play nicely together. In this case, the key point is that when you have Either (Paths A) (Paths B) on the left, you can left-invert (case-analyze) the coproduct, and then left-invert (do path-induction on) the paths—this is what lets you construct the equivalence by hand for coproducts, without using univalence.

In contrast, functions are negative/right invertible.  In the corresponding situation for functions, suppose you try to construct an equivalence between A -> Paths B and A -> B by hand. In this case, you will have A -> Paths B on the left. But functions are not left-invertible, so the path induction that you want to do on is “blocked” by the A -> - connective. From this point of view, I would say that

univalence implies function extensionality because it lets you do path induction under an ->

The Circle

I was wondering whether this proof template helps with higher inductives, but it doesn’t seem to. Here’s how it would look for the circle:

   Paths S1
== S1        [contract-Paths]
== Σ (x:S1,y:S1). C(x,y)

Between the second and third lines, for a fixed x, we need to prove that
Σ(y:S1). C(x,y) is contractible, which is essentially the original proof that the total spaces of the cover is contractible.

Streams

However, it seems like we can use the same proof template for other coinductive types. Suppose we have a coinductively defined type of infinite streams defined by

hd : Stream A -> A
tl : Stream A -> Stream A

with bisimulation defined by

Bisimilar : Stream A -> Stream A -> Type
hd' : Bisimilar s1 s1 -> hd s1 == hd s2
tl' : Bisimilar s1 s2 -> Bisimilar (tl s1) (tl s2)

Then we can calculate as follows:

   Paths (Stream A)
== Stream A         [by contract-Paths]
== Stream (Paths A) [by contact-Paths and univalence]
== Σ (x:S1,y:S1). Bisimilar x y

I haven’t fully checked the equivalence between lines 3 and 4, or that this preserves first projection (I need to update Agda to get the latest treatment of coinduction), but it seems like it should work.