Strong functional extensionality from weak | Homotopy Type Theory

Strong functional extensionality from weak

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:ABx, 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 extf,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: happlyf,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 extf,g is a right up-to-homotopy inverse for happlyf,g. So we could also consider the principle that it should be a left homotopy inverse for happlyf,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 extf,g being a left homotopy inverse for happlyf,g.

So, taken together [Π-ext], [Π-ext-comp-prop], and [Π-ext-app] imply that happlyf,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 happlyf,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:ABx, the space of pairs of functions { g : ∏x:ABx & h : f == g } is a retract up to homotopy of the space of functions into pairs, ∏x:A { y : Bx & 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 : Bx & 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 ηg as the first path, then the second path needed involves transport along ηg — and the behaviour under transport of terms produced from 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 : Bx & p : x = y } is contractible. Certainly, for each individual x the type { y : Bx & 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?