Proposition double_cat_to_double_bicat_cylinder_laws : double_bicat_cylinder_laws double_cat_to_ver_bicat_sq_id_comp_whisker. Proof. repeat split. - intros ; cbn -[transportf_square]. etrans. { apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros ; cbn -[transportf_square]. etrans. { apply maponpaths. refine (!_). apply lassociator_square'. } rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros ; cbn -[transportf_square]. etrans. { apply maponpaths. apply square_id_left_v. } unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros ; cbn -[transportf_square]. refine (!_). etrans. { apply maponpaths. apply lunitor_square. } unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros ; cbn -[transportf_square]. etrans. { apply maponpaths. apply square_id_right_v. } unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros ; cbn -[transportf_square]. refine (!_). etrans. { apply maponpaths. apply runitor_square. } unfold transportb_square. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros x₁ x₂ y₁ y₂ z₁ z₂ v₁ v₂ v₃ h₁ h₁' h₂ h₂' k₁ k₁' k₂ k₂'. intros s₁ s₁' s₂ s₂' s₃ s₃' s₄ s₄' p q. cbn in *. pose (maponpaths (transportb_square (id_v_left v₁) (id_v_left v₂)) p) as p'. rewrite transportbf_square in p'. unfold transportb_square in p'. rewrite transportf_f_square in p'. clear p. pose (maponpaths (transportb_square (id_v_left v₂) (id_v_left v₃)) q) as q'. rewrite transportbf_square in q'. unfold transportb_square in q'. rewrite transportf_f_square in q'. clear q. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite <- !comp_h_square_comp. rewrite !square_id_left_v. rewrite !square_id_right_v. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite !transportf_square_postwhisker. rewrite p', q'. rewrite !transportf_f_square. etrans. { rewrite transportf_hcomp_l. rewrite !transportf_f_square. cbn. rewrite transportf_hcomp_r. rewrite !transportf_f_square. cbn -[transportf_square]. apply idpath. } refine (!_). etrans. { rewrite transportf_hcomp_l. rewrite !transportf_f_square. cbn. rewrite transportf_hcomp_r. rewrite !transportf_f_square. apply idpath. } use transportf_square_eq. apply maponpaths_2. use transportf_square_eq. apply idpath. - intros x₁ x₂ y₁ y₂ z₁ z₂ v₁ v₂ v₃ h₁ h₁' h₂ h₂' k₁ k₁' k₂ k₂'. intros p p' q q' s₁ s₁' s₂ s₂' r r'. cbn -[transportf_square] in *. induction p, p', q, q'. cbn in r, r'. induction r, r'. use transportf_square_eq. apply idpath. 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.Examples.DiscreteBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints. Require Import UniMath.Bicategories.DoubleCategories.Underlying.HorizontalBicategory.