Proposition enriched_profunctor_square_comp_cylinder_down {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₃} {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₅} {F₇ F₈ : C₅ ⟶ C₆} {EF₇ : functor_enrichment F₇ E₅ E₆} {EF₈ : functor_enrichment F₈ E₅ E₆} {P₁ : enriched_profunctor E₁ E₄} {P₂ : enriched_profunctor E₂ E₅} {P₃ : enriched_profunctor E₃ E₆} {τ₁ : F₂ ⟹ F₁} {Eτ₁ : nat_trans_enrichment τ₁ EF₂ EF₁} {τ₂ : F₄ ⟹ F₃} {Eτ₂ : nat_trans_enrichment τ₂ EF₄ EF₃} {θ₁ : F₆ ⟹ F₅} {Eθ₁ : nat_trans_enrichment θ₁ EF₆ EF₅} {θ₂ : F₈ ⟹ pr1 F₇} {Eθ₂ : nat_trans_enrichment θ₂ EF₈ EF₇} (s₁ : enriched_profunctor_square EF₁ EF₅ P₁ P₂) (s₁' : enriched_profunctor_square EF₂ EF₆ P₁ P₂) (s₂ : enriched_profunctor_square EF₃ EF₇ P₂ P₃) (s₂' : enriched_profunctor_square EF₄ EF₈ P₂ P₃) (p : dwhisker_enriched_profunctor_square Eθ₁ s₁ = uwhisker_enriched_profunctor_square Eτ₁ s₁') (q : dwhisker_enriched_profunctor_square Eθ₂ s₂ = uwhisker_enriched_profunctor_square Eτ₂ s₂') (H₁ : nat_trans_enrichment (nat_trans_comp (F₆ ∙ F₈) (F₆ ∙ F₇) (F₅ ∙ F₇) (pre_whisker F₆ θ₂) (post_whisker θ₁ F₇)) (functor_comp_enrichment EF₆ EF₈) (functor_comp_enrichment EF₅ EF₇)) (H₂ : nat_trans_enrichment (nat_trans_comp (F₂ ∙ F₄) (F₂ ∙ F₃) (F₁ ∙ F₃) (pre_whisker F₂ τ₂) (post_whisker τ₁ F₃)) (functor_comp_enrichment EF₂ EF₄) (functor_comp_enrichment EF₁ EF₃)) : dwhisker_enriched_profunctor_square H₁ (comp_h_enriched_profunctor_square s₁ s₂) = uwhisker_enriched_profunctor_square H₂ (comp_h_enriched_profunctor_square s₁' s₂'). Proof. use eq_enriched_profunctor_transformation ; intros z x ; cbn. etrans. { rewrite !assoc'. do 2 apply maponpaths. rewrite enriched_from_arr_comp. rewrite !tensor_comp_id_r. rewrite !assoc'. rewrite lmap_e_comp'. rewrite !assoc. do 2 apply maponpaths_2. etrans. { apply maponpaths_2. rewrite !assoc'. rewrite <- tensor_comp_id_r. rewrite tensor_sym_mon_braiding. rewrite tensor_comp_id_r. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite <- tensor_comp_id_r. rewrite sym_mon_braiding_linvunitor. apply idpath. } rewrite !assoc'. rewrite tensor_lassociator. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite <- mon_inv_triangle. apply idpath. } rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite tensor_linvunitor. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. etrans. { do 2 apply maponpaths_2. apply maponpaths. apply tensor_split'. } rewrite !assoc. etrans. { do 3 apply maponpaths_2. rewrite <- tensor_split. apply tensor_split'. } rewrite !assoc'. apply maponpaths. rewrite !assoc. apply maponpaths_2. rewrite <- !tensor_comp_id_l. apply maponpaths. rewrite (functor_enrichment_from_arr EF₇). rewrite tensor_linvunitor. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_split. rewrite tensor_comp_r_id_l. rewrite !assoc'. apply maponpaths. exact (enriched_profunctor_square_lmap_e s₂ (F₅ z) (F₆ z) (F₁ x)). } etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. apply idpath. } etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_linvunitor. rewrite !assoc'. do 3 apply maponpaths. rewrite !assoc. exact (from_eq_enriched_profunctor_transformation q (F₆ z) (F₁ x)). } cbn. etrans. { rewrite !assoc. do 4 apply maponpaths_2. exact (from_eq_enriched_profunctor_transformation p z x). } cbn. rewrite !assoc'. apply maponpaths. etrans. { do 2 apply maponpaths. rewrite !assoc. do 3 apply maponpaths_2. exact (!(enriched_profunctor_square_rmap_e s₂' (F₆ z) (F₂ x) (F₁ x))). } etrans. { rewrite !assoc. do 4 apply maponpaths_2. rewrite (tensor_split _ (s₂' _ _)) ; cbn. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc. rewrite <- tensor_linvunitor. apply idpath. } rewrite !assoc'. do 2 apply maponpaths. rewrite enriched_from_arr_comp. etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite tensor_linvunitor. rewrite <- mon_linvunitor_triangle. rewrite !assoc'. apply maponpaths. etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split. rewrite tensor_split'. rewrite <- tensor_id_id. apply idpath. } rewrite !assoc. rewrite <- tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. exact (!(rmap_e_comp P₃ (F₈(F₆ z)) (F₄(F₂ x)) (F₄(F₁ x)) (F₃(F₁ x)))). } rewrite !assoc. apply maponpaths_2. rewrite <- !tensor_comp_id_r. apply maponpaths_2. rewrite (functor_enrichment_from_arr EF₃). rewrite tensor_comp_r_id_l. rewrite !assoc. rewrite mon_linvunitor_I_mon_rinvunitor_I. rewrite <- tensor_rinvunitor. rewrite !assoc'. apply maponpaths. rewrite !assoc. refine (_ @ !(Eτ₂ _ _)). apply maponpaths_2. rewrite tensor_linvunitor. rewrite !assoc'. rewrite <- tensor_split. 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.