respects_equivalenceR_equiv' {A} {P P' : forall B, (B <~> A) -> Type} (eP : forall B e, P B 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.