Looooong time no see! Recently I have wrote some Agda, and I’ve found something worth writing about.

{-# OPTIONS --allow-unsolved-meta #-} module 2021-3-2-AgdaEtaFunc (A : Set) (B : A -> Set) where open import Agda.Builtin.Equality private ImF = forall {x} -> B x private ExF = forall x -> B x

It all starts from a friend asking me about function extensionality in vanilla Agda (we all know we have that in cubical Agda). He postulated the extensionality of both implicit and explicit function types:

Implicit = {f g : ImF} -> ((x : A) -> f {x} ≡ g {x}) -> _≡_ {A = ImF} f g Explicit = {f g : ExF} -> ((x : A) -> f x ≡ g x) -> f ≡ g

And he wants to eliminate one of the postulates, because postulating is not
elegant in general.
So, I started with rewriting with `Implicit`

to prove `Explicit`

. Is that doable?

explicit₀ : Implicit -> Explicit explicit₀ im p rewrite im p = {! im p !}

In the above goal, the type of `im p`

is `(λ {x} -> f x) ≡ (λ {x} -> g x)`

,
and the goal type after rewrite is still `f ≡ g`

. So, Agda is unhappy with this rewrite.
Also, we have refined our goal: we wanna prove `(λ {x} -> f x) ≡ (λ {x} -> g x) -> f ≡ g`

.
Note that we could prove these (that Jon pointed out in a [tweet]):
[tweet]: https://twitter.com/jonmsterling/status/1362803441974804483

fact₀ : {f g : ImF} -> (λ {x} -> f {x}) ≡ (λ {x} -> g {x}) -> _≡_ {A = ImF} f g fact₀ p = p fact₁ : {f g : ExF} -> (λ x -> f x) ≡ (λ x -> g x) -> f ≡ g fact₁ p = p

But we could not turn `(λ {x} -> f x) ≡ (λ {x} -> g x)`

to `f ≡ g`

,
because this function could not be eta-shortened.
I think this is just impossible. In the end,
I came up with a solution: I hacked Agda’s dependent pattern matching.
First, I proved a lemma that converts this equation:

explicit function

`f : ExF`

after an implicit eta expansion`λ {x} -> f x`

is propositionally equal to`g : ImF`

into this equation: explicit function`f : ExF`

is propositionally equal to implicit function`g : ImF`

after an explicit eta expansion`λ x -> g {x}`

The proof is reflexivity. I think it’s because Agda finds a MGU (most general unifier, see Norell and Jesper’s papers on pattern matching about this notion) –`[(λ {x} -> f x) / g]`

, a substitution. It is the result of the positive success of the pattern matching over`refl`

, and apply this substitution to the goal, and`g`

gets replaced by`λ {x} -> f x`

. So, the result type is substituted to`f ≡ (λ x -> f x)`

, which, by Agda’s eta rule is a definitional equality. This process is similar to your pattern matching over`p : a ≡ b`

where Agda obtains`[a / b]`

as a MGU and substitutes your goal with it. So, the very idea of this lemma is that the parameter type`(λ {x} -> f x) ≡ g`

has its right-hand side in a reference form(unlike previously rewrited proofs, which are all eta-expanded lambdas).

lemma : (f : ExF) (g : ImF) -> (λ {x} -> f x) ≡ g -> f ≡ (λ x -> g {x}) lemma _ _ refl = refl

With `lemma`

we could very easily prove `Implicit -> Explicit`

:

explicit₁ : Implicit -> Explicit explicit₁ im {f = f} {g = g} p = lemma f (λ {x} -> g x) (im p)

We could polish this proof with some inference capabilities in Agda, to make it shorter (and harder to read):

explicit₂ : Implicit -> Explicit explicit₂ im {g = g} p = lemma _ (g _) (im p)

I’ll leave the proof of `Explicit -> Implicit`

as an exercise :)