Definition smash_product_monoidal_cat_braiding (X Y : category_of_hset_struct P) : X ∧* Y --> Y ∧* X. Proof. simple refine (_ ,, _). - use map_from_smash. + exact (λ x y, setquotpr _ (y ,, x)). + abstract (intros y₁ y₂ ; use iscompsetquotpr ; apply hinhpr ; use inr ; split ; use inr ; apply idpath). + abstract (intros x y ; use iscompsetquotpr ; apply hinhpr ; use inr ; split ; [ use inl | use inr ] ; apply idpath). + abstract (intros x₁ x₂ ; use iscompsetquotpr ; apply hinhpr ; use inr ; split ; use inl ; apply idpath). - apply hset_struct_with_smash_map_from_smash. refine (hset_struct_comp P _ (hset_struct_with_smash_setquotpr _ (pr2 Y) (pr2 X))). use hset_struct_pair. + apply hset_struct_pr2. + apply hset_struct_pr1. 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.