Proposition enriched_profunctor_square_comp_cylinder_left {V : benabou_cosmos} {C₁ : category} {E₁ : enrichment C₁ V} {C₂ : category} {E₂ : enrichment C₂ V} {C₃ : category} {E₃ : enrichment C₃ V} {C₄ : category} {E₄ : enrichment C₄ V} {C₅ : category} {E₅ : enrichment C₅ V} {C₆ : category} {E₆ : enrichment C₆ V} {F₁ : C₁ ⟶ C₂} {EF₁ : functor_enrichment F₁ E₁ E₂} {F₂ : C₃ ⟶ C₄} {EF₂ : functor_enrichment F₂ E₃ E₄} {F₃ : C₅ ⟶ C₆} {EF₃ : functor_enrichment F₃ E₅ E₆} {P₁ P₂ : enriched_profunctor E₁ E₃} {P₁' P₂' : enriched_profunctor E₃ E₅} {Q₁ Q₂ : enriched_profunctor E₂ E₄} {Q₁' Q₂' : enriched_profunctor E₄ E₆} (τ₁ : enriched_profunctor_transformation P₁ P₂) (τ₂ : enriched_profunctor_transformation P₁' P₂') (θ₁ : enriched_profunctor_transformation Q₁ Q₂) (θ₂ : enriched_profunctor_transformation Q₁' Q₂') (s₁ : enriched_profunctor_square EF₁ EF₂ P₁ Q₁) (s₁' : enriched_profunctor_square EF₁ EF₂ P₂ Q₂) (s₂ : enriched_profunctor_square EF₂ EF₃ P₁' Q₁') (s₂' : enriched_profunctor_square EF₂ EF₃ P₂' Q₂') (p : lwhisker_enriched_profunctor_square τ₁ s₁' = rwhisker_enriched_profunctor_square θ₁ s₁) (q : lwhisker_enriched_profunctor_square τ₂ s₂' = rwhisker_enriched_profunctor_square θ₂ s₂) : lwhisker_enriched_profunctor_square (enriched_profunctor_comp_transformation (rwhisker_enriched_profunctor τ₁ P₁') (lwhisker_enriched_profunctor P₂ τ₂)) (comp_v_enriched_profunctor_square s₁' s₂') = rwhisker_enriched_profunctor_square (enriched_profunctor_comp_transformation (rwhisker_enriched_profunctor θ₁ Q₁') (lwhisker_enriched_profunctor Q₂ θ₂)) (comp_v_enriched_profunctor_square s₁ s₂). Proof. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intro y. etrans. { rewrite !assoc. do 2 apply maponpaths_2. apply rwhisker_enriched_profunctor_mor_comm. } etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. apply maponpaths_2. apply lwhisker_enriched_profunctor_mor_comm. } rewrite !assoc'. etrans. { do 2 apply maponpaths. apply comp_v_enriched_profunctor_square_mor_comm. } refine (!_). etrans. { rewrite !assoc. do 2 apply maponpaths_2. apply comp_v_enriched_profunctor_square_mor_comm. } rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (rwhisker_enriched_profunctor_mor_comm θ₁). } etrans. { rewrite !assoc'. do 2 apply maponpaths. apply lwhisker_enriched_profunctor_mor_comm. } rewrite !assoc. apply maponpaths_2. rewrite <- !tensor_comp_mor. rewrite !id_left, !id_right. pose (from_eq_enriched_profunctor_transformation p y x) as p'. pose (from_eq_enriched_profunctor_transformation q z y) as q'. cbn in p', q'. refine (!_). etrans. { apply maponpaths_2. exact p'. } apply maponpaths. exact q'. 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.