The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I assume you mean (B -> X) -> (A -> X), not (A -> X) -> (B -> X); the latter is not derivable from a function A->B.

In any case, this feature is already implemented in Coq 8.4.  The following code works for me:

Axiom A : Set.

Axiom B : Set.

Axiom X : Set.

Axiom f : X -> A.

Axiom g : B -> X.

Axiom c : A -> B.

Coercion c : A >-> B.

Check f : X -> B.

Check g : A -> X.

On Sat, Mar 21, 2015 at 6:04 PM, Victor Porton <porton AT narod.ru> wrote:

What's about this idea?

I there is a coercion A->B then (in an obvious way) define also coercions (X->A)->(X->B) and (A->X)->(B->X) for every type X.

I realize that there may be some implementation difficulties or maybe even just wrong when considering my idea. But is my idea overally good?

-- 
Victor Porton - http://portonvictor.org