Definition hset_struct_smash_prod_lassociator_mor_alt_fun {X Y Z : ∁} (xy : pr11 (X ∧* Y)) (z : pr11 Z) : pr11 (X ∧* Y ∧* Z). Proof. revert xy. use map_from_smash'. - apply setproperty. - exact (λ x y, setquotpr _ (x ,, setquotpr _ (y ,, z))). - abstract (intros y₁ y₂ ; use iscompsetquotpr ; apply hinhpr ; use inr ; unfold product_point_coordinate ; cbn ; split ; use inl ; apply idpath). - abstract (intros x y ; use iscompsetquotpr ; apply hinhpr ; use inr ; unfold product_point_coordinate ; split ; [ | use inl ; apply idpath ] ; use inr ; refine (_ @ !(hset_struct_with_smash_closed_point_smash _ _)) ; use iscompsetquotpr ; cbn ; apply hinhpr ; use inr ; unfold product_point_coordinate ; cbn ; split ; use inl ; apply idpath). - abstract (intros x₁ x₂ ; use iscompsetquotpr ; apply hinhpr ; use inr ; unfold product_point_coordinate ; split ; cbn ; use inr ; refine (_ @ !(hset_struct_with_smash_closed_point_smash _ _)) ; use iscompsetquotpr ; cbn ; apply hinhpr ; use inr ; unfold product_point_coordinate ; split ; cbn ; use inl ; apply idpath). 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.