It’s amazing what you can find in the HoTT repository these days! I was browsing it the other week, looking up something quite different, when I came across a theorem in `Funext.v`

(originally by Voevodsky) which answers, in a surprising direction, a question posed by Richard Garner in his paper On the strength of dependent products…, and as far as I know still open in the literature.

The punchline is, roughly: *all forms of functional extensionality seem to be derivable from almost the weakest form you might think of.* In the terminology of Richard’s paper, [Π-ext] and [Π-ext-comp] together imply [Π-ext-app], [Π-Id-elim], and so on; and in fact even the assumption of [Π-ext-comp] is negotiable.

Coq code for most of what I say here can be found in my fork of `Funext.v`

.

The most traditional form of functional extensionality is the statement

*Naive functional extensionality:* If functions take equal values, then they are equal.

We can put a nice gloss on this in homotopical language. If *f*, *g* are dependent functions of type ∏_{x:A} *B _{x}*, a

*homotopy*

*h*:

*f*==

*g*is a function giving for each

*x:A*a path

*h(x)*:

*f(x)*=

*g(x)*. Then naive functional extensionality just posits a map

**ext**

_{f,g}: (

*f*==

*g*) → (

*f*=

*g*), converting homotopies to paths. (This is the rule [Π-ext] in Richard’s paper.)

In a world where UIP held, this would be quite satisfactory on its own. But with non-trivial path spaces, one often needs to know more!

For instance, when we feed **ext** the identity homotopy on a function *f*, it should give just the identity path on *f*, not some potentially non-trivial loop. In other words, we want a path **ext-comp** *f*: **ext**(λ*x*, r(*f*(*x*))) = r(*f*). Or we could even ask this to be a definitional equality; this is [Π-ext-comp] in Richard’s paper, and if we think of **ext** as an eliminator, this is the appropriate computation rule, telling us how it acts on canonical forms. Let’s call our propositional version [Π-ext-comp-prop].

On the other hand, we might want to know at least something about how the paths produced by **ext** behave under path-elimination. In particular, there’s always a canonical function going in the opposite direction, converting homotopies into paths: **happly**_{f,g}: (*f* = *g*) → (*f* == *g*). (It’s defined just by path-elimination.) If we produce a path with **ext** and then take it back with **happly**, we’d like to get back the homotopy we first thought of, i.e. to have for each *h* a path **ext-app** *h*: **happly**(**ext** *h*) = *h*.

This is easily interderivable with [Π-ext-app] in the paper; again it has an associated computation principle, [Π-ext-app-comp], but this will be a bit peripheral to our main story, so I won’t go into its details.

In other words, though, [Π-ext-app] just says that **ext**_{f,g} is a right up-to-homotopy inverse for **happly**_{f,g}. So we could also consider the principle that it should be a *left* homotopy inverse for **happly**_{f,g} — except that we already have, pretty much! It’s easy to show — try it as an exercise! — that [Π-ext-comp-prop] is equivalent to **ext**_{f,g} being a left homotopy inverse for **happly**_{f,g}.

So, taken together [Π-ext], [Π-ext-comp-prop], and [Π-ext-app] imply that **happly**_{f,g} is an equivalence; and on the other hand, it clearly implies them all back. So this can be taken as an alternative form of functional extensionality:

*Strong functional extensionality:* The canonical map **happly**_{f,g}: (*f* = *g*) → (*f* == *g*) is an equivalence.

This is more clearly a homotopically-good statement than the others. In particular, being an equivalence is a mere proposition — so in assuming this, we don’t need to worry about the particular choice of witness being canonical in any sense. No computation rules needed!

Richard Garner doesn’t discuss this statement in the paper, but he has a closely related rule [Π-Id-elim], which together with its computation rule [Π-Id-elim-comp] says that the types of homotopies (*f* == *g*) have the same universal property as the path types (*f* = *g*), with the identity homotopy playing the role of the identity path. It’s not hard to show that modulo making [Π-Id-elim-comp] propositional, this is equivalent to strong functional extensionality — an instance of the general principle that two things with the same universal property should be equivalent.

So now, the question is: to what extent does naive functional extensionality — [Π-ext] alone — imply any of the others?

