proposition: Lemma Initial_and_Terminal_ob_equals_Zero_ob (I : Initial C) (T :Terminal C) (e : iso (InitialObject I) (TerminalObject T)) : (iso (InitialObject I) (ZeroObject (Initial_and_Terminal_to_Zero I T e))) × (iso (TerminalObject T) (ZeroObject (Initial_and_Terminal_to_Zero I T e))).
proof: Proof. exact(identity_iso (InitialObject I),,iso_inv_from_iso e). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Initial UniMath.CategoryTheory.Limits.Graphs.Terminal UniMath.CategoryTheory.Limits.Zero