Definition make_isInitial (a : C) (H : ∏ (b : C), iscontr (a --> b)) : isInitial a. Proof. intros b cb. use tpair. - exists (pr1 (H b)); intro v; induction v. - intro t. apply subtypePath; simpl; [intro; apply impred; intro v; induction v|]. apply (pr2 (H b)). 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.