proposition: Lemma CokernelOutOp {x y z : A} (f1 f2 : A⟦y, z⟧) (g : A⟦x, y⟧) (CK : Cokernel Z g) (H1 : g · f1 = ZeroArrow Z _ _) (H2 : g · f2 = ZeroArrow Z _ _) : CokernelOut Z CK _ (to_binop _ _ f1 f2) (CokernelOutOp_Eq f1 f2 g H1 H2) = to_binop _ _ (CokernelOut Z CK _ f1 H1) (CokernelOut Z CK _ f2 H2).
proof: Proof. use CokernelOutsEq. rewrite CokernelCommutes. rewrite to_premor_linear'. rewrite CokernelCommutes. rewrite CokernelCommutes. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels