A/Ψ / cong_ker hom_third_surjection = A/Ψ / Θ. Proof. apply path_quotient_algebra_iff. intros s x y. split; generalize dependent y; generalize dependent x; refine (Quotient_ind_hprop (Ψ s) _ _); intro x; refine (Quotient_ind_hprop (Ψ s) _ _); intro y. - intros K x' y' Cx Cy. apply subrel in Cx. apply subrel in Cy. apply (related_quotient_paths (Φ s)) in K. transitivity x. + by symmetry. + by transitivity y. - intro T. apply qglue. exact (T x y (EquivRel_Reflexive x) (EquivRel_Reflexive y)). Defined.
Require Import Import algebra_notations quotient_algebra_notations isomorphic_notations.