proposition: Proposition horizontal_dual_double_bicat_cylinder_laws : double_bicat_cylinder_laws horizontal_dual_ver_bicat_sq_id_comp_whisker.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.UnivalenceOp UniMath.Bicategories.Core.Examples.OpMorBicat UniMath.Bicategories.Core.Examples.OpCellBicat UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence