Proposition horizontal_dual_double_bicat_cylinder_laws : double_bicat_cylinder_laws horizontal_dual_ver_bicat_sq_id_comp_whisker. Proof. repeat split. - intro ; intros ; cbn. etrans. { apply maponpaths. apply lassociator_h_comp_square''. } rewrite <- dwhisker_square_comp. rewrite lassociator_rassociator. apply dwhisker_square_id. - intro ; intros ; cbn. etrans. { apply maponpaths. apply lassociator_v_comp_square'. } rewrite <- rwhisker_lwhisker_square. rewrite <- rwhisker_square_comp. rewrite (lassociator_rassociator (C := 𝕍)). apply rwhisker_square_id. - intro ; intros ; cbn. apply runitor_h_comp_square. - intro ; intros ; cbn. refine (!_). etrans. { apply maponpaths. apply lunitor_v_comp_square'. } rewrite rwhisker_lwhisker_square. rewrite <- lwhisker_square_comp. rewrite (linvunitor_lunitor (C := 𝕍)). apply lwhisker_square_id. - intro ; intros ; cbn. apply lunitor_h_comp_square. - intro ; intros ; cbn. refine (!_). etrans. { apply maponpaths. apply runitor_v_comp_square'. } rewrite rwhisker_lwhisker_square. rewrite <- lwhisker_square_comp. rewrite (rinvunitor_runitor (C := 𝕍)). apply lwhisker_square_id. - intros x₁ x₂ y₁ y₂ z₁ z₂ h₁ h₂ h₃ v₁ v₁' v₂ v₂'. intros w₁ w₁' w₂ w₂' τ₁ τ₂ θ₁ θ₂ s₁ s₁' s₂ s₂' p q ; cbn. rewrite <- !(vcomp_whisker (C := 𝕍)). exact (!(ver_bicat_hcomp_v_comp_square B _ _ _ _ _ _ _ _ (!p) (!q))). - intros x₁ x₂ y₁ y₂ z₁ z₂ h₁ h₂ h₃ v₁ v₁' v₂ v₂'. intros w₁ w₁' w₂ w₂' τ₁ τ₂ θ₁ θ₂ s₁ s₁' s₂ s₂' p q ; cbn. rewrite <- !vcomp_whisker. exact (hor_bicat_hcomp_h_comp_square B _ _ _ _ _ _ _ _ q p). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence.