{w : SymbolType σ} (α : Operation A w) (γ : Operation (A/Φ) w) (ζ : Operation ((A&&P) / Ψ) w) (CA : ClosedUnderOp (A/Φ) Q γ) (CB : ClosedUnderOp A P α) (QA : ComputeOpQuotient A Φ α γ) (QB : ComputeOpQuotient (A&&P) Ψ (op_subalgebra A P α CB) ζ) : OpPreserving def_second_isomorphism ζ (op_subalgebra (A/Φ) Q γ CA). Proof. unfold ComputeOpQuotient in *. induction w; cbn in *. - apply path_sigma_hprop. cbn. destruct (QB tt)^, (QA tt)^. by apply qglue. - refine (Quotient_ind_hprop (Ψ t) _ _). intro x. apply (IHw (α (i t x)) (γ (class_of (Φ t) (i t x))) (ζ (class_of (Ψ t) x)) (CA (class_of (Φ t) (i t x)) (tr (x; _))) (CB (i t x) x.2)). + intro a. exact (QA (i t x, a)). + intro a. exact (QB (x, a)). Defined.
Require Import Import