Lemma EpisAreCokernels_opp_isKernel {D1 : Data1 C} {D2 : Data2 C D1} (AECD : EpisAreCokernels C D1 D2) (y z : C^op) (M : Monic (op_category C) y z) : isKernel (Zero_opp C (to_Zero D1)) M (KernelArrow (to_Kernels D2 z y (opp_Monic C M))) (EpisAreCokernels_opp_eq AECD y z M). Proof. use (isKernel_opp _). - exact (to_Zero D1). - exact (KernelCompZero _ (to_Kernels D2 z y (opp_Monic C M))). - exact (AECD _ _ (opp_Monic C M)). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. isKernel (to_Zero A) (ZeroArrowFrom x) M (ArrowsFromZero A (to_Zero A) y (ZeroArrowFrom x · M) (ZeroArrow (to_Zero A) _ _)). make_Kernel (to_Zero A) (ZeroArrowFrom _) M _ (MonicKernelZero_isKernel M). - intros y0 Y. apply ArrowsFromZero.