Proposition monoidal_laws_REL : monoidal_laws monoidal_data_REL. Proof. split6. - repeat split. + intros X Y ; cbn. use funextsec ; intro xy₁. induction xy₁ as [ x₁ y₁ ]. use funextsec ; intro xy₂. induction xy₂ as [ x₂ y₂ ] ; cbn. use hPropUnivalence. * intros p. use pathsdirprod. ** exact (pr1 p). ** exact (pr2 p). * intros p. split. ** exact (maponpaths dirprod_pr1 p). ** exact (maponpaths dirprod_pr2 p). + intros X Y ; cbn. use funextsec ; intro xy₁. induction xy₁ as [ x₁ y₁ ]. use funextsec ; intro xy₂. induction xy₂ as [ x₂ y₂ ] ; cbn. use hPropUnivalence. * intros p. use pathsdirprod. ** exact (pr2 p). ** exact (pr1 p). * intros p. split. ** exact (maponpaths dirprod_pr2 p). ** exact (maponpaths dirprod_pr1 p). + intros X Y₁ Y₂ Y₃ g₁ g₂. use funextsec ; intro xy₁. induction xy₁ as [ x₁ y₁ ]. use funextsec ; intro xy₂. induction xy₂ as [ x₂ y₂ ] ; cbn. use hPropUnivalence. * intros p. induction p as [ p q ]. induction p. use (factor_through_squash _ _ q) ; [ apply propproperty | ] ; clear q. intros [ y q ]. apply hinhpr. exact ((x₁ ,, y) ,, (idpath _ ,, pr1 q) ,, (idpath _ ,, pr2 q)). * use factor_through_squash ; [ apply propproperty | ]. intros [ y [ [ p₁ p₂ ] [ q₁ q₂ ]]] ; cbn in *. induction p₁, q₁. exact (idpath _ ,, hinhpr (pr2 y ,, p₂ ,, q₂)). + intros X Y₁ Y₂ Y₃ g₁ g₂. use funextsec ; intro xy₁. induction xy₁ as [ y₁ x₁ ]. use funextsec ; intro xy₂. induction xy₂ as [ y₂ x₂ ] ; cbn. use hPropUnivalence. * intros p. induction p as [ p q ]. induction p. use (factor_through_squash _ _ q) ; [ apply propproperty | ] ; clear q. intros [ y q ]. exact (hinhpr ((y ,, x₁) ,, ((idpath _ ,, pr1 q) ,, (idpath _ ,, pr2 q)))). * use factor_through_squash ; [ apply propproperty | ]. intros [ y [ [ p₁ p₂ ] [ q₁ q₂ ]]] ; cbn in *. induction p₁, q₁. exact (idpath _ ,, hinhpr (_ ,, p₂ ,, q₂)). + intros X₁ X₂ Y₁ Y₂ R₁ R₂. use funextsec ; intro xy₁. induction xy₁ as [ y₁ x₁ ]. use funextsec ; intro xy₂. induction xy₂ as [ y₂ x₂ ] ; cbn. use hPropUnivalence. * use factor_through_squash ; [ apply propproperty | ]. intros [ y [ [ p₁ p₂ ] [ q₁ q₂ ]]] ; cbn in *. induction p₁, q₁. exact (hinhpr ((_ ,, _) ,, ((idpath _ ,, q₂) ,, (idpath _ ,, p₂)))). * use factor_through_squash ; [ apply propproperty | ]. intros [ y [ [ p₁ p₂ ] [ q₁ q₂ ]]] ; cbn in *. induction p₁, q₁. exact (hinhpr ((_ ,, _) ,, ((idpath _ ,, q₂) ,, (idpath _ ,, p₂)))). - split. + intros X Y R. use funextsec ; intro x. induction x as [ [] x ]. use funextsec ; intro y. use hPropUnivalence. * use factor_through_squash ; [ apply propproperty | ]. intros [ [ [] y' ] [ [ p₁ p₂ ] p₃ ]] ; cbn in *. induction p₃. exact (hinhpr (x ,, (idpath _ ,, p₂))). * use factor_through_squash ; [ apply propproperty | ]. intros [ a [ p q ]] ; cbn in *. induction p. exact (hinhpr ((tt ,, y) ,, ((idpath _ ,, q) ,, idpath _))). + intros X. split. * use funextsec ; intro x. induction x as [ [] x ]. use funextsec ; intro x'. induction x' as [ [] x' ]. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros [ a [ p q ]] ; cbn in *. induction p, q. apply idpath. ** intro p ; cbn in *. refine (hinhpr (x' ,, _ ,, idpath _)). exact (maponpaths dirprod_pr2 p). * use funextsec ; intro x. use funextsec ; intro x'. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros [ a [ p q ]] ; cbn in *. induction p, q. apply idpath. ** intro p ; cbn in *. induction p. exact (hinhpr ((tt ,, x) ,, idpath _ ,, idpath _)). - split. + intros X Y R. use funextsec ; intro x. induction x as [ x [] ]. use funextsec ; intro y. use hPropUnivalence. * use factor_through_squash ; [ apply propproperty | ]. intros [ [ y' [] ] [ [ p₁ p₂ ] p₃ ]] ; cbn in *. induction p₃. exact (hinhpr (x ,, (idpath _ ,, p₂))). * use factor_through_squash ; [ apply propproperty | ]. intros [ a [ p q ]] ; cbn in *. induction p. exact (hinhpr ((y ,, tt) ,, ((idpath _ ,, q) ,, idpath _))). + intros X. split. * use funextsec ; intro x. induction x as [ x [] ]. use funextsec ; intro x'. induction x' as [ x' [] ]. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros [ a [ p q ]] ; cbn in *. induction p, q. apply idpath. ** intro p ; cbn in *. refine (hinhpr (x' ,, _ ,, idpath _)). exact (maponpaths dirprod_pr1 p). * use funextsec ; intro x. use funextsec ; intro x'. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros [ a [ p q ]] ; cbn in *. induction p, q. apply idpath. ** intro p ; cbn in *. induction p. exact (hinhpr ((x ,, tt) ,, idpath _ ,, idpath _)). - split4. + intros X Y Z₁ Z₂ R. use funextsec ; intro x. induction x as [ [ x y ] z ]. use funextsec ; intro x'. induction x' as [ x' [ y' z' ]]. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros ((a & b & c) & ( p₁ & p₂ & p₃ ) & ( p₄ & p₅ & p₆ )). cbn in *. induction p₁, p₂, p₃, p₄, p₅. refine (hinhpr (((x ,, y) ,, z') ,, _)). repeat split ; try (apply idpath). exact p₆. ** use factor_through_squash ; [ apply propproperty | ]. cbn. intros (((a & b) & c) & (p₁ & p₂) & p₃ & p₄ & p₅) ; cbn in *. induction p₃, p₄, p₅. refine (hinhpr ((x ,, y ,, z) ,, _)) ; cbn. repeat split ; try (apply idpath). *** exact (maponpaths dirprod_pr1 p₁). *** exact (maponpaths dirprod_pr2 p₁). *** exact p₂. + intros X Y₁ Y₂ Z R. use funextsec ; intro x. induction x as [ [ x y ] z ]. use funextsec ; intro x'. induction x' as [ x' [ y' z' ]]. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros ((a & b & c) & ((p₁ & p₂ & p₃) & (p₄ & p₅))) ; cbn in *. induction p₁, p₂, p₃. refine (hinhpr (((x' ,, y') ,, z) ,, _)) ; cbn. repeat split ; try (apply idpath). *** exact (maponpaths dirprod_pr1 p₄). *** exact p₅. *** exact (maponpaths dirprod_pr2 p₄). ** use factor_through_squash ; [ apply propproperty | ]. intros (((a & b) & c) & ((p₁ & p₂ & p₃) & (p₄ & p₅ & p₆))) ; cbn in *. induction p₁, p₂, p₄, p₅, p₆. refine (hinhpr ((x ,, y ,, z) ,, _)). repeat split ; try (apply idpath). exact p₃. + intros X₁ X₂ Y Z R. use funextsec ; intro x. induction x as [ [ x y ] z ]. use funextsec ; intro x'. induction x' as [ x' [ y' z' ]]. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros ((a & b & c) & ((p₁ & p₂ & p₃) & (p₄ & p₅ & p₆))) ; cbn in *. induction p₁, p₂, p₃, p₄, p₅. refine (hinhpr (((x ,, y') ,, z) ,, _)) ; cbn. repeat split ; try (apply idpath). exact p₆. ** use factor_through_squash ; [ apply propproperty | ]. intros (((a & b) & c) & ((p₁ & p₂ & p₃) & (p₄ & p₅ & p₆))) ; cbn in *. induction p₁, p₂, p₄, p₅, p₆. refine (hinhpr ((x ,, y ,, z) ,, _)). repeat split ; try (apply idpath). exact p₃. + intros X Y Z. split. * use funextsec ; intro x. induction x as [[ x y ] z ]. use funextsec ; intro x'. induction x' as [[ x' y' ] z' ]. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros ((a & b & c) & (p₁ & p₂ & p₃) & (p₄ & p₅ & p₆)) ; cbn in *. induction p₁, p₂, p₃, p₄, p₅, p₆. apply idpath. ** cbn ; intro p. refine (hinhpr ((x' ,, (y' ,, z')) ,, _)) ; cbn. repeat split ; try (apply idpath). *** exact (maponpaths dirprod_pr1 (maponpaths dirprod_pr1 p)). *** exact (maponpaths dirprod_pr2 (maponpaths dirprod_pr1 p)). *** exact (maponpaths dirprod_pr2 p). * use funextsec ; intro x. induction x as [ x [ y z ]]. use funextsec ; intro x'. induction x' as [ x' [ y' z' ]]. use hPropUnivalence. ** use factor_through_squash ; [ apply propproperty | ]. intros (((a & b) & c) & (p₁ & p₂ & p₃) & (p₄ & p₅ & p₆)) ; cbn in *. induction p₁, p₂, p₃, p₄, p₅, p₆. apply idpath. ** cbn ; intro p. refine (hinhpr (((x ,, y) ,, z) ,, _)) ; cbn. repeat split ; try (apply idpath). *** exact (maponpaths dirprod_pr1 p). *** exact (maponpaths dirprod_pr1 (maponpaths dirprod_pr2 p)). *** exact (maponpaths dirprod_pr2 (maponpaths dirprod_pr2 p)). - intros X Y. use funextsec ; intro x. induction x as [ [ x [] ] y ]. use funextsec ; intro x'. induction x' as [ x' y' ]. use hPropUnivalence. + use factor_through_squash ; [ apply propproperty | ] ; cbn. intros ( (a & [] & b) & ((p₁ & p₂ & p₃) & (p₄ & p₅)) ) ; cbn in *. induction p₁, p₃, p₄, p₅. split ; apply idpath. + intros [ p q ] ; cbn in *. induction p, q. refine (hinhpr ((x ,, (tt ,, y)) ,, _)) ; cbn. repeat split ; apply idpath. - intros W X Y Z. use funextsec ; intros (((w & x) & y) & z). use funextsec ; intros (w' & x' & y' & z'). use hPropUnivalence. + use factor_through_squash ; [ apply propproperty | ]. intros ((a & (b & c) & d) & (p₁ & p₂ & p₃ & p₄ & p₅)). cbn in p₂, p₃, p₄, p₅. induction p₂, p₃, p₄, p₅. use (factor_through_squash _ _ p₁) ; [ apply propproperty | ] ; clear p₁ ; cbn. intros (((a' & b' & c') & d') & ((p₁ & p₂ & p₃ & p₄) & (p₅ & p₆ & p₇))) ; cbn in *. induction p₁, p₂, p₃, p₄, p₅, p₇. refine (hinhpr (((w ,, x) ,, (y ,, z)) ,, _)) ; cbn. repeat split ; try (apply idpath). * exact (maponpaths dirprod_pr1 p₆). * apply maponpaths_2. exact (maponpaths dirprod_pr2 p₆). + use factor_through_squash ; [ apply propproperty | ]. intros (((a & b) & c & d) & ((p₁ & p₂ & p₃) & (p₄ & p₅ & p₆))) ; cbn in *. induction p₂, p₃, p₄, p₅. refine (hinhpr ((w ,, ((x ,, y) ,, z)) ,, hinhpr (((w ,, (x ,, y)) ,, z) ,, _) ,, _)) ; cbn ; repeat split. * exact (maponpaths dirprod_pr1 p₁). * exact (maponpaths dirprod_pr2 p₁). * exact (maponpaths dirprod_pr1 p₆). * exact (maponpaths dirprod_pr2 p₆). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Categories.Rel. Require Import UniMath.CategoryTheory.Adjunctions.Core. 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.