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. induction (TerminalArrowEq f g). cbn. rewrite (dispTerminalArrowUnique' _ _ _ _ ff). rewrite (dispTerminalArrowUnique' _ _ _ _ gg). apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.