proposition: Proposition hset_struct_with_smash_closed_fun_point {PC : hset_struct_with_smash_closed} (PX PY : category_of_hset_struct PC) (x : pr11 PX) : pr1 (hset_struct_point PC (pr2 (PX -->* PY))) x = hset_struct_point PC (pr2 PY).
proof: Proof. apply hset_struct_with_smash_closed_funspace_point. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits