Lemma equiv_isZero2 (c : C) : Limits.Zero.isZero c <- isZero c. Proof. intros X. set (XZ := make_Zero c X). split. - intros b. use tpair. apply (InitialArrow (Zero_to_Initial XZ) b). intros t. use (InitialArrowUnique (Zero_to_Initial XZ) b). - intros a. use tpair. apply (TerminalArrow (Zero_to_Terminal XZ) a). intros t. use (TerminalArrowUnique (Zero_to_Terminal XZ) a). 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.