Proposition associator_profunctor_nat_trans_law {C₁ C₂ C₃ C₄ : category} (P₁ : C₁ ↛ C₂) (P₂ : C₂ ↛ C₃) (P₃ : C₃ ↛ C₄) : profunctor_nat_trans_law (associator_profunctor_nat_trans_mor P₁ P₂ P₃). Proof. intros z₁ z₂ w₁ w₂ f₄ f₁ h ; cbn. use (mor_from_comp_profunctor_ob_eq P₁ (comp_profunctor P₂ P₃) _ _ (λ h, associator_profunctor_nat_trans_mor P₁ P₂ P₃ z₂ w₂ (comp_profunctor_mor P₁ (comp_profunctor P₂ P₃) f₄ (identity w₂) (comp_profunctor_mor P₁ (comp_profunctor P₂ P₃) (identity z₁) f₁ h))) (λ h, comp_profunctor_mor (comp_profunctor P₁ P₂) P₃ f₄ (identity w₂) (comp_profunctor_mor (comp_profunctor P₁ P₂) P₃ (identity z₁) f₁ (associator_profunctor_nat_trans_mor P₁ P₂ P₃ z₁ w₁ h)))). clear h. intros x h kl ; cbn. use (mor_from_comp_profunctor_ob_eq P₂ P₃ z₁ x (λ kl, associator_profunctor_nat_trans_mor P₁ P₂ P₃ z₂ w₂ (comp_profunctor_mor P₁ (comp_profunctor P₂ P₃) f₄ (identity w₂) (comp_profunctor_mor P₁ (comp_profunctor P₂ P₃) (identity z₁) f₁ (comp_profunctor_ob_in P₁ (comp_profunctor P₂ P₃) x h kl)))) (λ kl, comp_profunctor_mor (comp_profunctor P₁ P₂) P₃ f₄ (identity w₂) (comp_profunctor_mor (comp_profunctor P₁ P₂) P₃ (identity z₁) f₁ (associator_profunctor_nat_trans_mor P₁ P₂ P₃ z₁ w₁ (comp_profunctor_ob_in P₁ (comp_profunctor P₂ P₃) x h kl))))). clear kl. intros y k l ; cbn. rewrite !comp_profunctor_mor_comm ; cbn. rewrite !comp_profunctor_mor_comm. rewrite !associator_profunctor_nat_trans_mor_comm. rewrite !rmap_id, !lmap_id. etrans. { exact (associator_profunctor_nat_trans_mor_ob_comm P₁ P₂ P₃ (rmap P₁ f₁ h) k (lmap P₃ f₄ l)). } refine (!_). etrans. { do 2 apply maponpaths. exact (associator_profunctor_nat_trans_mor_ob_comm P₁ P₂ P₃ h k l). } rewrite !comp_profunctor_mor_comm. cbn. rewrite lmap_id. rewrite !comp_profunctor_mor_comm. rewrite !lmap_id, !rmap_id. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. 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.