Proposition bicat_to_pentagon_law : pentagon_law bicat_to_associator. Proof. intros v w x y z f g h k ; cbn. rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite linvunitor_lunitor. rewrite id2_left. rewrite rinvunitor_runitor. rewrite id2_left. apply idpath. } refine (!_). etrans. { do 6 apply maponpaths. rewrite !vassocr. rewrite rinvunitor_runitor. rewrite id2_left. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite linvunitor_lunitor. rewrite id2_left. rewrite !vassocl. rewrite <- !rwhisker_vcomp. rewrite !vassocl. rewrite <- linvunitor_assoc. apply idpath. } rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite <- lassociator_lassociator. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite runitor_rwhisker. rewrite lwhisker_vcomp. rewrite !vassocl. rewrite linvunitor_lunitor. rewrite id2_right. rewrite <- !lwhisker_vcomp. rewrite !vassocr. rewrite runitor_triangle. rewrite !vassocl. do 2 apply maponpaths. etrans. { do 6 apply maponpaths. rewrite runitor_triangle. apply rinvunitor_runitor. } rewrite id2_right. rewrite !vassocr. refine (_ @ id2_left _). apply maponpaths_2. rewrite !vassocl. rewrite <- lunitor_triangle. etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. apply id2_left. } rewrite rwhisker_vcomp. rewrite !vassocl. rewrite linvunitor_lunitor. rewrite id2_right. rewrite runitor_rwhisker. rewrite lwhisker_vcomp. rewrite linvunitor_lunitor. apply lwhisker_id2. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Strictness. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats.