Proposition enriched_profunctor_interchange {V : benabou_cosmos} {C₁ C₂ C₃ C₄ C₅ C₆ C₇ C₈ C₉ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} {E₃ : enrichment C₃ V} {E₄ : enrichment C₄ V} {E₅ : enrichment C₅ V} {E₆ : enrichment C₆ V} {E₇ : enrichment C₇ V} {E₈ : enrichment C₈ V} {E₉ : enrichment C₉ V} {P₁ : E₁ ↛e E₂} {P₂ : E₂ ↛e E₃} {Q₁ : E₄ ↛e E₅} {Q₂ : E₅ ↛e E₆} {R₁ : E₇ ↛e E₈} {R₂ : E₈ ↛e E₉} {F₁ : C₁ ⟶ C₄} {EF₁ : functor_enrichment F₁ E₁ E₄} {F₂ : C₄ ⟶ C₇} {EF₂ : functor_enrichment F₂ E₄ E₇} {G₁ : C₂ ⟶ C₅} {EG₁ : functor_enrichment G₁ E₂ E₅} {G₂ : C₅ ⟶ C₈} {EG₂ : functor_enrichment G₂ E₅ E₈} {H₁ : C₃ ⟶ C₆} {EH₁ : functor_enrichment H₁ E₃ E₆} {H₂ : C₆ ⟶ C₉} {EH₂ : functor_enrichment H₂ E₆ E₉} (τ₁ : enriched_profunctor_square EF₁ EG₁ P₁ Q₁) (τ₂ : enriched_profunctor_square EG₁ EH₁ P₂ Q₂) (θ₁ : enriched_profunctor_square EF₂ EG₂ Q₁ R₁) (θ₂ : enriched_profunctor_square EG₂ EH₂ Q₂ R₂) : comp_h_enriched_profunctor_square (comp_v_enriched_profunctor_square τ₁ τ₂) (comp_v_enriched_profunctor_square θ₁ θ₂) = comp_v_enriched_profunctor_square (comp_h_enriched_profunctor_square τ₁ θ₁) (comp_h_enriched_profunctor_square τ₂ θ₂). Proof. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intros y. rewrite !assoc. etrans. { apply maponpaths_2. apply comp_v_enriched_profunctor_square_mor_comm. } rewrite !assoc'. etrans. { apply maponpaths. apply (comp_v_enriched_profunctor_square_mor_comm θ₁ θ₂). } refine (!_). rewrite !assoc. etrans. { apply (comp_v_enriched_profunctor_square_mor_comm (comp_h_enriched_profunctor_square τ₁ θ₁) (comp_h_enriched_profunctor_square τ₂ θ₂)). } cbn. rewrite <- tensor_comp_mor. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.StandardProfunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Invertible. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorSquares. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Coend. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.CompositionProf. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.SquareComp. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Unitors. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Associators. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Whiskering. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.