Definition hset_struct_smash_curry_fun {P : hset_cartesian_struct} {Pt : pointed_hset_struct P} {SP : hset_struct_with_smash P Pt} (PC : hset_struct_with_smash_closed_pointed SP) {PX PY PZ : category_of_hset_struct P} (f : PX --> hset_struct_with_smash_closed_to_funspace PC PY PZ) : setquot (smash_hrel P Pt (pr2 PX) (pr2 PY)) → pr11 PZ. Proof. use map_from_smash. - exact (λ x y, pr1 (pr1 f x) y). - abstract (intros y₁ y₂ ; cbn ; rewrite !(pointed_hset_struct_preserve_point Pt (pr2 f)) ; refine (pr2 PC _ _ _ _ _ @ !_) ; exact (pr2 PC _ _ _ _ _)). - abstract (intros x y ; cbn ; rewrite !(pointed_hset_struct_preserve_point Pt (pr2 f)) ; refine (_ @ !(pr2 PC _ _ _ _ _)) ; exact (pointed_hset_struct_preserve_point Pt (pr2 (pr1 f x)))). - abstract (intros x₁ x₂ ; cbn ; refine (pointed_hset_struct_preserve_point Pt (pr2 (pr1 f x₁)) @ !_) ; refine (pointed_hset_struct_preserve_point Pt (pr2 (pr1 f x₂)))). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.