Definition i_respectful {A B : Type → Type}
           (RA : ∀ T, A T → A T → Prop)
           (RB : ∀ T, B T → B T → Prop)
           (f1 f2 : A ~> B)
  : Prop
  := ∀ T (a1 a2 : A T), RA T a1 a2 → (RB T) (f1 T a1) (f2 T a2).

Definition i_pointwise {A B : Type → Type}
           (RB : ∀ T, B T → B T → Prop)
           (f1 f2 : A ~> B)
  : Prop
  := ∀ T (a : A T), (RB T) (f1 T a) (f2 T a).

#[global]
Instance Reflexive_i_pointwise {A B : Type → Type}
         (RB : ∀ T, B T → B T → Prop)
         {Reflexive_R : ∀ T, Reflexive (RB T)}
  : Reflexive (@i_pointwise A B RB).
Proof.
  repeat red; intros; red in Reflexive_R; eauto.
Qed.

#[global]
Instance Symmetric_i_pointwise {A B : Type → Type}
         (RB : ∀ T, B T → B T → Prop)
         {Symmetric_R : ∀ T, Symmetric (RB T)}
  : Symmetric (@i_pointwise A B RB).
Proof.
  repeat red; intros; red in Symmetric_R; eauto.
Qed.

#[global]
Instance Transitive_i_pointwise {A B : Type → Type}
         (RB : ∀ T, B T → B T → Prop)
         {Transitive_R : ∀ T, Transitive (RB T)}
  : Transitive (@i_pointwise A B RB).
Proof.
  repeat red; intros; red in Transitive_R; eauto.
Qed.

#[global]
Instance Equivalence_i_pointwise {A B : Type → Type}
         (RB : ∀ T, B T → B T → Prop)
         {Equivalence_R : ∀ T, Equivalence (RB T)}
  : Equivalence (@i_pointwise A B RB).
Proof.
  split; try typeclasses eauto.
Qed.

#[global]
Instance subrelation_i_pointwise_i_respectful {A B : Type → Type}
           (RB : ∀ T, B T → B T → Prop)
  : subrelation (i_pointwise RB) (i_respectful (fun T ⇒ @eq (A T)) RB).
Proof.
  repeat red; intros; subst; auto.
Qed.

(* This is not an instance, to avoid instance resolution loops. *)
Definition subrelation_i_respectful_i_pointwise {A B : Type → Type}
           (RB : ∀ T, B T → B T → Prop)
  : subrelation (i_respectful (fun T ⇒ @eq (A T)) RB) (i_pointwise RB).
Proof.
  repeat red; auto.
Qed.