For a warmup, let’s think about [Π-ext-comp]. Does [Π-ext] imply it? Yes and no. [Π-ext-comp] is an assertion about the specific witness **ext** for [Π-ext]; and while an arbitrary witness **ext** may not necessarily satisfy [Π-ext-comp], but it can always be “corrected” to one that does. Proof? Try this, it’s a nice exercise; solution here.

So, that’s an encouraging start! Can we similarly get from these to [Π-ext-app], or equivalently to strong functional extensionality? It’s far from obvious; but this was the surprising theorem that I originally found in `Funext.v`

:

**Theorem (Voevodsky).** Naive functional extensionality implies strong functional extensionality.

What follows is my distillation of the proof I first found, which was itself a cleanup by Mike Shulman of Voevodsky’s original proof. It’s still fairly fiddly, though; so if you’re not in the mood, I recommend skipping to the end.

From what we’ve seen above, it’s enough to show:

**Theorem.** [Π-ext] and [Π-ext-comp-prop] imply [Π-ext-app].

*Proof.* We need to show that for any functions *f*, *g* and homotopy *f*: *g* == *h*, we can construct some path **happly**(**ext** *h*) = *h*.

Fix *f*, and think of *g* and *h* as varying. In the case where (*g*,*h*) is the pair (*f*,(λ*x*. r(*f*(*x*)))), it’s easy to construct the desired path, using [Π-ext-comp-prop] together with the computational behaviour of **happly**.

So to show it for arbitrary *g*,*h*, it’s sufficent to give a path from the pair (*g*,*h*) to the pair (*f*,(λ*x*. r(*f*(*x*)))). In other words, we want to show that the space of such pairs (*g*,*h*) is *contractible*. (This statement itself could be considered as another form of functional extensionality.)

To do this, we’ll look at the space of such pairs as a retract, up to homotopy, of another space — of functions into pairs — which we’ll then show contractible. In other words, we need to show two lemmas:

**Lemma 1.** Assume [Π-ext]. Given any function *f* : ∏_{x:A} *B _{x}*, the space of pairs of functions {

*g*: ∏

_{x:A}

*B*&

_{x}*h*:

*f*==

*g*} is a retract up to homotopy of the space of functions into pairs, ∏

_{x:A}{

*y*:

*B*&

_{x}*p*:

*x*=

*y*}. (I’m using roughly Coq’s notation for Σ-types here; I hope it’s clear what it means.)

**Lemma 2.** Assume [Π-ext]. Then for any *f* as above, the type ∏_{x:A} { *y* : *B _{x}* &

*p*:

*x*=

*y*} is contractible.

*Proof of Lemma 1.* It’s easy to write down functions going between the two types. To see that they give a retraction, take a pair (*g*,*h*), and send it out and back; what we get back is the pair ((λ*x*. *gx*),(λ*x*. *hx*)) — with *η*-expansions of the original functions. So, we need to use an *η*-rule somehow.

Since we have functional extensionality, it’s easy to show the necessary *η*-rule: any function *k* has a path *η _{k}* to its own

*η*-expansion. But using it is a little subtle: we’re trying to construct a path between pairs, (

*g*,

*h*) = ((λ

*x*.

*gx*),(λ

*x*.

*hx*)), and the obvious thing to try is the fact that a path between pairs comes from a pair of paths. But if we do that, using

*η*as the first path, then the second path needed involves transport along

_{g}*η*— and the behaviour under transport of terms produced from

_{g}**ext**is exactly what we’re trying to get a handle on in the first place!

Instead, we approach it a bit differently: we use the *η*-rule at the point where the hypotheses *g*,*h* are introduced. So given *g*, but with *h* still generalised, we want to show that for all *h*, (*g*,*h*) = ((λ*x*. *gx*),(λ*x*. *hx*)). By eta-expansion, it’s enough to show this with (λ*x*. *gx*) in place of *g*: so, that for all appropriate *h*, ((λ*x*. *gx*),*h*) = ((λ*x*. *gx*),(λ*x*. *hx*)). Only then do we introduce *h*; and this time, there’s no transport along *η _{g}* involved in the goal, so we’re home and dry.

