Definition initial_from_empty_coproduct (C : category): Coproduct empty C fromempty -> Initial C. Proof. intros X. use (make_Initial (CoproductObject _ _ X)). use make_isInitial. intros b. assert (H : ∏ i : empty, C⟦fromempty i, b⟧) by (intros i; apply (fromempty i)). apply (make_iscontr (CoproductArrow _ _ X H)). abstract (intros t; apply CoproductArrowUnique; intros i; apply (fromempty i)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Coproducts.