Definition dispBinProducts_hset_disp_struct : dispBinProducts (hset_struct_disp_cat P) BinProductsHSET. Proof. intros X Y PX PY. simple refine ((_ ,, (_ ,, _)) ,, _). - exact (hset_struct_prod P PX PY). - exact (hset_struct_pr1 P PX PY). - exact (hset_struct_pr2 P PX PY). - intros W f g PW Mf Mg ; cbn. use iscontraprop1. + abstract (use isaproptotal2 ; [ intro ; apply isapropdirprod ; apply hset_struct_disp_cat | ] ; intros ; apply isaprop_hset_struct_on_mor). + simple refine (_ ,, _ ,, _). * exact (hset_struct_pair P Mf Mg). * apply isaprop_hset_struct_on_mor. * apply isaprop_hset_struct_on_mor. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts.