Proposition bicat_to_runitor_laws : double_runitor_laws bicat_to_runitor_data. Proof. intros x₁ x₂ y₁ y₂ f g p q s. induction p, q ; cbn. rewrite !vassocl. rewrite lwhisker_id2. rewrite id2_left. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. rewrite (maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)). rewrite linvunitor_lunitor. rewrite id2_left. rewrite (maponpaths (λ z, _ • z) (vassocr _ _ _)). rewrite runitor_rinvunitor. rewrite id2_left. rewrite (maponpaths (λ z, _ • (_ • (_ • z))) (vassocr _ _ _)). rewrite rinvunitor_runitor. rewrite id2_left. refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite <- lunitor_triangle. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite vcomp_runitor. rewrite !vassocl. rewrite lunitor_linvunitor. apply id2_right. } rewrite vcomp_runitor. apply idpath. 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.