(s : Sort σ) : Relation (A s) := λ (x y : A s), f s x = f s y. Global Instance equiv_rel_ker (s : Sort σ) : EquivRel ( s). Proof. repeat constructor. - intros x y. exact inverse. - intros x y z. exact concat. Qed.
Require Import Import