Definition univcat_profunctor_ver_sq_bicat_id_comp_cells : ver_sq_bicat_id_comp_cells univcat_profunctor_ver_sq_bicat_ver_id_comp. Proof. repeat split. - exact (λ (C₁ C₂ : univalent_category) (P : C₁ ↛ C₂), profunctor_nat_trans_id P). - exact (λ (C₁ C₂ : univalent_category) (P : C₁ ↛ C₂), lunitor_profunctor_nat_trans P). - exact (λ (C₁ C₂ : univalent_category) (P : C₁ ↛ C₂), runitor_profunctor_nat_trans P). - exact (λ (C₁ C₂ : univalent_category) (P : C₁ ↛ C₂), linvunitor_profunctor_nat_trans P). - exact (λ (C₁ C₂ : univalent_category) (P : C₁ ↛ C₂), rinvunitor_profunctor_nat_trans P). - exact (λ (C₁ C₂ C₃ C₄ : univalent_category) (P : C₁ ↛ C₂) (Q : C₂ ↛ C₃) (R : C₃ ↛ C₄), inv_associator_profunctor_nat_trans P Q R). - exact (λ (C₁ C₂ C₃ C₄ : univalent_category) (P : C₁ ↛ C₂) (Q : C₂ ↛ C₃) (R : C₃ ↛ C₄), associator_profunctor_nat_trans P Q R). - exact (λ (C₁ C₂ : univalent_category) (P Q R : C₁ ↛ C₂) (τ : profunctor_nat_trans P Q) (θ : profunctor_nat_trans Q R), profunctor_nat_trans_comp τ θ). - exact (λ (C₁ C₂ C₃ : univalent_category) (P : C₁ ↛ C₂) (Q₁ Q₂ : C₂ ↛ C₃) (τ : profunctor_nat_trans Q₁ Q₂), lwhisker_profunctor_nat_trans P τ). - exact (λ (C₁ C₂ C₃ : univalent_category) (P₁ P₂ : C₁ ↛ C₂) (Q : C₂ ↛ C₃) (τ : profunctor_nat_trans P₁ P₂), rwhisker_profunctor_nat_trans τ Q). 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.