Definition hset_struct_set_coprod_laws {P : hset_struct} {I : hSet} (HP : hset_struct_set_coprod_data P I) : UU := (∏ (D : I → hSet) (PD : ∏ (i : I), P (D i)) (i : I), mor_hset_struct P (PD i) (HP D PD) (λ d, i ,, d)) × (∏ (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))).
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.