Proposition braiding_laws_one_hexagon_to_braiding_laws {C : category} {M : monoidal C} {B : braiding_data M} (H : braiding_laws_one_hexagon B) : braiding_laws B B. Proof. split4. - split. + exact (pr11 H). + exact (pr21 H). - exact (pr12 H). - exact (pr22 H). - intros x y z. pose (pr22 H z x y). rewrite !assoc'. use (z_iso_inv_on_right _ _ _ (z_iso_from_associator_iso M _ _ _)). cbn. use (z_iso_inv_on_right _ _ _ (braiding_laws_one_hexagon_braiding_z_iso H _ _)). cbn. refine (!(id_right _) @ _). use (z_iso_inv_on_right _ _ _ (z_iso_from_associator_iso M _ _ _)). cbn. rewrite !assoc. rewrite p. rewrite !assoc'. refine (!_). etrans. { do 2 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. refine (!(bifunctor_leftcomp M _ _ _ _ (B z y) (B y z)) @ _). etrans. { apply maponpaths. apply H. } apply (bifunctor_leftid M). } rewrite id_left. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (monoidal_associatorisolaw M). } rewrite id_left. refine (!(bifunctor_rightcomp M _ _ _ _ (B z x) (B x z)) @ _). etrans. { apply maponpaths. apply H. } apply (bifunctor_rightid M). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import BifunctorNotations. Import MonoidalNotations.