proposition: Lemma dispTerminalArrowEq {T : Terminal C} {TT: dispTerminal T} {a : C} {aa : D a} {f g : a --> T} (ff: aa -->[f] dispTerminalObject TT) (gg: aa -->[g] dispTerminalObject TT) : ff = transportb _ (TerminalArrowEq f g) gg.
proof: Proof. induction (TerminalArrowEq f g). cbn. rewrite (dispTerminalArrowUnique' _ _ _ _ ff). rewrite (dispTerminalArrowUnique' _ _ _ _ gg). apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total