Definition closed_under_fun_laws (P : hset_cartesian_closed_struct_data) : UU := (∏ (X Y : hSet) (PX : P X) (PY : P Y), mor_hset_struct P (hset_struct_prod P PX (hset_struct_fun P PX PY)) PY (λ xf, pr12 xf (pr1 xf))) × (∏ (X Y Z : hSet) (PX : P X) (PY : P Y) (PZ : P Z) (f : X × Z → Y) (Pf : mor_hset_struct P (hset_struct_prod P PX PZ) PY f), mor_hset_struct P PZ (hset_struct_fun P PX PY) (λ z, _ ,, hset_struct_pointwise P f Pf z)).
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.