proposition: Lemma oppreserving_third_surjection {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: 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.
imports: Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_quotient_algebra Classes.theory.ua_isomorphic Classes.theory.ua_first_isomorphism