Consider for example the following code:
open import Relation.Binary.PropositionalEquality
record Foo (A : Set) : Set where
constructor foo
field
foo-a : A
map-foo : forall {A} -> (A -> A) -> Foo A -> Foo A
map-foo f (foo a) = foo (f a)
map-foo-injective : forall {A} {f g : A -> A} -> map-foo f ≡ map-foo g -> f ≡ g
map-foo-injective {A} {f} {g} eq = ?
Intuitively I think the equivalence should hold, both extensionally and intensionally.
map-foo
is just calling f
on the value inside the foo
and rewrapping it;map-foo f
is the exact same function as map-foo g
then all the captures must be exactly the same too, so f ≡ g
should hold as well.However I can't find a way to formalize this. Is there any way to prove it?
You are correct that in your case, thanks to eta-equality of functions, you can actually get it without any postulate:
open import Function.Base
map-foo-injective : forall {A} {f g : A -> A} ->
map-foo f ≡ map-foo g -> f ≡ g
map-foo-injective {A} {f} {g} eq
= let eq = cong (Foo.foo-a ∘′_) eq in
let eq = cong (_∘′ foo) eq in
eq