Definition Initial_and_Terminal_to_Zero (I : Initial C) (T : Terminal C) (e: iso (InitialObject I) (TerminalObject T)) : Zero. Proof. use (make_Zero (InitialObject I)). split. - use (make_isInitial (InitialObject I)); intro b. apply make_iscontr with (x := (InitialArrow I b)), InitialArrowUnique. - use (make_isTerminal (InitialObject I)); intro a. apply (iscontrretract (postcomp_with (inv_from_iso e)) (postcomp_with (morphism_from_iso e))). intros y. unfold postcomp_with. rewrite <- assoc. rewrite (iso_inv_after_iso e). apply (remove_id_right _ _ _ y y _ (idpath _) (idpath _)). apply (make_iscontr (TerminalArrow T a)), TerminalArrowUnique. 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.