proposition: Lemma path_quotient_algebras_third_surjection : A/Ψ / cong_ker hom_third_surjection = A/Ψ / Θ.
proof: 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.
imports: Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_quotient_algebra Classes.theory.ua_isomorphic Classes.theory.ua_first_isomorphism