{w : SymbolType σ} (f : Operation A w) : ∀ (α : Operation (A/Φ) w) (Qα : ComputeOpQuotient A Φ f α) (β : Operation (A/Ψ) w) (Qβ : ComputeOpQuotient A Ψ f β), OpPreserving def_third_surjection β α. Proof. induction w. - refine (Quotient_ind_hprop (Φ t) _ _). intros α Qα. refine (Quotient_ind_hprop (Ψ t) _ _). intros β Qβ. apply qglue. transitivity f. + apply subrel. apply (related_quotient_paths (Ψ t)). exact (Qβ tt). + apply (related_quotient_paths (Φ t)). symmetry. exact (Qα tt). - intros α Qα β Qβ. refine (Quotient_ind_hprop (Ψ t) _ _). intro x. exact (IHw (f x) (α (class_of (Φ t) x)) (λ a, Qα (x,a)) (β (class_of (Ψ t) x)) (λ a, Qβ (x,a))). Defined.
Require Import Import algebra_notations quotient_algebra_notations isomorphic_notations.