proposition: Proposition bicat_to_triangle_law : triangle_law bicat_to_lunitor bicat_to_runitor bicat_to_associator.
proof: Proof. intros x y z f g ; cbn. rewrite <- !rwhisker_vcomp. rewrite !vassocr. do 3 apply maponpaths_2. rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite linvunitor_lunitor. rewrite id2_left. rewrite !vassocl. rewrite <- rinvunitor_triangle. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. rewrite id2_left. apply idpath. } rewrite !vassocr. rewrite lwhisker_vcomp. rewrite !vassocr. rewrite rinvunitor_runitor. rewrite id2_left. rewrite !vassocl. apply idpath. } rewrite runitor_rwhisker. rewrite lwhisker_vcomp. rewrite linvunitor_lunitor. rewrite lwhisker_id2. rewrite id2_right. rewrite !vassocr. apply maponpaths_2. rewrite runitor_triangle. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.Groupoids UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Strictness UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats