Proposition bicat_to_hor_comp_laws : hor_comp_laws bicat_to_hor_comp_data. Proof. split. - intros x y z f g ; cbn. rewrite <- lwhisker_vcomp. rewrite !vassocr. rewrite runitor_triangle. rewrite !vassocl. apply maponpaths. rewrite <- rwhisker_vcomp. rewrite !vassocl. rewrite <- linvunitor_assoc. rewrite !vassocr. refine (_ @ id2_left _). apply maponpaths_2. rewrite !vassocl. rewrite runitor_rwhisker. rewrite lwhisker_vcomp. rewrite linvunitor_lunitor. rewrite lwhisker_id2. apply idpath. - intros x₁ x₂ x₃ y₁ y₂ y₃ z₁ z₂ z₃ p₁ p₂ p₃ p₄ p₅ p₆ f₁ f₂ g₁ g₂ h₁ h₂ s₁ s₂ s₃ s₄. induction p₁, p₂, p₃, p₄, p₅, p₆ ; cbn. rewrite !vassocl. apply maponpaths. rewrite <- lwhisker_vcomp. rewrite !vassocl. apply maponpaths. rewrite !vassocr. apply maponpaths_2. rewrite <- rwhisker_vcomp. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. refine (!_). etrans. { do 2 apply maponpaths. rewrite <- lunitor_triangle. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite <- rinvunitor_triangle. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. rewrite id2_left. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. apply maponpaths_2. rewrite rwhisker_vcomp. rewrite !vassocl. rewrite lwhisker_vcomp. rewrite vcomp_whisker. apply idpath. } rewrite !vassocl. rewrite <- rwhisker_rwhisker. rewrite vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. rewrite <- vcomp_lunitor. rewrite <- !lwhisker_vcomp. rewrite !vassocl. do 2 apply maponpaths. refine (!_). etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite rinvunitor_natural. rewrite <- rwhisker_hcomp. apply idpath. } rewrite <- !rwhisker_vcomp. rewrite !vassocr. do 2 apply maponpaths_2. refine (_ @ lassociator_lassociator _ _ _ _). rewrite <- lunitor_triangle. rewrite <- lwhisker_vcomp. rewrite !vassocl. apply maponpaths. rewrite <- rinvunitor_triangle. rewrite <- rwhisker_vcomp. rewrite !vassocr. apply maponpaths_2. rewrite rwhisker_lwhisker. rewrite !vassocl. rewrite rwhisker_vcomp. rewrite lwhisker_vcomp. rewrite lunitor_runitor_identity. rewrite runitor_rinvunitor. rewrite lwhisker_id2. rewrite id2_rwhisker. apply id2_right. 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.