Definition hset_coequalizer_struct_laws {P : hset_struct} (EP : hset_coequalizer_struct_data P) : UU := (∏ (X Y : hSet) (f g : X → Y) (PX : P X) (PY : P Y) (Pf : mor_hset_struct P PX PY f) (Pg : mor_hset_struct P PX PY g), mor_hset_struct P PY (hset_struct_coequalizer EP Pf Pg) (coequalizer_map_hSet f g)) × (∏ (X Y : hSet) (f g : X → Y) (PX : P X) (PY : P Y) (Pf : mor_hset_struct P PX PY f) (Pg : mor_hset_struct P PX PY g) (Z : hSet) (PZ : P Z) (h : Y → Z) (Ph : mor_hset_struct P PY PZ h) (q : (λ w, h(f w)) = (λ w, h(g w))), mor_hset_struct P (hset_struct_coequalizer EP Pf Pg) PZ (coequalizer_out_hSet f g h (eqtohomot q))).
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.