(This approach to *η*-expansion — essentially, assuming as soon as a function is introduced that WLOG it’s already *η*-expanded — seems to work quite cleanly in general, so I wrapped it up in a couple of tactics `eta_intro`

, `eta_expand`

, which others may also find useful. They’re still a bit limited, though, so someone with more Ltac experience might well be able to improve them, which would be great! Of course, if Coq gets a definitional η-rule then these won’t be necessary…)

*Proof of Lemma 2.* We need to show that given *f* as above, the type ∏_{x:A} { *y* : *B _{x}* &

*p*:

*x*=

*y*} is contractible. Certainly, for each individual

*x*the type {

*y*:

*B*&

_{x}*p*:

*x*=

*y*} is contractible — you probably knew it already, and if not, it’s nice and easy to prove.

But now, by [Π-ext], it’s easy to show that a product of contractible spaces is contractible; so we’re done! □

(In the code, I handle the contractibility statements slightly differently. Contractibility seems the conceptually clearer way of stating them; but one can make the overall proof slightly more compact by working just with the contractions, since the basepoints in all cases are obvious.

We thus have strong functional extensionality from weak — and moreover, we have a kicker:

**Scholium.** If the witness **ext-app** for [Π-ext-app] is as constructed as above, and moreover [Π-ext-comp] holds *definitionally*, then so does [Π-ext-app-comp].

*Proof.* By appropriate contemplation of the preceding proof. □

(Unlike the rest, this can’t be formalised in Coq, since one can’t take a definitional equality as a hypothesis.) The results of Section 5 of Garner then show that these imply the definitional forms of [Π-Id-elim(-comp)] and other rules.

So — what’s the moral of this proof? It was moderately long and rather fiddly; but what actually makes the whole thing tick? I’d say: Σ-types. We’re trying to show how paths produced by **ext** behave under **happly**, or more generally under path-elimination. The retraction of Lemma 2 lets us relate them to paths in Σ-types; and for paths in Σ-types, or rather for their projections to the base space, we *do* know something about transport, thanks to their “second projections” to a path in a fiber. And this is just enough that with some leverage, we can work up to the more general statements.

**Extra bonus exercise.** In the view of [Π-ext-comp-prop] and [Π-ext-app] as making **ext** an inverse to **happly**, what does [Π-ext-app-comp-prop] correspond to?

Very nice! My immediate thought upon reading the Extra Bonus Exercise was “obviously, it should be the triangle identity making

happlyinto an adjoint equivalence.” And looking back at Richard’s paper, I think that’s basically what it is, modulo eta-conversion, path-induction, and propositionality of [Π-ext-comp] (that’s a lot of moduli…).Yep — that was exactly my take on it too. And this tells us immediately that up to a “correction” of [Π-ext-app], it can always be made to hold.

Another interesting thing I’ve noticed recently about function extensionality is that in terms of semantics in a model category, the “weak funext” axiom that the product of contractible types is contractible, i.e. , is equivalent to asking that dependent product along a fibration preserve acyclic fibrations — or equivalently that pullback along a fibration preserve cofibrations. This is the “other half” of the condition for to be a Quillen adjunction — the first half (pullback along a fibration preserves acyclic cofibrations, or dependent product along a fibration preserves fibrations) being requisite for an interpretation of dependent products at all (or, in the absence of dependent products, for dealing with the necessary extra context in the identity type rules).

Since the proof Peter summarized above shows that weak funext, together with the eta rule (which holds definitionally in any locally cartesian closed category), implies strong funext, this means that being a Quillen adjunction is exactly what we need in order to interpret dependent products with function extensionality. Once again there is a surprisingly close match between the type theory and the homotopy theory.

Lovely. Now, let us revisit your thesis (sorry!), and recall all the trouble we had there when trying to avoid extensionality. If we now assume weak, and thus strong, extensionality, does the -category of types become more manageable?

I also enjoyed discovering this result in Voevodsky’s files. I have a

slightly more precise statement in my Agda formalisation

(http://www.cse.chalmers.se/~nad/listings/equality/Weak-equivalence.html):

Here ext⁻¹ is happly, and a and b are universe levels.

For some early speculation regarding these kinds of statements, see

Section 5.3 of Hofmann and Streicher’s “The groupoid interpretation of

type theory”.