Definition make_isTerminal (b : C) (H : ∏ (a : C), iscontr (a --> b)) : isTerminal b. Proof. intros a ca. use tpair. - exists (pr1 (H a)); intro v; induction v. - intro t. apply subtypePath; simpl; [ intro f; apply impred; intro v; induction v|]. apply (pr2 (H a)). 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.Limits. Require Import UniMath.CategoryTheory.Limits.Terminal.