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. apply hset_struct_with_smash_closed_funspace_point. Qed.
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.