proposition: Lemma oppreserving_quotient_algebra_mapout {w : SymbolType σ} (g : Operation (A/Φ) w) (α : Operation A w) (β : Operation B w) (G : ComputeOpQuotient A Φ α g) (P : OpPreserving f α β) : OpPreserving def_hom_quotient_algebra_mapout g β.
proof: Proof. unfold ComputeOpQuotient in G. induction w; cbn in *. - destruct (G tt)^. apply P. - refine (Quotient_ind_hprop (Φ t) _ _). intro x. apply (IHw (g (class_of (Φ t) x)) (α x) (β (f t x))). + intro a. apply (G (x,a)). + apply P. Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism