The fact that the univalence axiom implies function extensionality is one of the most well-known results of Homotopy Type Theory.

The original proof by Voevodsky has been simplified over time, and eventually assumed the distilled form presented in the HoTT book.

All the various versions of the proof have roughly the same outline. They first show that the weak function extensionality principle (WFEP) follows from univalence, and then prove that this is enough to establish function extensionality.

Following the book, WFEP is the statement that contractible types are closed under \(Π\), i.e.:

WFEP : ∀ i j → Set _
WFEP i j = {A : Set i}{B : A → Set j}
         → ((x : A) → contr (B x))
         → contr ((x : A) → B x)

WFEP implies function extensionality

Showing that WFEP implies function extensionality does not need univalence, and is quite straightforward. First, we define what we mean by function extensionality:

Funext : ∀ i j → Set _
Funext i j = {A : Set i}{B : A → Set j}
           → {f g : (x : A) → B x}
           → ((x : A) → f x ≡ g x)
           → f ≡ g

Now we want to show the following:

wfep-to-funext : ∀ {i}{j} → WFEP i j → Funext i j
wfep-to-funext {i}{j} wfep {A}{B}{f}{g} h = p
  where

To prove that \(f\) and \(g\) are equal, we show that they both have values in the following dependent type, which we can think of as a subtype of \(B(x)\) for all \(x : A\):

    C : A → Set j
    C x = Σ (B x) λ y → f x ≡ y

We denote by \(f'\) and \(g'\) the range restrictions of \(f\) and \(g\) to \(C\):

    f' g' : (x : A) → C x
    f' x = (f x , refl)
    g' x = (g x , h x)

where we made use of the homotopy \(h\) between \(f\) and \(g\) to show that \(g\) has values in \(C\). Now, \(C(x)\) is a singleton for all \(x : A\), so, by WFEP, \(f'\) and \(g'\) have the same contractible type, hence they are equal:

    p' : f' ≡ g'
    p' = contr⇒prop (wfep (λ x → singl-contr (f x))) f' g'

The fact that \(f\) and \(g\) are equal then follows immediately by applying the first projection and (implicitly) using \(η\) conversion for \(Π\)-types:

    p : f ≡ g
    p = ap (λ u x → proj₁ (u x)) p'

In the book, the strong version of extensionality, i.e.

StrongFunext : ∀ i j → Set _
StrongFunext i j = {A : Set i}{B : A → Set j}
                 → {f g : (x : A) → B x}
                 → ((x : A) → f x ≡ g x)
                 ≅ (f ≡ g)

is obtained directly using a more sophisticated, but very similar argument.

Proving WFEP

Now we turn to proving WFEP itself. Most of the proofs I know use the fact that univalence implies a certain congruence rule for function-types, i.e. if \(B\) and \(B'\) are equivalent types, then \(A → B\) and \(A → B'\) are also equivalent, and furthermore the equivalence is given by precomposing with the equivalence between \(B\) and \(B'\).

However, if we have η conversion for record types, there is a much simpler way to obtain WFEP from univalence.

The idea is as follows: since \(B(x)\) is contractible for all \(x : A\), univalence implies that \(B(x) ≡ ⊤\), so the contractibility of \((x : A) → B(x)\) is a consequence of the contractibility of \(A → ⊤\), which is itself an immediate consequence of the definitional \(η\) rule for \(⊤\):

record ⊤ : Set j where
  constructor tt

⊤-contr : contr ⊤
⊤-contr = tt , λ { tt → refl }

contr-exp-⊤ : ∀ {i}{A : Set i} → contr (A → ⊤)
contr-exp-⊤ = (λ _ → tt) , (λ f → refl)

However, the proof sketch above is missing a crucial step: even though \(B(x)\) is pointwise equal to \(⊤\), in order to substitute \(⊤\) for \(B(x)\) in the \(Π\)-type, we need to show that \(B ≡ λ \_ → ⊤\), but we’re not allowed to use function extensionality, yet!

Fortunately, we only need a very special case of function extensionality. So the trick here is to apply the argument to this special case first, and then use it to prove the general result.

First we prove WFEP for non-dependent \(Π\)-types, by formalising the above proof sketch.

nondep-wfep : ∀ {i j}{A : Set i}{B : Set j}
            → contr B
            → contr (A → B)
nondep-wfep {A = A}{B = B} hB = subst contr p contr-exp-⊤
  where
    p : (A → ⊤) ≡ (A → B)
    p = ap (λ X → A → X) (unique-contr ⊤-contr hB)

Since \(B\) is non-dependent in this case, the proof goes through without function extensionality, so we don’t get stuck in an infinite regression: two iterations are enough!

Now we can prove the special case of function extensionality that we will need for the proof of full WFEP:

funext' : ∀ {i j}{A : Set i}{B : Set j}
        → (f : A → B)(b : B)(h : (x : A) → b ≡ f x)
        → (λ _ → b) ≡ f
funext' f b h =
  ap (λ u x → proj₁ (u x))
       (contr⇒prop (nondep-wfep (singl-contr b))
                    (λ _ → (b , refl))
                    (λ x → f x , h x))

Same proof as for wfep-to-funext, only written more succinctly.

Finally, we are ready to prove WFEP:

wfep : ∀ {i j} → WFEP i j
wfep {i}{j}{A}{B} hB = subst contr p contr-exp-⊤
  where
    p₀ : (λ _ → ⊤) ≡ B
    p₀ = funext' B ⊤ (λ x → unique-contr ⊤-contr (hB x))

    p : (A → ⊤ {j}) ≡ ((x : A) → B x)
    p = ap (λ Z → (x : A) → Z x) p₀

By putting it all together we get function extensionality:

funext : ∀ {i j} → Funext i j
funext = wfep-to-funext wfep

Avoiding η for records

This proof can also be modified to work in a theory where \(⊤\) does not have definitional η conversion.

The only point where η is used is in the proof of contr-exp-⊤ above. So let’s define a version of \(⊤\) without η, and prove contr-exp-⊤ for it.

data ⊤ : Set j where
  tt : ⊤

⊤-contr : contr ⊤
⊤-contr = tt , λ { tt → refl }

We begin by defining the automorphism \(k\) of \(⊤\) which maps everything to \(\mathsf{tt}\). Clearly, \(k\) is going to be the identity, but we can’t prove that until we have function extensionality.

k : ⊤ → ⊤
k _ = tt

k-we : weak-equiv k
k-we tt = Σ-contr ⊤-contr (λ _ → h↑ ⊤-contr tt tt)

Now we apply the argument sketched above, based on the fact that univalence implies congruence rules for function types. We extract an equality out of \(k\), and then transport it to the exponentials:

k-eq : ⊤ ≡ ⊤
k-eq = ≈⇒≡ (k , k-we)

k-exp-eq : ∀ {i}(A : Set i) → (A → ⊤) ≡ (A → ⊤)
k-exp-eq A = ap (λ X → A → X) k-eq

If we were working in a theory with computational univalence, coercion along k-exp-eq would reduce to precomposition with \(k\). In any case, we can manually show that this is the case propositionally by using path induction and the computational rule for ≈⇒≡:

ap-comp : ∀ {i k}{A : Set i}{X X' : Set k}
        → (p : X ≡ X')
        → (f : A → X)
        → coerce (ap (λ X → A → X) p) f
        ≡ coerce p ∘ f
ap-comp refl f = refl

k-exp-eq-comp' : ∀ {i}{A : Set i}(f : A → ⊤)
               → coerce (k-exp-eq A) f
               ≡ λ _ → tt
k-exp-eq-comp' f = ap-comp k-eq f
                 · ap (λ c → c ∘ f)
                      (uni-coherence (k , k-we))

Now it’s easy to conclude that \(A → ⊤\) is a mere proposition (hence contractible): given functions \(f g : A → ⊤\), precomposing them with \(k\) makes them both equal to \(λ \_ → \mathsf{tt}\). Since precomposing with \(k\) is an equivalence by the computational rule above, \(f\) must be equal to \(g\).

prop-exp-⊤ : ∀ {i}{A : Set i} → prop (A → ⊤)
prop-exp-⊤ {i}{A} f g = ap proj₁
  ( contr⇒prop (coerce-equiv (k-exp-eq A) (λ _ → tt))
      (f , k-exp-eq-comp' f)
      (g , k-exp-eq-comp' g) )

contr-exp-⊤ : ∀ {i}{A : Set i} → contr (A → ⊤)
contr-exp-⊤ = (λ _ → tt) , prop-exp-⊤ _