{A A'} {P : forall B, (B <~> A) -> Type} {P' : forall B, B <~> A' -> Type} (eA : A' <~> A) (eP : forall B e, P B (equiv_compose' eA e) <~> P' B e) `{HP : RespectsEquivalenceR A P} : RespectsEquivalenceR A' P'. Proof. simple refine ((fun B e => _); _). { refine (equiv_compose' (eP _ _) (equiv_compose' (equiv_compose' (HP.1 _ _) (equiv_inverse (HP.1 _ _))) (equiv_inverse (eP _ _)))). } { t. } Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Tactics. Require Import Types.Equiv Types.Prod Types.Forall Types.Sigma Types.Universe.