Lemma ArrowsToTerminal (T : Terminal) (b : C) (f g : C⟦b,TerminalObject T⟧) : f = g. Proof. eapply pathscomp0. apply TerminalArrowUnique. now apply pathsinv0, TerminalArrowUnique. 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.