(_ : ∀ s x y, Ψ s x y → Φ s x y) (s : Sort σ) (a b : (A/Ψ) s) := ∀ (x y : A s), in_class (Ψ s) a x → in_class (Ψ s) b y → Φ s x y. Global Instance equivalence_relation_quotient (s : Sort σ) : EquivRel ( subrel s). Proof. constructor. - refine (Quotient_ind_hprop (Ψ s) _ _). intros x y z P Q. apply subrel. by transitivity x. - refine (Quotient_ind_hprop (Ψ s) _ _). intro x1. refine (Quotient_ind_hprop (Ψ s) _ _). intros x2 C y1 y2 P Q. symmetry. by apply C. - refine (Quotient_ind_hprop (Ψ s) _ _). intro x1. refine (Quotient_ind_hprop (Ψ s) _ _). intro x2. refine (Quotient_ind_hprop (Ψ s) _ _). intros x3 C D y1 y2 P Q. transitivity x2. + exact (C y1 x2 P (EquivRel_Reflexive x2)). + exact (D x2 y2 (EquivRel_Reflexive x2) Q). Defined.
Require Import Import algebra_notations quotient_algebra_notations isomorphic_notations.