Definition univcat_profunctor_double_bicat_whiskering : double_bicat_whiskering univcat_profunctor_ver_bicat_sq_bicat_ver_id_comp. Proof. repeat split. - exact (λ (C₁ C₂ C₃ C₄ : univalent_category) (F : C₁ ⟶ C₂) (G : C₃ ⟶ C₄) (P₁ P₂ : C₁ ↛ C₃) (Q : C₂ ↛ C₄) (τ : profunctor_nat_trans P₁ P₂) (s : profunctor_square G F P₂ Q), lwhisker_profunctor_square τ s). - exact (λ (C₁ C₂ C₃ C₄ : univalent_category) (F : C₁ ⟶ C₂) (G : C₃ ⟶ C₄) (P : C₁ ↛ C₃) (Q₁ Q₂ : C₂ ↛ C₄) (τ : profunctor_nat_trans Q₁ Q₂) (s : profunctor_square G F P Q₁), rwhisker_profunctor_square τ s). - exact (λ (C₁ C₂ C₃ C₄ : univalent_category) (F₁ F₂ : C₁ ⟶ C₂) (G : C₃ ⟶ C₄) (P : C₁ ↛ C₃) (Q : C₂ ↛ C₄) (τ : F₂ ⟹ F₁) (s : profunctor_square G F₂ P Q), uwhisker_profunctor_square τ s). - exact (λ (C₁ C₂ C₃ C₄ : univalent_category) (F : C₁ ⟶ C₂) (G₁ G₂ : C₃ ⟶ C₄) (P : C₁ ↛ C₃) (Q : C₂ ↛ C₄) (τ : G₂ ⟹ G₁) (s : profunctor_square G₁ F P Q), dwhisker_profunctor_square τ s). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Categories.HSET.SetCoends. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Squares. Require Import UniMath.CategoryTheory.Profunctors.Transformation. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ProfunctorTwosidedDispCat. 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.OpCellBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.