Definition hset_struct_smash_prod_mor_l (PY : ∁) {PX₁ PX₂ : ∁} (f : PX₁ --> PX₂) : PX₁ ∧* PY --> PX₂ ∧* PY. Proof. simple refine (_ ,, _). - use map_from_smash. + exact (λ x y, setquotpr _ (pr1 f x ,, y)). + abstract (intros y₁ y₂ ; use iscompsetquotpr ; apply hinhpr ; cbn ; use inr ; refine (inl _ ,, inl _) ; apply (pointed_hset_struct_preserve_point _ (pr2 f))). + abstract (intros x y ; use iscompsetquotpr ; apply hinhpr ; cbn ; use inr ; refine (inr (idpath _) ,, inl _) ; apply pointed_hset_struct_preserve_point ; exact (pr2 f)). + abstract (intros x₁ x₂ ; use iscompsetquotpr ; apply hinhpr ; cbn ; use inr ; exact (inr (idpath _) ,, inr (idpath _))). - 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 ; [ refine (hset_struct_comp P _ (pr2 f)) ; apply hset_struct_pr1 | 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.