Lemma isCokernel_opp {x y z : C} {f : C⟦x, y⟧} {g : C⟦y, z⟧} {Z : Zero C} {H : f · g = ZeroArrow Z _ _} (K' : isKernel Z f g H) {Z' : Zero C^op} : isCokernel Z' (g : C^op⟦z, y⟧) (f : C^op⟦y, x⟧) (isCokernel_opp_eq f g Z H Z'). Proof. set (K := make_Kernel _ _ _ _ K'). use make_isCokernel. - intros w h H'. cbn in H'. set (XXX := (ZerosArrowEq C^op (Zero_opp Z) Z' z w)). use unique_exists. + use (KernelIn Z K w h _). rewrite ZeroArrow_opp. rewrite XXX. apply H'. + cbn. use (KernelCommutes Z K). + intros y0. apply (has_homsets_opp hs). + cbn. intros y0 X. use (KernelInsEq Z K). rewrite KernelCommutes. exact X. 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.