The Coq mailing list

[Burak Ekici <ekcburak AT hotmail.com>]

Thanks a lot Ralf, Robbert and Anton!

Right after asking the question, I noticed that my problem is a bit more complicated than what I've put in the e-mail unless I miss something trivial.

I'm actually trying to prove Mac Lane's (Kleisli) comparison theorem in Coq which basically relates an arbitrary adjunction to the Klesili adjunction via a unique functor. Therefore, I need to prove a structural equality between functors using the fact that two functors are equal if they map objects and arrows in the same way.

I brief, at some point, I obtain the following hypothesis

H1c : (fun (a b : obj catC) (f : arrow catC b a) => fmap2 a b (f o trans1 a)) =
      (fun (a b : obj catC) (f : arrow catC b a) => fmap1 a b f)

(* where "a" and "b" are objects of a category "catC", "f" is an arrow mapping "a" into "b", "fmap1" and "fmap2" are different functors, and "trans1" is a natural transformation *)

and would like to somehow convert it into

H1c : forall (a b : obj catC) (f : arrow catC b a), fmap2 a b (f o trans1 a)) = fmap1 a b f.

However, could not make it work whatever I did...

This is where the problematic case actually appears: https://github.com/ekiciburak/adjunctions_monads_Klesili/blob/master/adj_mon_kl.v#L1714-L1716

I'd be appreciated if you could take a look and give me some pointers!

Many thanks!

―

Burak.

On 26-10-2017 14:30, Ralf Jung wrote:

Oh, right -- I read "Goal" instead of Hypothesis.  Sorry for that.

; Ralf

On 26.10.2017 13:18, Robbert Krebbers wrote:

Unless I am mistaken, what Burak wants goes in the opposite way, so
function extensionality is not needed.

A simplified example of what I think he asks for:

Goal forall (A B : Type) (f g : A -> B),
  (fun x => f x) = (fun x => g x) ->
  forall x, f x = g x.
Proof.
  intros A B f g Hfg x.
  change ((fun x => f x) x = (fun x => g x) x).
  rewrite Hfg.
  reflexivity.
Qed.

On 10/26/2017 01:13 PM, Ralf Jung wrote:

Hi Burak,

what you are looking for is function extensionality:

   f = g <-> forall x, f x = g x

Function extensionality cannot be proven in Coq, but you can assume it
as an axiom.  (It is compatible with the theory.)

So, the answer to "Is there a way" is "Yes, if you are willing to assume
an axiom".  You can find it in the standard library at
<https://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html>.

Kind regards,
Ralf

On 26.10.2017 13:09, Burak Ekici wrote:

Hi all,

I have an hypothesis of the following form "H : (fun a b f => XX a b f)
= (fun a b f => YY a b f)".

Is there a way to turn it into "H: forall a b f, XX a b f = YY a b f"?

Thanks!

Best,

―

Burak.