The Coq mailing list

[maxim.krivchikov AT gmail.com]

Hi,

Suppose we have class:

Class Ob (A : Type): Type := {
 o_ord : relation A;
 o_preord : PreOrder o_ord;
 o_equiv : relation A;
 o_equiv_proof : Equivalence o_equiv;
 o_po : PartialOrder o_equiv o_ord
}.

and two classes on functions between objects:

P : forall A B : Type, Ob A -> Ob B -> (A->B)->Prop
Q : forall A B : Type, Ob A -> Ob B -> (A->B)->Prop

Then we declare instance of Ob (sig P).

Instance P_Ob (A B : Type) : Ob (sig (P A B)) := ... .

Suppose we have implication (forall A B, Q A B -> P A B) and coercion based on
this implication.


Is it possible to show that P_Ob is an instance of Ob over (sig Q)? 

(i.e. something like:
Instance Q_Ob (A B : Type) : Ob (sig (Q A B)) := P_Ob A B.)

Thanks a lot!

Maxim.