There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For example, if you had the following context:

P (λx. 1 + f x)
f : Bool -> Nat
e : (x : Bool) -> f x == 1

You could rewrite the goal to P (λx. 1 + 1) as follows:

rewrite X in P (λx. 1 + X) with e x

This "rewrite" primitive would work exactly as usual, with the only exception being we allow e to access the x bound in P (λx. 1 + X); which makes logical sense, after all, why should it not? This syntax would elaborate to the full rewrite primitive, whose type could be, kind-of, written as:

rewrite :
  (K : Type) ->
  (A : Type) ->
  (a : K -> A) ->
  (b : K -> A) ->
  (e : K -> Equal A a b) ->
  (P : A -> Type) ->
  (p : P a{k:K}) ->
  P b{k:K}

Here, Equal is just propositional equality, K is the type of a variable that is in context where x occurs in P, and {k:K} means that, after substitution, this expression will "capture" the k:K bound, and be applied to it. Explaining with words is hard, but the "magic" is that rewrite would, in an ugly and hard-coded way, inspect P to assert that there is a k:K variable where its bound variable occurs, and it would apply e to that bound variable. That's basically it.

rewrite _ _ _ _ e (λ x -> ... (λ k -> ... x ...) ...) p
                                 /\ k is in context where x occurs

The actual type of rewrite would depend on the amount of λ-binders surrounding x in the body of P. If it had no λ, then its type would be the same as the usual rewrite ((A : Type) -> (a b : A) -> (e : Equal A a b) -> (P : A -> Type) -> P a -> P b).

With such primitive, fun-ext would be trivial, because we would be able to rewrite g y in (λx. f x) == (λk. g k) applying h to the k variable bound inside the λk.

fun-ext :
  (A : Type) ->
  (B : A -> Type) ->
  (f : (x : A) -> B x) -> 
  (g : (x : A) -> B x) -> 
  (h : (x : A) -> f x == g x) ->
  f == g

fun-ext =

  // goal: f == g

  eta-expand f
  eta-expand g

  // goal: (λx. f x) == (λk. g k)

  rewrite K in (λx. f x) == (λk. K) with h k
  //                                       /\ we use the `k` bound in `λk. K` 
  //                                       /\ to make `h k : f k == g k` here,
  //                                       /\ which justifies rewriting `g k`                                           
  //                                       /\ by `f k` in the goal. this
  //                                       /\ is the only difference w.r.t.
  //                                       /\ the usual `rewrite`, which
  //                                       /\ won't let `h` access that `k`

  // goal: (λx. f x) == (λk. f k)


As a last attempt to explain: the naive intuition is that, in order to prove fun-ext, we need to apply h to some variable k : A, but there is no such variable in context. But, in the location where we need to rewrite - i.e., (λx. f x) == (λk. <HERE>), inside the goal - we do have a k in context. Normally, we can't apply h to that "inner" k in the goal. But if we hard-coded rewrite to allow its equality witness, e, to depend on variables in context in the location where the rewrite takes place (<HERE>), then we could apply h to that k, and fun-ext would be trivial. It kinda makes logical sense that the equality witness e should be allowed to depend on these variables; after all, e exists to justify the rewrite, and these variables are in scope where the rewrite takes place.

My question is: what is wrong with this approach? I assume this isn't done because it is ugly and kind of hacky, but so are the current cubical type theories, specially when it comes to transp and faces. Regardless, I'm curious: is there anything inherently wrong/broken/inconsistent in implementing funext that way?

  • 2
    $\begingroup$ Are these rewrites terms inside type theory or some sort of meta-level tactics? Also, is == judgemental or propositional equality? $\endgroup$ Commented Nov 28, 2021 at 21:19
  • 1
    $\begingroup$ Your "context-aware rewrite" reminds me of Observational Type Theory. There, equality isn't an inductive type, but is defined by case-analysis on the types of the equated terms, yielding a computational interpretation of extensionality. See cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf and hal.inria.fr/hal-03367052/document $\endgroup$ Commented Nov 28, 2021 at 21:33
  • 1
    $\begingroup$ After some further thinking: if rewrites are meta-level tactics, then you've got a lot of explaining to do. If they are terms then I will bet that they are interderivable with function extensionality. $\endgroup$ Commented Nov 28, 2021 at 23:55
  • $\begingroup$ @AndrejBauer this question is really not as in-depth as you're making it seem. It was just something silly that was always stuck on my head, and that I assumed would be wrong for some obvious reason, but never asked. Regardless, I've updated the question to clarify what the rewrite I'm talking about is and does. Let me know if it makes sense. $\endgroup$
    – MaiaVictor
    Commented Nov 29, 2021 at 4:39
  • 1
    $\begingroup$ Well, function extensionality seems less complicated than the stuff about "being under a binder" etc. that you would need to rewrite. But let me also say that exploring such ideas is often worthwhile because it may lead to nead techniques and tactics. For example, if rewrite turns out to be mre easily used, then it might be worth implementing it. $\endgroup$ Commented Nov 29, 2021 at 17:58


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.