Definition make_dispTerminal_locally_prop (P : Terminal C) (LP : locally_propositional D) (dTO_data : D (TerminalObject P)) (mediating : ∏ (a : C) (aa : D a), aa -->[TerminalArrow P a] dTO_data) : dispTerminal P. Proof. exists dTO_data. intro; intros. use tpair. - exact (mediating a aa). - intro; apply LP. 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.