Definition associator_profunctor_square {C₁ C₂ C₃ C₄ : category} (P₁ : C₁ ↛ C₂) (P₂ : C₂ ↛ C₃) (P₃ : C₃ ↛ C₄) : profunctor_square (functor_identity C₄) (functor_identity C₁) (comp_profunctor P₁ (comp_profunctor P₂ P₃)) (comp_profunctor (comp_profunctor P₁ P₂) P₃). Proof. use profunctor_nat_trans_to_square. exact (associator_profunctor_nat_trans P₁ P₂ P₃). 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.