Definition pointed_hset_struct_laws {P : hset_struct} (Pt : pointed_hset_struct_data P) : UU := (∏ (X Y : hSet) (PX : P X) (PY : P Y), mor_hset_struct P PX PY (λ _, hset_struct_point Pt PY)) × (∏ (X Y : hSet) (f : X → Y) (PX : P X) (PY : P Y) (Pf : mor_hset_struct P PX PY f), f (hset_struct_point Pt PX) = hset_struct_point Pt PY).
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.