fact: Definition map_from_smash_pt {Z : hSet} (PZ : P Z) (Pz := hset_struct_point Pt PZ) (h : X → Y → Z) (hp₁ : ∏ (y : Y), h Px y = Pz) (hp₂ : ∏ (x : X), h x Py = Pz) : setquot smash_eqrel → Z.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits