Definition make_dispBinProduct_locally_prop (c d : C) (P : BinProduct C c d) (cc : D c) (dd : D d) (LP : locally_propositional D) (dBP_data : ∑ pp : D (BinProductObject _ P), (pp -->[BinProductPr1 _ P] cc) × (pp -->[BinProductPr2 _ P] dd)) (mediating : ∏ (a : C) (f : a --> c) (g : a --> d) (aa : D a) (ff : aa -->[f] cc) (gg : aa -->[g] dd), aa -->[ BinProductArrow C P f g] pr1 dBP_data) : dispBinProduct c d P cc dd. Proof. exists dBP_data. intro; intros. use tpair. - exists (mediating a f g aa ff gg). abstract (split; apply LP). - abstract (intro t; apply subtypePath; [intro; apply isapropdirprod; apply homsets_disp | 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.