Lemma binprod_lassociator {a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : B} (f₁ : a₁ --> a₂) (g₁ : b₁ --> b₂) (f₂ : a₂ --> a₃) (g₂ : b₂ --> b₃) (f₃ : a₃ --> a₄) (g₃ : b₃ --> b₄) : f₁ ⊗₁ g₁ ◃ pair_1cell_comp f₂ f₃ g₂ g₃ • pair_1cell_comp f₁ (f₂ · f₃) g₁ (g₂ · g₃) • lassociator f₁ f₂ f₃ ⊗₂ lassociator g₁ g₂ g₃ = lassociator (f₁ ⊗₁ g₁) (f₂ ⊗₁ g₂) (f₃ ⊗₁ g₃) • (pair_1cell_comp f₁ f₂ g₁ g₂ ▹ f₃ ⊗₁ g₃) • pair_1cell_comp (f₁ · f₂) f₃ (g₁ · g₂) g₃. Proof. use binprod_ump_2cell_unique_alt. - apply (pr2 B). - rewrite <- !rwhisker_vcomp. rewrite !vassocl. etrans. { apply maponpaths. etrans. { apply maponpaths. apply pair_2cell_pr1. } apply maponpaths_2. apply binprod_ump_2cell_pr1. } rewrite !vassocl. etrans. { do 6 apply maponpaths. rewrite !vassocr. rewrite vcomp_linv. rewrite id2_left. apply idpath. } refine (!_). etrans. { apply maponpaths. apply maponpaths. apply binprod_ump_2cell_pr1. } rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths_2. apply maponpaths. apply binprod_ump_2cell_pr1. } rewrite <- !rwhisker_vcomp. rewrite !vassocl. do 5 apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite vcomp_linv. rewrite id2_rwhisker. apply id2_left. } refine (!_). etrans. { rewrite !vassocr. rewrite <- rwhisker_lwhisker_rassociator. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths_2. apply maponpaths. apply binprod_ump_2cell_pr1. } rewrite <- !lwhisker_vcomp. rewrite !vassocl. do 5 apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite vcomp_linv. rewrite lwhisker_id2. rewrite id2_left. rewrite !vassocl. apply idpath. } use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite rassociator_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { rewrite !vassocr. rewrite lwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite <- rassociator_rassociator. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite rassociator_lassociator. rewrite lwhisker_id2. rewrite id2_left. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { rewrite !vassocr. rewrite rwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite rassociator_rassociator. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } etrans. { rewrite !vassocr. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocl. apply idpath. } apply maponpaths. rewrite !vassocr. use vcomp_move_R_Mp ; [ is_iso | ] ; cbn. refine (!_). apply rassociator_rassociator. - rewrite <- !rwhisker_vcomp. rewrite !vassocl. etrans. { apply maponpaths. etrans. { apply maponpaths. apply pair_2cell_pr2. } apply maponpaths_2. apply binprod_ump_2cell_pr2. } rewrite !vassocl. etrans. { do 6 apply maponpaths. rewrite !vassocr. rewrite vcomp_linv. rewrite id2_left. apply idpath. } refine (!_). etrans. { apply maponpaths. apply maponpaths. apply binprod_ump_2cell_pr2. } rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths_2. apply maponpaths. apply binprod_ump_2cell_pr2. } rewrite <- !rwhisker_vcomp. rewrite !vassocl. do 5 apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite vcomp_linv. rewrite id2_rwhisker. apply id2_left. } refine (!_). etrans. { rewrite !vassocr. rewrite <- rwhisker_lwhisker_rassociator. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths_2. apply maponpaths. apply binprod_ump_2cell_pr2. } rewrite <- !lwhisker_vcomp. rewrite !vassocl. do 5 apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite vcomp_linv. rewrite lwhisker_id2. rewrite id2_left. rewrite !vassocl. apply idpath. } use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite rassociator_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { rewrite !vassocr. rewrite lwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite <- rassociator_rassociator. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite rassociator_lassociator. rewrite lwhisker_id2. rewrite id2_left. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { rewrite !vassocr. rewrite rwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite rassociator_rassociator. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } etrans. { rewrite !vassocr. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocl. apply idpath. } apply maponpaths. rewrite !vassocr. use vcomp_move_R_Mp ; [ is_iso | ] ; cbn. refine (!_). apply rassociator_rassociator. Qed.
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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.