proposition: Lemma ZerosArrowEq (Z Z' : Zero) (a b : C) : ZeroArrow Z a b = ZeroArrow Z' a b.
proof: Proof. set (i := z_iso_Zeros Z Z'). unfold ZeroArrow. assert (e : ZeroArrowTo Z a · identity _ = ZeroArrowTo Z a) by apply id_right. rewrite <- e. clear e. rewrite <- (z_iso_inv_after_z_iso i). rewrite assoc. assert (e1 : ZeroArrowTo Z a · i = ZeroArrowTo Z' a) by apply ArrowsToZero. rewrite e1. clear e1. assert (e2 : inv_from_z_iso i · ZeroArrowFrom Z b = ZeroArrowFrom Z' b) by apply ArrowsFromZero. rewrite <- assoc. rewrite e2. clear e2. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal