Proposition hset_struct_pointwise (P : hset_cartesian_closed_struct_data) {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) (z : Z) : mor_hset_struct P PX PY (λ x : X, f (x ,, z)). Proof. exact (hset_struct_comp P (hset_struct_pair P (hset_struct_id P PX) (hset_struct_const P PX PZ z)) Pf). Qed.
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.