proposition: Proposition hset_struct_set_coprod_sum {D : I → hSet} (PD : ∏ (i : I), P (D i)) {W : hSet} (PW : P W) {fs : ∏ (i : I), D i → W} (Pfs : ∏ (i : I), mor_hset_struct P (PD i) PW (fs i)) : mor_hset_struct P (HP D PD) PW (λ id, fs (pr1 id) (pr2 id)).
proof: Proof. exact (pr22 HP D PD W PW fs Pfs). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Binproducts UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure