Proposition smash_product_monoidal_laws : monoidal_laws smash_product_monoidal_data. Proof. repeat split. - intros X Y. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros x. use iscompsetquotpr. apply hinhpr ; cbn. use inl. apply idpath. - intros X Y. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros x. use iscompsetquotpr. apply hinhpr ; cbn. use inl. apply idpath. - intros W X Y Z g₁ g₂. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros x. use iscompsetquotpr. apply hinhpr ; cbn. use inl. apply idpath. - intros W X Y Z f₁ f₂. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros x. use iscompsetquotpr. apply hinhpr ; cbn. use inl. apply idpath. - intros X₁ X₂ Y₁ Y₂ f g. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros x. use iscompsetquotpr. apply hinhpr ; cbn. use inl. apply idpath. - intros X Y f. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros x. induction x as [ b x ]. cbn in *. induction b. + apply idpath. + refine (!_). apply pointed_hset_struct_preserve_point. exact (pr2 f). - use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intro z. induction z as [ b z ]. use iscompsetquotpr. apply hinhpr ; cbn. induction b ; cbn. + use inl. apply idpath. + use inr. split ; unfold product_point_coordinate ; cbn. * use inr. apply idpath. * use inl. rewrite hset_struct_with_smash_point_unit. apply idpath. - use eq_mor_hset_struct. intro z ; cbn. apply idpath. - intros X Y f. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros x. induction x as [ x b ]. cbn in *. induction b. + apply idpath. + refine (!_). apply pointed_hset_struct_preserve_point. exact (pr2 f). - use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intro z. induction z as [ z b ]. use iscompsetquotpr. apply hinhpr ; cbn. induction b ; cbn. + use inl. apply idpath. + use inr. split ; unfold product_point_coordinate ; cbn. * use inl. apply idpath. * use inr. rewrite hset_struct_with_smash_point_unit. apply idpath. - use eq_mor_hset_struct. intro z ; cbn. apply idpath. - intros X Y Z₁ Z₂ h. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intro z. induction z as [ xx y ]. revert xx. use setquotunivprop'. { intro. apply setproperty. } intro xx. induction xx as [ x₁ x₂ ]. use iscompsetquotpr ; cbn. apply hinhpr. use inl. apply idpath. - intros X₁ X₂ Y Z f. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intro z. induction z as [ xx y ]. revert xx. use setquotunivprop'. { intro. apply setproperty. } intro xx. induction xx as [ x₁ x₂ ]. use iscompsetquotpr ; cbn. apply hinhpr. use inl. apply idpath. - intros X Y₁ Y₂ Z g. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intro z. induction z as [ xx y ]. revert xx. use setquotunivprop'. { intro. apply setproperty. } intro xx. induction xx as [ x₁ x₂ ]. use iscompsetquotpr ; cbn. apply hinhpr. use inl. apply idpath. - use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intro xyz. induction xyz as [ xy z' ]. revert xy. use setquotunivprop'. { intro. apply setproperty. } intro xy. induction xy as [ x' y' ]. use iscompsetquotpr. apply hinhpr ; cbn. use inl. apply idpath. - use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intro xyz. induction xyz as [ x' yz ]. revert yz. use setquotunivprop'. { intro. apply setproperty. } intro yz. induction yz as [ y' z' ]. use iscompsetquotpr. apply hinhpr ; cbn. use inl. apply idpath. - intros X Y. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros xby. induction xby as [ xb y ]. revert xb. use setquotunivprop'. { intro. apply setproperty. } intros xb. induction xb as [ x b ]. use iscompsetquotpr ; cbn. apply hinhpr. induction b. + exact (inl (idpath _)). + use inr. unfold product_point_coordinate ; cbn. split. * exact (inr (idpath _)). * exact (inl (idpath _)). - intros W X Y Z. use eq_mor_hset_struct. use setquotunivprop'. { intro. apply setproperty. } intros wxyz. induction wxyz as [ wxy z ]. revert wxy. use setquotunivprop'. { intro. apply setproperty. } intros wxy. induction wxy as [ wx y ]. revert wx. use setquotunivprop'. { intro. apply setproperty. } intros wx. induction wx as [ w x ]. use iscompsetquotpr ; cbn. apply hinhpr. use inl. apply idpath. Qed.
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.