Definition comp_v_profunctor_square {C₁ C₂ D₁ D₂ E₁ E₂ : category} {F₁ : C₁ ⟶ C₂} {F₂ : D₁ ⟶ D₂} {F₃ : E₁ ⟶ E₂} {P₁ : C₁ ↛ D₁} {Q₁ : D₁ ↛ E₁} {P₂ : C₂ ↛ D₂} {Q₂ : D₂ ↛ E₂} (τ : profunctor_square F₂ F₁ P₁ P₂) (θ : profunctor_square F₃ F₂ Q₁ Q₂) : profunctor_square F₃ F₁ (comp_profunctor P₁ Q₁) (comp_profunctor P₂ Q₂). Proof. use make_profunctor_square. - exact (λ z x, comp_v_profunctor_square_mor τ θ z x). - exact (comp_v_profunctor_square_laws τ θ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.Transformation.