Definition dispCoproducts_hset_struct {P : hset_struct} {I : hSet} (HP : hset_struct_set_coprod P I) : disp_Coproducts (hset_struct_disp_cat P) I (CoproductsHSET I (pr2 I)). Proof. intros D DD. simple refine (_ ,, (_ ,, _)). - exact (HP D DD). - exact (hset_struct_set_coprod_in HP DD). - intros W PW fs Hf. use iscontraprop1. + abstract (use isaproptotal2 ; [ intro ; use impred ; intro ; apply hset_struct_disp_cat | ] ; intros ; apply isaprop_hset_struct_on_mor). + simple refine (_ ,, _). * exact (hset_struct_set_coprod_sum HP _ _ Hf). * intro i. 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.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.MonadAlgebras. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure.