proposition: Proposition bicat_to_lunitor_laws : double_lunitor_laws bicat_to_lunitor_data.
proof: Proof. intros x₁ x₂ y₁ y₂ f g p q s. induction p, q ; cbn. rewrite !vassocl. rewrite rinvunitor_runitor. rewrite id2_right. rewrite id2_rwhisker. rewrite id2_left. rewrite (maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)). rewrite lassociator_rassociator. rewrite id2_left. rewrite vcomp_lunitor. rewrite !vassocr. apply maponpaths_2. rewrite <- lunitor_triangle. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite <- vcomp_runitor. rewrite !vassocl. rewrite runitor_rinvunitor. apply id2_right. 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