<p>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 <strong>context-aware rewrite</strong>. For example, if you had the following context:</p>
<pre><code>P (λx. 1 + f x)
---------------
f : Bool -&gt; Nat
e : (x : Bool) -&gt; f x == 1
</code></pre>
<p>You could rewrite the goal to <code>P (λx. 1 + 1)</code> as follows:</p>
<pre><code>...
rewrite X in P (λx. 1 + X) with e x
...
</code></pre>
<p>This &quot;rewrite&quot; primitive would work exactly as usual, with the only exception being we allow <code>e</code> to access the <code>x</code> bound in <code>P (λx. 1 + X)</code>; which makes logical sense, after all, why should it not? This syntax would elaborate to the full <code>rewrite</code> primitive, whose type could be, kind-of, written as:</p>
<pre><code>rewrite :
  (K : Type) -&gt;
  (A : Type) -&gt;
  (a : K -&gt; A) -&gt;
  (b : K -&gt; A) -&gt;
  (e : K -&gt; Equal A a b) -&gt;
  (P : A -&gt; Type) -&gt;
  (p : P a{k:K}) -&gt;
  P b{k:K}
</code></pre>
<p>Here, <code>Equal</code> is just propositional equality, <code>K</code> is the type of a variable that is in context where <code>x</code> occurs in <code>P</code>, and <code>{k:K}</code> means that, after substitution, this expression will &quot;capture&quot; the <code>k:K</code> bound, and be applied to it. Explaining with words is hard, but the &quot;magic&quot; is that <code>rewrite</code> would, in an ugly and hard-coded way, inspect <code>P</code> to assert that there is a <code>k:K</code> variable where its bound variable occurs, and it would apply <code>e</code> to that bound variable. That's basically it.</p>
<pre><code>rewrite _ _ _ _ e (λ x -&gt; ... (λ k -&gt; ... x ...) ...) p
                                 /\ k is in context where x occurs
</code></pre>
<p>The actual type of <code>rewrite</code> would depend on the amount of <code>λ</code>-binders surrounding <code>x</code> in the body of <code>P</code>. If it had no <code>λ</code>, then its type would be the same as the usual <code>rewrite</code> (<code>(A : Type) -&gt; (a b : A) -&gt; (e : Equal A a b) -&gt; (P : A -&gt; Type) -&gt; P a -&gt; P b</code>).</p>
<p>With such primitive, fun-ext would be trivial, because we would be able to rewrite <code>g y</code> in <code>(λx. f x) == (λk. g k)</code> applying <code>h</code> to the <code>k</code> variable bound inside the <code>λk</code>.</p>
<pre><code>fun-ext :
  (A : Type) -&gt;
  (B : A -&gt; Type) -&gt;
  (f : (x : A) -&gt; B x) -&gt; 
  (g : (x : A) -&gt; B x) -&gt; 
  (h : (x : A) -&gt; f x == g x) -&gt;
  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)

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

CC BY-SA 4.0
2021-11-28T21:19:30.497Z
Are these rewrites terms inside type theory or some sort of meta-level tactics? Also, is `==` judgemental or propositional equality?
Andrej Bauer
CC BY-SA 4.0
2021-11-28T21:33:54.260Z
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 http://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf and https://hal.inria.fr/hal-03367052/document
Joey Eremondi
CC BY-SA 4.0
2021-11-28T23:55:07.873Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-11-29T04:39:26.460Z
@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.
MaiaVictor
CC BY-SA 4.0
2021-11-29T04:52:47.447Z
@jmite I'm aware of OTT, but I don't get the connection. I'll revisit OTT with that intuition in mind. Thanks!
MaiaVictor
CC BY-SA 4.0
2021-11-29T12:56:19.600Z
From what I can understand, your `rewrite` ought to be inter-derivable with function extensionality. You showed that if you have `rewrite` then you get function extensionality. But it also works the other way, does it not? Intuitively, this is so because one way of reading function extensionality is: if things are equal under a binder then they're equal. So it should be possible to derive each particular instance of `rewrite` from function extensionality.
Andrej Bauer
CC BY-SA 4.0
2021-11-29T14:55:32.247Z
@AndrejBauer yes, I think that's the case. So you're saying it is simpler to just add function extensionality itself as a primitive, right? That makes sense.
MaiaVictor
CC BY-SA 4.0
2021-11-29T17:58:42.790Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-11-29T22:29:03.367Z
@AndrejBauer implementing is simpler than explaining, though; ideally, the rewrite would just happen in-place where you want it to, so these variables would already be in-scope. I don't think it is a great idea, but **if** it is not inherently "wrong", then I'll feel tempted to explore **what** makes it correct and what I can extract out of it; which may be some more fundamental insight? -- thanks for the inputs!
MaiaVictor
CC BY-SA 4.0
2021-11-30T07:25:08.010Z
If we're talking about propositional identity types (you never made that clear, or do you mean judgemental equality?) then I am afraid there are some nasty dependent transports that you'd have to deal with to make it all tight.
Andrej Bauer
<type-theory><lambda-calculus><homotopy-type-theory><extensionality>
What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?
MaiaVictor
# What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?

(Asked by: username_0 on 2021-11-28)

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)

  refl

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. ), 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 (), 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?

**Tags:** type-theory, lambda-calculus, homotopy-type-theory, extensionality
> **Comments:**
> **username_1**: Are these rewrites terms inside type theory or some sort of meta-level tactics? Also, is `==` judgemental or propositional equality?  
> **username_2**: 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 http://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf and https://hal.inria.fr/hal-03367052/document  
> **username_1**: 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.  
> **username_0**: @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.  
> **username_0**: @jmite I'm aware of OTT, but I don't get the connection. I'll revisit OTT with that intuition in mind. Thanks!  
> **username_1**: From what I can understand, your `rewrite` ought to be inter-derivable with function extensionality. You showed that if you have `rewrite` then you get function extensionality. But it also works the other way, does it not? Intuitively, this is so because one way of reading function extensionality is: if things are equal under a binder then they're equal. So it should be possible to derive each particular instance of `rewrite` from function extensionality.  
> **username_0**: @AndrejBauer yes, I think that's the case. So you're saying it is simpler to just add function extensionality itself as a primitive, right? That makes sense.  
> **username_1**: 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.  
> **username_0**: @AndrejBauer implementing is simpler than explaining, though; ideally, the rewrite would just happen in-place where you want it to, so these variables would already be in-scope. I don't think it is a great idea, but **if** it is not inherently "wrong", then I'll feel tempted to explore **what** makes it correct and what I can extract out of it; which may be some more fundamental insight? -- thanks for the inputs!  
> **username_1**: If we're talking about propositional identity types (you never made that clear, or do you mean judgemental equality?) then I am afraid there are some nasty dependent transports that you'd have to deal with to make it all tight.  

---

## 0 answers

