proposition: Lemma compute_op_quotient (u : Symbol σ) : ComputeOpQuotient u.#A u.#QuotientAlgebra.
proof: Proof. apply op_quotient_algebra. Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism