(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. 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.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.