Definition hset_binary_coprod_struct_laws {P : hset_struct} (EP : hset_binary_coprod_struct_data P) : UU := (∏ (X Y : hSet) (PX : P X) (PY : P Y), mor_hset_struct P PX (hset_struct_binary_coprod EP PX PY) inl) × (∏ (X Y : hSet) (PX : P X) (PY : P Y), mor_hset_struct P PY (hset_struct_binary_coprod EP PX PY) inr) × (∏ (X Y Z : hSet) (PX : P X) (PY : P Y) (PZ : P Z) (f : X → Z) (g : Y → Z) (Pf : mor_hset_struct P PX PZ f) (Pg : mor_hset_struct P PY PZ g), mor_hset_struct P (hset_struct_binary_coprod EP PX PY) PZ (sumofmaps f g)).
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.