Definition bidisp_tensor_disp_prebicat_ops : disp_prebicat_ops bidisp_tensor_disp_prebicat_1_id_comp_cells. Proof. repeat split. - intros C D F TC TD ptF. apply identitynattrans_preservestensor_commutes. - intros C D F TC TD ptF. intros x y. rewrite id_right. simpl. rewrite tensor_id. rewrite id_left. unfold identityfunctor_preserves_tensor_data. unfold compositions_preserves_tensor_data. rewrite functor_id. apply id_right. - intros C D F TC TD ptF. intros x y. rewrite id_right. cbn. unfold compositions_preserves_tensor_data. unfold identityfunctor_preserves_tensor_data. rewrite id_left. simpl. rewrite tensor_id. rewrite id_left. apply idpath. - intros C D F TC TD ptF. intros x y. rewrite id_right. simpl. rewrite tensor_id. rewrite id_left. cbn. unfold compositions_preserves_tensor_data. cbn. unfold identityfunctor_preserves_tensor_data. rewrite functor_id. rewrite id_right. apply idpath. - intros C D F TC TD ptF. intros x y. rewrite id_right. cbn. rewrite tensor_id. unfold compositions_preserves_tensor_data. unfold identityfunctor_preserves_tensor_data. simpl. rewrite id_left. rewrite id_left. apply idpath. - intros C D E W F G H TC TD TE TW ptF ptG ptH. intros x y. simpl. rewrite id_right. rewrite tensor_id. rewrite id_left. cbn. unfold compositions_preserves_tensor_data. cbn. rewrite assoc'. rewrite functor_comp. apply idpath. - intros C D E W F G H TC TD TE TW ptF ptG ptH. intros x y. simpl. rewrite id_right. rewrite tensor_id. rewrite id_left. cbn. unfold compositions_preserves_tensor_data. cbn. rewrite assoc'. rewrite functor_comp. apply idpath. - intros C D F G H α β TC TD ptF ptG ptH ptcα ptcβ. intros x y. simpl. rewrite assoc. rewrite ptcα. rewrite assoc'. rewrite ptcβ. rewrite assoc. rewrite tensor_comp. apply idpath. - intros C D E F G H α TC TD TE ptF ptG ptH ptcα. intros x y. cbn. unfold compositions_preserves_tensor_data. rewrite assoc'. rewrite (pr2 α). rewrite assoc. rewrite ptcα. rewrite assoc. apply idpath. - intros C D E F G H α TC TD TE ptF ptG ptH ptcα. intros x y. cbn. unfold compositions_preserves_tensor_data. rewrite assoc'. etrans. { apply maponpaths. apply (pathsinv0 (functor_comp _ _ _)). } etrans. { do 2 apply maponpaths. apply ptcα. } rewrite assoc. rewrite functor_comp. rewrite assoc. apply cancel_postcomposition. etrans. { apply (pr2 ptH). } apply maponpaths. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import TensorNotation. Import TensorNotation.