Lemma equiv_isTerminal2 (c : C) : Limits.Terminal.isTerminal C c <- isTerminal c. Proof. intros X. set (XT := make_Terminal c X). intros b. use tpair. - exact (TerminalArrow XT b). - intros t. use (TerminalArrowUnique XT b). Qed.
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.