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