Lemma equiv_ZeroArrow (x y : C) (Z : Zero) : @Limits.Zero.ZeroArrow C (equiv_Zero2 Z) x y = ZeroArrow Z x y. Proof. unfold Limits.Zero.ZeroArrow. unfold ZeroArrow. rewrite equiv_ZeroArrowTo. rewrite equiv_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.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Initial. Require Import UniMath.CategoryTheory.Limits.Graphs.Terminal. Require Import UniMath.CategoryTheory.Limits.Zero. Definition ZeroArrowFrom (Z : Zero) (c : C) : C⟦ZeroObject Z, c⟧ := @compose C _ (ZeroObject Z) _ (ZeroArrowTo Z c) (ZeroArrowFrom Z d). Lemma ZeroArrowFromUnique (Z : Zero) (c : C) (f : C⟦ZeroObject Z, c⟧) : f = (ZeroArrowFrom Z c). Corollary ArrowsFromZero (Z : Zero) (c : C) (f g : C⟦ZeroObject Z, c⟧) : apply (ZeroArrowFromUnique Z c f). apply (ZeroArrowFromUnique Z c g). rewrite (ZeroArrowFromUnique Z d g). apply ArrowsFromZero. is_iso (ZeroArrowFrom Z (ZeroObject Z')). apply (is_iso_qinv _ (ZeroArrowFrom Z' (ZeroObject Z))). split; apply ArrowsFromZero. tpair _ (ZeroArrowFrom Z (ZeroObject Z')) (isiso_from_Zero_to_Zero Z Z'). Lemma equiv_ZeroArrowFrom (x : C) (Z : Zero) : @Limits.Zero.ZeroArrowFrom C (equiv_Zero2 Z) x = ZeroArrowFrom Z x. apply ZeroArrowFromUnique. rewrite equiv_ZeroArrowFrom.