Lemma isiso_from_Zero_to_Zero (Z Z' : Zero) : is_iso (ZeroArrowFrom Z (ZeroObject Z')). Proof. apply (is_iso_qinv _ (ZeroArrowFrom Z' (ZeroObject Z))). split; apply ArrowsFromZero. Defined.
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.