Definition make_Initial (a : C) (H : isInitial a) : Initial. Proof. use (make_ColimCocone _ a (initCocone a)). apply make_isInitial. intro b. set (x := H b (initCocone b)). use tpair. - apply (pr1 x). - simpl; intro f; apply path_to_ctr; intro v; induction v. 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.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.Initial. Lemma ArrowsFromInitial (I : Initial) (a : C) (f g : C⟦InitialObject I,a⟧) : f = g.