Lemma prebicat_laws_from_monoidal : prebicat_laws (prebicat_data_from_monoidal). Proof. split. { intros. apply id_left. } split. { intros. apply id_right. } split. { intros. apply assoc. } split. { intros ? ? ? f g. apply (bifunctor_leftid M). } split. { intros ? ? ? f g. apply (bifunctor_rightid M). } split. { intros ? ? ? f g h i x y. apply pathsinv0, (bifunctor_leftcomp M). } split. { intros ? ? ? f g h i x y. apply pathsinv0, (bifunctor_rightcomp M). } split. { intros. apply (leftunitorlaw_nat (monoidal_leftunitorlaw M)). } split. { intros. apply (rightunitorlaw_nat (monoidal_rightunitorlaw M)). } split. { intros ? ? ? ? f g h i x. cbn. apply pathsinv0. apply (z_iso_inv_on_right _ _ _ (_,,(_,,associatorlaw_iso_law (monoidal_associatorlaw M) f g h))). rewrite assoc. apply (z_iso_inv_on_left _ _ _ _ (_,,(_,,associatorlaw_iso_law (monoidal_associatorlaw M) f g i))). apply (associatorlaw_natleft (monoidal_associatorlaw M)). } split. { intros ? ? ? ? f g h i x. cbn. apply pathsinv0. apply (z_iso_inv_on_right _ _ _ (_,,(_,,associatorlaw_iso_law (monoidal_associatorlaw M) f g i))). rewrite assoc. apply (z_iso_inv_on_left _ _ _ _ (_,,(_,,associatorlaw_iso_law (monoidal_associatorlaw M) f h i))). apply (associatorlaw_natleftright (monoidal_associatorlaw M)). } split. { intros ? ? ? ? f g h i x. cbn. apply (z_iso_inv_on_right _ _ _ (_,,(_,,associatorlaw_iso_law (monoidal_associatorlaw M) f h i))). rewrite assoc. apply (z_iso_inv_on_left _ _ _ _ (_,,(_,,associatorlaw_iso_law (monoidal_associatorlaw M) g h i))). apply (associatorlaw_natright (monoidal_associatorlaw M)). } split. { intros. cbn. apply (bifunctor_equalwhiskers M). } split. { intros ? ? f. exact (pr1 (leftunitorlaw_iso_law (monoidal_leftunitorlaw M) f)). } split. { intros ? ? f. exact (pr2 (leftunitorlaw_iso_law (monoidal_leftunitorlaw M) f)). } split. { intros ? ? f. exact (pr1 (rightunitorlaw_iso_law (monoidal_rightunitorlaw M) f)). } split. { intros ? ? f. exact (pr2 (rightunitorlaw_iso_law (monoidal_rightunitorlaw M) f)). } split. { intros ? ? ? ? f g h. exact (pr2 (associatorlaw_iso_law (monoidal_associatorlaw M) f g h)). } split. { intros ? ? ? ? f g h. exact (pr1 (associatorlaw_iso_law (monoidal_associatorlaw M) f g h)). } split. { intros ? ? ? f g. apply (z_iso_inv_on_right _ _ _ (_,,(_,,associatorlaw_iso_law (monoidal_associatorlaw M) f I_{ M} g))). apply pathsinv0, monoidal_triangleidentity. } intros ? ? ? ? ? f g h i. cbn. apply monoidal_pentagon_identity_inv. 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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Section Bicat_From_Monoidal_Cat. Import Bicat.Notations. Import BifunctorNotations. Import MonoidalNotations. End Bicat_From_Monoidal_Cat.