Proposition comp_v_profunctor_square_laws {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_laws (comp_v_profunctor_square_mor τ θ). Proof. intros z₁ z₂ x₁ x₂ k f h. cbn. use (mor_from_comp_profunctor_ob_eq P₁ Q₁ z₁ x₁ (λ h, comp_v_profunctor_square_mor τ θ z₂ x₂ (comp_profunctor_mor P₁ Q₁ k (identity x₂) (comp_profunctor_mor P₁ Q₁ (identity z₁) f h))) (λ h, comp_profunctor_mor P₂ Q₂ (# F₃ k) (identity (F₁ x₂)) (comp_profunctor_mor P₂ Q₂ (identity (F₃ z₁)) (# F₁ f) (comp_v_profunctor_square_mor τ θ z₁ x₁ h)))). clear h. intros y h h'. cbn. rewrite !comp_profunctor_mor_comm. etrans. { exact (comp_v_profunctor_square_mor_comm τ θ z₂ x₂ y _ _). } refine (!_). etrans. { do 2 apply maponpaths. exact (comp_v_profunctor_square_mor_comm τ θ z₁ x₁ y _ _). } rewrite !comp_profunctor_mor_comm. rewrite !lmap_id. rewrite !rmap_id. rewrite (profunctor_square_lmap θ). rewrite (profunctor_square_rmap τ). apply idpath. Qed.
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.