How to prove that a functional is injective in Agda?

March 22, 2023

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.

Extensionally it should be immediate, map-foo is just calling f on the value inside the foo and rewrapping it;
Intensionally, if 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?

>Solution :

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