Definition disp_BinCoproducts_hset_disp_struct {P : hset_struct} (EP : hset_binary_coprod_struct P) : disp_BinCoproducts (hset_struct_disp_cat P) BinCoproductsHSET. Proof. intros X Y PX PY. simple refine (_ ,, _ ,, _ ,, _). - exact (hset_struct_binary_coprod EP PX PY). - exact (hset_binary_coprod_struct_inl EP PX PY). - exact (hset_binary_coprod_struct_inr EP PX PY). - intros W PW f Pf g Pg. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply isasetaprop ; apply isaprop_hset_struct_on_mor | ] ; apply isaprop_hset_struct_on_mor). + simple refine (_ ,, _ ,, _). * exact (hset_binary_coprod_struct_sumofmaps EP Pf Pg). * 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.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.