proposition: Lemma MonicsAreKernels_opp_isCokernel {D1 : Data1 C} {D2 : Data2 C D1} (AMKD : MonicsAreKernels C D1 D2) (y z : C^op) (E : Epi (op_category C) y z) : isCokernel (Zero_opp C (pr1 D1)) (CokernelArrow (pr2 D2 z y (opp_Epi C E))) E (MonicsAreKernels_opp_eq AMKD y z E).
proof: Proof. use (isCokernel_opp _ ). - exact (to_Zero D1). - exact (CokernelCompZero _ (to_Cokernels D2 z y (opp_Epi C E))). - exact (AMKD _ _ (opp_Epi C E)). 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