fact: Definition ops_quotient_algebra (u : Symbol σ) : Operation carriers_quotient_algebra (σ u) := (op_quotient_algebra u.#A (ops_compatible_cong A Φ u)).1.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism