Lemma isKernel_opp {x y z : C^op} {f : C⟦x, y⟧} {g : C⟦y, z⟧} {Z : Zero C} {H : f · g = ZeroArrow Z _ _} (CK' : isCokernel Z f g H) {Z' : Zero C^op} : isKernel Z' (g : C^op⟦z, y⟧) (f : C^op⟦y, x⟧) (isCokernel_opp_eq f g Z H Z'). Proof. set (CK := make_Cokernel _ _ _ _ CK'). use make_isKernel. - intros w h H'. rewrite <- (ZerosArrowEq C^op (Zero_opp Z) Z' w x) in H'. rewrite <- ZeroArrow_opp in H'. use unique_exists. + exact (CokernelOut Z CK w h H'). + use (CokernelCommutes Z CK). + intros y0. apply hs. + cbn. intros y0 X. use (CokernelOutsEq _ CK). rewrite (CokernelCommutes Z CK). cbn. rewrite X. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Zero. 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.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. @ZeroArrowTo (C^op) Z x = @ZeroArrowFrom C (opp_Zero Z) x. Lemma opp_ZeroArrowFrom {x : C} (Z : @Zero (C^op)) : @ZeroArrowFrom (C^op) Z x = @ZeroArrowTo C (opp_Zero Z) x. apply ArrowsFromZero. rewrite opp_ZeroArrowFrom. @ZeroArrowTo C Z x = @ZeroArrowFrom (C^op) (Zero_opp Z) x. Lemma ZeroArrowFrom_opp {x : C} (Z : @Zero C) : @ZeroArrowFrom C Z x = @ZeroArrowTo (C^op) (Zero_opp Z) x. apply ArrowsFromZero. rewrite ZeroArrowFrom_opp.