Definition horizontal_dual_double_bicat_whiskering : double_bicat_whiskering horizontal_dual_ver_bicat_sq_bicat_ver_id_comp. Proof. repeat split. - exact (λ (w x y z : B) (h₁ : x --> w) (h₂ : z --> y) (v₁ v₁' : w -|-> y) (v₂ : x -|-> z) (τ : v₁' =|=> v₁) (s : square_double_bicat h₁ h₂ v₂ v₁'), τ ▹s s). - exact (λ (w x y z : B) (h₁ : x --> w) (h₂ : z --> y) (v₁ : w -|-> y) (v₂ v₂' : x -|-> z) (τ : v₂' =|=> v₂) (s : square_double_bicat h₁ h₂ v₂ v₁), τ ◃s s). - exact (λ (w x y z : B) (h₁ h₁' : x --> w) (h₂ : z --> y) (v₁ : w -|-> y) (v₂ : x -|-> z) (τ : h₁ ==> h₁') (s : square_double_bicat h₁' h₂ v₂ v₁), τ ▵s s). - exact (λ (w x y z : B) (h₁ : x --> w) (h₂ h₂' : z --> y) (v₁ : w -|-> y) (v₂ : x -|-> z) (τ : h₂ ==> h₂') (s : square_double_bicat h₁ h₂ v₂ v₁), τ ▿s 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.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.