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. Proof. use map_from_smash. - exact h. - abstract (intros y₁ y₂ ; rewrite !hp₁ ; apply idpath). - abstract (intros x y ; rewrite hp₁, hp₂ ; apply idpath). - abstract (intros x₁ x₂ ; rewrite !hp₂ ; apply idpath). 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.