Definition map_from_smash {Z : hSet} (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. Proof. use setquotuniv. - exact (λ xy, h (pr1 xy) (pr2 xy)). - abstract (intros xy₁ xy₂ ; use factor_through_squash ; [ apply setproperty | ] ; intro p ; induction p as [ p | p ] ; [ induction p ; apply idpath | ] ; induction p as [ p₁ p₂ ] ; induction xy₁ as [ x₁ y₁ ] ; induction xy₂ as [ x₂ y₂ ] ; induction p₁ as [ p₁ | p₁ ] ; induction p₂ as [ p₂ | p₂ ] ; cbn in * ; rewrite p₁, p₂ ; [ apply hp₁ | refine (!_) ; apply hp₂ | apply hp₂ | apply hp₃ ]). 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.