Proposition double_cat_to_whisker_square_bicat_law : whisker_square_bicat_law double_cat_to_ver_bicat_sq_id_comp_whisker. Proof. repeat split. - intros w x y z v₁ v₂ h₁ h₂ s ; cbn in *. etrans. { apply maponpaths. apply square_id_left_v. } unfold transportb_square. rewrite transportf_f_square. apply transportf_square_id. - intros w x y z v₁ v₂ h₁ h₁' h₁'' h₂ s₁ s₂ s₃. cbn in *. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. refine (!_). etrans. { do 2 apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_f_square. use transportf_square_eq. apply idpath. - intros w x y z v₁ v₂ h₁ h₂ s ; cbn in *. etrans. { apply maponpaths. apply square_id_right_v. } unfold transportb_square. rewrite transportf_f_square. apply transportf_square_id. - intros w x y z v₁ v₂ h₁ h₂ h₂' h₂'' s₁ s₂ s₃. cbn in *. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. etrans. { do 2 apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_f_square. use transportf_square_eq. apply idpath. - intros w x y z v₁ v₂ h₁ h₂ s. cbn in *. apply transportf_square_id. - intros w x y z v₁ v₁' v₁'' v₂ h₁ h₂ p q s. cbn in *. induction p, q ; cbn. apply transportf_square_id. - intros w x y z v₁ v₂ h₁ h₂ s. cbn -[transportf_square] in *. apply transportf_square_id. - intros w x y z v₁ v₂ v₂' v₂'' h₁ h₂ p q s. cbn -[transportf_square] in *. induction p, q. cbn -[transportf_square]. apply transportf_square_id. - intros w x y z v₁ v₁' v₂ v₂' h₁ h₂ p q s. cbn -[transportf_square] in *. induction p, q. rewrite !transportf_f_square. use transportf_square_eq. apply idpath. - intros w x y z v₁ v₁' v₂ h₁ h₁' h₂ p s₁ s₂. cbn in *. induction p. cbn. use transportf_square_eq. apply idpath. - intros w x y z v₁ v₁' v₂ h₁ h₂ h₂' p s₁ s₂. cbn in *. induction p ; cbn. use transportf_square_eq. apply idpath. - intros w x y z v₁ v₂ v₂' h₁ h₁' h₂ p s₁ s₂. cbn in *. induction p ; cbn. use transportf_square_eq. apply idpath. - intros w x y z v₁ v₂ v₂' h₁ h₂ h₂' p s₁ s₂. cbn in *. induction p ; cbn. use transportf_square_eq. apply idpath. - intros w x y z v₁ v₂ h₁ h₁' h₂ h₂' s₁ s₂ s₃. cbn in *. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. refine (!_). etrans. { do 2 apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_f_square. use transportf_square_eq. apply idpath. - intros x y h k s. cbn in *. etrans. { apply maponpaths. apply square_id_right_v. } refine (!_). etrans. { apply maponpaths. apply square_id_left_v. } unfold transportb_square. rewrite !transportf_f_square. use transportf_square_eq. apply idpath. - intros x y h k p. cbn in *. induction p ; cbn. apply idpath. - intros x₁ x₂ y₁ y₂ z₁ z₂ v₁ v₁' v₂ v₃ h₁ h₂ k₁ k₂ p s₁ s₂. cbn in *. induction p ; cbn. apply idpath. - intros x₁ x₂ y₁ y₂ z₁ z₂ v₁ v₂ v₃ v₃' h₁ h₂ k₁ k₂ p s₁ s₂. cbn in *. induction p ; cbn. apply idpath. - intros x₁ x₂ y₁ y₂ z₁ z₂ v₁ v₂ v₂' v₃ h₁ h₂ k₁ k₂ p s₁ s₂. cbn in *. induction p ; cbn. apply idpath. - intros x₁ x₂ x₃ y₁ y₂ y₃ v₁ v₂ w₁ w₂ h₁ h₁' h₂ h₃ s₁ s₂ s₃. cbn in *. rewrite transportf_square_prewhisker. etrans. { apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_f_square. use transportf_square_eq. apply idpath. - intros x₁ x₂ x₃ y₁ y₂ y₃ v₁ v₂ w₁ w₂ h₁ h₂ h₃ h₃' s₁ s₂ s₃. cbn in *. rewrite transportf_square_postwhisker. refine (!_). etrans. { apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_f_square. use transportf_square_eq. apply idpath. - intros x₁ x₂ x₃ y₁ y₂ y₃ v₁ v₂ w₁ w₂ h₁ h₂ h₂' h₃ s₁ s₂ s₃. cbn in *. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. etrans. { apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_f_square. 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.