Lemma dispTerminalArrowUnique' (P : Terminal C) (dP : dispTerminal P) {x : C} (xx : D x) (f: x --> TerminalObject P) (kk : xx -->[f] dispTerminalObject dP) : kk = transportb _ (TerminalArrowUnique P x f) (dispTerminalArrow P dP xx). Proof. apply transportf_transpose_right. apply dispTerminalArrowUnique. 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.