Definition double_cat_to_double_bicat_whiskering : double_bicat_whiskering double_cat_to_ver_bicat_sq_bicat_ver_id_comp. Proof. repeat split. - exact (λ (w x y z : C) (v₁ : w -->v x) (v₂ : y -->v z) (h₁ h₁' : w -->h y) (h₂ : x -->h z) (s₁ : square (identity_v w) (identity_v y) h₁ h₁') (s₂ : square v₁ v₂ h₁' h₂), transportf_square (id_v_left _) (id_v_left _) (s₁ ⋆v s₂)). - exact (λ (w x y z : C) (v₁ : w -->v x) (v₂ : y -->v z) (h₁ : w -->h y) (h₂ h₂' : x -->h z) (s₁ : square (identity_v _) (identity_v _) h₂ h₂') (s₂ : square v₁ v₂ h₁ h₂), transportf_square (id_v_right _) (id_v_right _) (s₂ ⋆v s₁)). - exact (λ (w x y z : C) (v₁ v₁' : w -->v x) (v₂ : y -->v z) (h₁ : w -->h y) (h₂ : x -->h z) (p : v₁ = v₁') (s : square v₁' v₂ h₁ h₂), transportf_square (!p) (idpath _) s). - exact (λ (w x y z : C) (v₁ : w -->v x) (v₂ v₂' : y -->v z) (h₁ : w -->h y) (h₂ : x -->h z) (p : v₂ = v₂') (s : square v₁ v₂ h₁ h₂), transportf_square (idpath _) p s). Defined.
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.