Definition univcat_profunctor_ver_bicat_sq_bicat_ver_id_comp_sq : ver_bicat_sq_bicat_ver_id_comp_sq univcat_profunctor_ver_bicat_sq_bicat. Proof. split. - exact (λ (C₁ C₂ : univalent_category) (F : C₁ ⟶ C₂), id_v_profunctor_square F). - exact (λ (C₁ C₂ C₃ D₁ D₂ D₃ : univalent_category) (F₁ : C₁ ⟶ D₁) (F₂ : C₂ ⟶ D₂) (F₃ : C₃ ⟶ D₃) (P₁ : C₁ ↛ C₂) (P₂ : C₂ ↛ C₃) (Q₁ : D₁ ↛ D₂) (Q₂ : D₂ ↛ D₃) (τ : profunctor_square F₂ F₁ P₁ Q₁) (θ : profunctor_square F₃ F₂ P₂ Q₂), comp_v_profunctor_square τ θ). 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.