Definition map_from_smash' {Z : UU} (HZ : isaset Z) (h : X → Y → Z) (hp₁ : ∏ (y₁ y₂ : Y), h Px y₁ = h Px y₂) (hp₂ : ∏ (x : X) (y : Y), h x Py = h Px y) (hp₃ : ∏ (x₁ x₂ : X), h x₁ Py = h x₂ Py) : setquot smash_eqrel → Z := @map_from_smash (make_hSet Z HZ) h hp₁ hp₂ hp₃.
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.