proposition: Lemma equiv_isTerminal2 (c : C) : Limits.Terminal.isTerminal C c <- isTerminal c.
proof: Proof. intros X. set (XT := make_Terminal c X). intros b. use tpair. - exact (TerminalArrow XT b). - intros t. use (TerminalArrowUnique XT b). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Terminal