Definition hset_struct_smash_prod_mor_r (PX : ∁) {PY₁ PY₂ : ∁} (f : PY₁ --> PY₂) : PX ∧* PY₁ --> PX ∧* PY₂. Proof. simple refine (_ ,, _). - use map_from_smash. + exact (λ x y, setquotpr _ (x ,, pr1 f y)). + abstract (intros y₁ y₂ ; use iscompsetquotpr ; apply hinhpr ; cbn ; use inr ; exact (inl (idpath _) ,, inl (idpath _))). + abstract (intros x y ; use iscompsetquotpr ; apply hinhpr ; cbn ; use inr ; refine (inr _ ,, inl (idpath _)) ; apply pointed_hset_struct_preserve_point ; exact (pr2 f)). + abstract (intros x₁ x₂ ; use iscompsetquotpr ; apply hinhpr ; cbn ; use inr ; refine (inr _ ,, inr _) ; apply (pointed_hset_struct_preserve_point _ (pr2 f))). - abstract (apply hset_struct_with_smash_map_from_smash ; refine (hset_struct_comp P _ (hset_struct_with_smash_setquotpr _ (pr2 PX) (pr2 PY₂))) ; use hset_struct_pair ; [ apply hset_struct_pr1 | refine (hset_struct_comp P _ (pr2 f)) ; apply hset_struct_pr2 ]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal.