Definition hset_struct_type_prod_laws {P : hset_struct} {I : UU} (HP : hset_struct_type_prod_data P I) : UU := (∏ (D : I → hSet) (PD : ∏ (i : I), P (D i)) (i : I), mor_hset_struct P (HP D PD) (PD i) (λ f, f i)) × (∏ (D : I → hSet) (PD : ∏ (i : I), P (D i)) (W : hSet) (PW : P W) (fs : ∏ (i : I), W → D i) (Pfs : ∏ (i : I), mor_hset_struct P PW (PD i) (fs i)), mor_hset_struct P PW (HP D PD) (λ w i, fs i w)).
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.