Definition hset_equalizer_struct_laws {P : hset_struct} (EP : hset_equalizer_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 (hset_struct_equalizer EP Pf Pg) PX pr1) × (∏ (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) (W : hSet) (PW : P W) (h : W → X) (Ph : mor_hset_struct P PW PX h) (q : (λ w, f(h w)) = (λ w, g(h w))), mor_hset_struct P PW (hset_struct_equalizer EP Pf Pg) (λ w, h w ,, eqtohomot q 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.