proposition: Lemma prebicat_laws_from_monoidal : prebicat_laws (prebicat_data_from_monoidal).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.whiskering UniMath.Bicategories.Core.Bicat