Lemma ZerosArrowEq (Z Z' : Zero) (a b : C) : ZeroArrow Z a b = ZeroArrow Z' a b. 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.
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.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Definition ZeroArrowFrom (Z : Zero) (b : C) : Z --> b := pr1 (pr1 (pr2 Z) b). Lemma ArrowsFromZero (Z : Zero) (b : C) (f g : Z --> b) : f = g. Definition ZeroArrow (Z : Zero) (a b : C) : C⟦a, b⟧ := (ZeroArrowTo Z a) · (ZeroArrowFrom Z b). rewrite (ArrowsFromZero Z b g1 (ZeroArrowFrom Z b)). assert (e2 : inv_from_z_iso i · ZeroArrowFrom Z b = ZeroArrowFrom Z' b) by apply ArrowsFromZero. Arguments ZeroArrowFrom [C]{Z} b. + exact (i · (ZeroArrowFrom a)). apply ArrowsFromZero.