Proposition REL_braiding_laws : sym_mon_cat_laws_tensored REL_monoidal_cat REL_braiding. Proof. repeat split. - intros X Y. 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 y as [ a b ] ; cbn in *. induction p₁, p₂, q₁, q₂. apply idpath. + intros p. refine (hinhpr ((_ ,, _) ,, ((idpath _ ,, idpath _) ,, (_ ,, _)))) ; cbn. * exact (maponpaths dirprod_pr2 p). * exact (maponpaths dirprod_pr1 p). - 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₂ ]. use hPropUnivalence. + use factor_through_squash ; [ apply propproperty | ]. intros [ [ a b ] [ p [ q₁ q₂ ]]] ; cbn in q₁, q₂. induction q₁, q₂. use (factor_through_squash _ _ p) ; [ apply propproperty | ] ; cbn ; clear p. intros [ [ c d ] [ [ p₁ p₂ ] [ q₁ q₂ ] ]]. apply hinhpr ; cbn in *. induction p₁, q₁. refine ((x₁ ,, y₁) ,, ((idpath _ ,, idpath _) ,, hinhpr _)) ; cbn. refine ((b ,, y₁) ,, ((idpath _ ,, _) ,, (idpath _ ,, _))) ; cbn. * exact q₂. * exact p₂. + use factor_through_squash ; [ apply propproperty | ]. intros [ [ a b ] [ [ p₁ p₂ ] q]] ; cbn in p₁, p₂. induction p₁, p₂. use (factor_through_squash _ _ q) ; [ apply propproperty | ] ; cbn ; clear q. intros [ [ c d ] [ [ p₁ p₂ ] [ q₁ q₂ ] ]]. apply hinhpr ; cbn in *. induction p₁, q₁. refine ((x₂ ,, c) ,, (hinhpr _ ,, (idpath _ ,, idpath _))) ; cbn. refine ((x₂ ,, x₁) ,, ((idpath _ ,, _) ,, (idpath _ ,, _))) ; cbn. * exact q₂. * exact p₂. - intros X Y Z. use funextsec ; intro xy₁. induction xy₁ as [ [ x₁ y₁ ] z₁ ]. use funextsec ; intro xy₂. induction xy₂ as [ y₂ [ z₂ x₂ ]]. use hPropUnivalence. + use factor_through_squash ; [ apply propproperty | ]. intros ( ((y & z) & x) & q & p₁ & p₂ & p₃). cbn in p₁, p₂, p₃. induction p₁, p₂, p₃. use (factor_through_squash _ _ q) ; [ apply propproperty | ] ; cbn ; clear q. intros ( (a & b & c) & ( p₁ & ( p₂ & p₃ ) ) & ( p₄ & p₅ ) ). cbn in *. induction p₁, p₂, p₃, p₄. refine (hinhpr ((y ,, x₁ ,, z) ,, hinhpr _ ,, hinhpr _)). * refine (((y ,, x₁) ,, z) ,, hinhpr (((y ,, x₁) ,, z) ,, _) ,, _) ; repeat split ; try (apply idpath) ; cbn. ** exact (maponpaths dirprod_pr2 p₅). ** exact (maponpaths dirprod_pr1 p₅). * refine ((y ,, (x₁ ,, z)) ,, ((_ ,, _) ,, (_ ,, (_ ,, _)))) ; apply idpath. + use factor_through_squash ; [ apply propproperty | ]. intros ((a & b & c) & (p₁ & p₂)). use (factor_through_squash _ _ p₁) ; [ apply propproperty | ] ; clear p₁. intros (((a' & b') & c') & (q₁ & q₂ & q₃ & q₄)). cbn in q₂, q₃, q₄. induction q₂, q₃, q₄. use (factor_through_squash _ _ p₂) ; [ apply propproperty | ] ; clear p₂. intros ((a'' & b'' & c'') & ((r₁ & r₂) & (r₃ & r₄ & r₅))). cbn in r₁, r₂, r₃, r₄, r₅. induction r₂, r₃, r₄, r₅. use (factor_through_squash _ _ q₁) ; [ apply propproperty | ] ; clear q₁. intros (((a''' & b''') & c''') & ((s₁ & s₂ & s₃) & s₄ & s₅)) ; cbn in *. induction s₁, s₂, s₃, s₅. refine (hinhpr (((y₁ ,, z₁) ,, x₁) ,, hinhpr ((x₁ ,, (y₁ ,, z₁)) ,, _) ,, _)) ; cbn ; repeat split ; try (apply idpath). * exact (maponpaths dirprod_pr1 s₄). * exact (maponpaths dirprod_pr2 r₁). * exact (maponpaths dirprod_pr2 s₄ @ maponpaths dirprod_pr1 r₁). 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.