Lemma opp_ZeroArrow {x y : C} (Z : @Zero (C^op)) : @ZeroArrow (C^op) Z x y = @ZeroArrow C (opp_Zero Z) y x. Proof. unfold ZeroArrow. rewrite opp_ZeroArrowTo. rewrite opp_ZeroArrowFrom. 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.