Lemma ZeroArrow_opp {x y : C} (Z : @Zero C) : @ZeroArrow C Z x y = @ZeroArrow (C^op) (Zero_opp Z) y x. Proof. unfold ZeroArrow. rewrite ZeroArrowTo_opp. rewrite ZeroArrowFrom_opp. 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.