proposition: Lemma MonicsAreKernels_opp_eq {D1 : Data1 C} {D2 : Data2 C D1} (AMKD : MonicsAreKernels C D1 D2) (y z : C^op) (E : Epi (op_category C) y z) : @compose C _ _ _ E (CokernelArrow ((to_Cokernels D2) z y (opp_Epi C E))) = @ZeroArrow (op_category C) (Zero_opp C (to_Zero D1)) _ _.
proof: Proof. rewrite <- ZeroArrow_opp. set (tmp := KernelCompZero (to_Zero D1) (make_Kernel _ _ _ _ (AMKD z y (opp_Epi C E)))). cbn in tmp. cbn. rewrite tmp. clear tmp. apply ZerosArrowEq. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive