Definition total_category_Binproducts (Ps : BinProducts C) (dPs : dispBinProducts Ps) : BinProducts (total_category D). Proof. intros ccc ddd. use tpair. - apply (total_category_Binproducts_data Ps dPs). - induction ccc as [c cc]. induction ddd as [d dd]. intros aaa fff ggg. destruct aaa as [a aa]; destruct fff as [f ff]; destruct ggg as [g gg]. cbn. use unique_exists. + exact (total_category_Binproducts_mediating_morphism Ps dPs ff gg). + exact (total_category_Binproducts_mediating_morphism_ok Ps dPs ff gg). + intro y. apply isapropdirprod. * apply (homset_property (total_category D) (a ,, aa) (c ,, cc)). * apply (homset_property (total_category D) (a ,, aa) (d ,, dd)). + intro fgfgfg. induction fgfgfg as [fg fgfg]. exact (total_category_Binproducts_mediating_morphism_unique Ps dPs ff gg fgfg). 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.