proposition: Lemma op_quotient_algebra_well_def (q : ∀ (w : SymbolType σ), QuotOp w) (s : Sort σ) (w : SymbolType σ) (f : Operation A (s ::: w)) (P : OpCompatible A Φ f) (x y : A s) (C : Φ s x y) : op_qalg_cons q f P x = op_qalg_cons q f P y.
proof: Proof. apply (@path_forall_ap_operation _ σ). apply quotient_ind_prop_family_prod; try exact _. intro a. destruct (q _ _ (op_compatible_cons Φ s w f x P)) as [g1 P1]. destruct (q _ _ (op_compatible_cons Φ s w f y P)) as [g2 P2]. refine ((P1 a) @ _ @ (P2 a)^). apply qglue. exact (P (x,a) (y,a) (C, reflexive_for_all_2_family_prod A Φ a)). Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism