Definition isTerminal_opp {x : C} (H : @isTerminal C x) : @isInitial (C^op) x := H.
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.