proposition: Lemma oppreserving_quotient `{Funext} (w : SymbolType σ) (g : Operation (A/Φ) w) (α : Operation A w) (G : ComputeOpQuotient A Φ α g) : OpPreserving def_hom_quotient α g.
proof: Proof. unfold ComputeOpQuotient in G. induction w; cbn in *. - by destruct (G tt)^. - intro x. apply IHw. intro a. apply (G (x,a)). Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism