Curry-Howard isomorphism definitions in Coq using fun

Question

I'm having some issues with defining in Coq, more specifically when defining using the CHI. I have managed to gain the understanding of basic principals but when I try to define this"

((A -> (A -> C)) * ((A -> C) -> A)) -> C :=

I get nowhere due to the fact it keeps telling me:
"Error: The type of this term is a product while it is expected to be "C".
I have already tried the usual tactics I have used earlier in my script and I'm convinced this has to be solved using the same methods (fun) however everything I seem to be trying ends in that error message. Any tips?

Answer 1

It seems you are defining a function that takes as input:

• a function of type A -> (A -> C): given an object of type A, it gives back a function of type A -> C.
• a function of type (A -> C) -> A: given a function of type A -> C, it gives back an object of type A.

You are trying to build an object of type C which I don't see how you will managed to do it. However you can build an object of type A by combining the two functions you have as input.

Hope it helps,

V.