Lemma ZeroArrowToUnique (Z : Zero) (c : C) (f : C⟦c, ZeroObject Z⟧) : f = (ZeroArrowTo Z c). Proof. apply (TerminalArrowUnique (Zero_to_Terminal Z) c f). 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.