Definition total_category_Terminal (P : Terminal C) (dP : dispTerminal P) : Terminal (total_category D). Proof. use tpair. - exists (TerminalObject P). exact (dispTerminalObject dP). - intros aaa. destruct aaa as [a aa]. cbn. use tpair. + exact (TerminalArrow P a,, dispTerminalArrow P dP aa). + intro fff. induction fff as [f ff]. use total2_paths_f; cbn. * apply TerminalArrowUnique. * apply dispTerminalArrowUnique. Defined.
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.