fact: Definition cong_quotient (_ : ∀ 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.
imports: Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_quotient_algebra Classes.theory.ua_isomorphic Classes.theory.ua_first_isomorphism