From 672e72f93458e75c2494cd0bc6f2bcdf0f6dcb5d Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 11:17:43 -0600
Subject: [PATCH 01/40] feat(CategoryTheory): define profunctors

---
 Mathlib.lean                                 |   1 +
 Mathlib/CategoryTheory/Profunctor/Basic.lean | 150 +++++++++++++++++++
 2 files changed, 151 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Profunctor/Basic.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 374808d80ee064..16f59e19c97341 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3181,6 +3181,7 @@ public import Mathlib.CategoryTheory.Products.Associator
 public import Mathlib.CategoryTheory.Products.Basic
 public import Mathlib.CategoryTheory.Products.Bifunctor
 public import Mathlib.CategoryTheory.Products.Unitor
+public import Mathlib.CategoryTheory.Profunctor.Basic
 public import Mathlib.CategoryTheory.Quotient
 public import Mathlib.CategoryTheory.Quotient.Linear
 public import Mathlib.CategoryTheory.Quotient.LocallySmall
diff --git a/Mathlib/CategoryTheory/Profunctor/Basic.lean b/Mathlib/CategoryTheory/Profunctor/Basic.lean
new file mode 100644
index 00000000000000..5e6fd55887f63f
--- /dev/null
+++ b/Mathlib/CategoryTheory/Profunctor/Basic.lean
@@ -0,0 +1,150 @@
+/-
+Copyright (c) 2026 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson, Adam Topaz, Adrian Marti
+-/
+module
+
+public import Mathlib.CategoryTheory.Yoneda
+
+/-!
+
+# Profunctors
+
+A profunctor from a category `C` to a category `D` is a functor from `C` to a category of
+presheaves of sets on `D`. We define this as `Profunctor.{w} C D := C ⥤ Dᵒᵖ ⥤ Type w`.
+
+This file provides convenient constructors `ProfunctorCore` and `ProfunctorCore.Hom` for profunctors
+and natural transformations between them. We also define the identity profunctor `Profunctor.id`
+as the Yoneda bifunctor, the opposite of a profunctor, the `ulift` of a profunctor, whiskering
+of a profunctor with functors, and the profunctors in both directions corresponding to a functor
+`C ⥤ D` (see `Functor.toProfunctor` and `Functor.toProfunctorFlip`).
+
+## Future work
+
+- Define composition of profunctors.
+- Define the bicategory of categories where the 1-cells are profunctors.
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Opposite
+
+universe w' w
+
+variable (C D : Type*) [Category* C] [Category* D]
+
+/-- Custom structure to construct profunctors, i.e. bifunctors `C ⥤ Dᵒᵖ ⥤ Type w`. -/
+@[pp_with_univ]
+structure ProfunctorCore where
+  /-- The object part -/
+  obj : C → D → Type w
+  /-- The morphism part -/
+  map {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') : obj X Y' ⟶ obj X' Y
+  map_id (X : C) (Y : D) : map (𝟙 X) (𝟙 Y) = 𝟙 _ := by cat_disch
+  map_comp {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) :
+    map (f ≫ f') (g ≫ g') = map f g' ≫ map f' g := by cat_disch
+
+attribute [simp] ProfunctorCore.map_id ProfunctorCore.map_comp
+
+/-- A profunctor from C to D (`Profunctor.{w} C D`) is a bifunctor `C ⥤ Dᵒᵖ ⥤ Type w`. -/
+@[pp_with_univ]
+abbrev Profunctor := C ⥤ Dᵒᵖ ⥤ Type w
+
+variable {C D}
+
+/-- Typecheck a bifunctor `C ⥤ Dᵒᵖ ⥤ Type w` as a profunctor. -/
+abbrev Functor.profunctor (F : C ⥤ Dᵒᵖ ⥤ Type w) : Profunctor.{w} C D := F
+
+namespace ProfunctorCore
+
+/-- Custom structure to construct natural transformations between profunctors. -/
+structure Hom (P Q : ProfunctorCore.{w} C D) where
+  /-- The components of the natural transformation -/
+  app (X : C) (Y : D) : P.obj X Y ⟶ Q.obj X Y
+  naturality ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y') :
+    P.map f g ≫ app X' Y = app X Y' ≫ Q.map f g := by cat_disch
+
+attribute [reassoc (attr := simp)] ProfunctorCore.Hom.naturality
+
+@[simp]
+lemma map_id_comp (P : ProfunctorCore.{w} C D) (X : C) {Y Y' Y'' : D}
+    (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
+    P.map (𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g := by
+  nth_rw 1 [← Category.id_comp (𝟙 X)]
+  simp only [P.map_comp]
+
+@[simp]
+lemma map_comp_id (P : ProfunctorCore.{w} C D) {X X' X'' : C} (Y : D)
+    (f : X ⟶ X') (f' : X' ⟶ X'') :
+    P.map (f ≫ f') (𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y) := by
+  nth_rw 1 [← Category.id_comp (𝟙 Y)]
+  simp only [P.map_comp]
+
+@[reassoc (attr := simp)]
+lemma map_lid_comp_map_rid (P : ProfunctorCore.{w} C D) {X X' : C} {Y Y' : D}
+    (f : X ⟶ X') (g : Y ⟶ Y') : P.map (𝟙 _) g ≫ P.map f (𝟙 _) = P.map f g := by
+  simp [← P.map_comp]
+
+@[reassoc (attr := simp)]
+lemma map_rid_comp_map_lid (P : ProfunctorCore.{w} C D) {X X' : C} {Y Y' : D}
+    (f : X ⟶ X') (g : Y ⟶ Y') : P.map f (𝟙 _) ≫ P.map (𝟙 _) g = P.map f g := by
+  simp [← P.map_comp]
+
+end ProfunctorCore
+
+namespace Profunctor
+
+/-- Construct a profunctor from a `ProfunctorCore`. -/
+@[simps]
+def ofCore (P : ProfunctorCore.{w} C D) : Profunctor.{w} C D where
+  obj X := { obj Y := P.obj X (unop Y), map f := P.map (𝟙 _) f.unop }
+  map g := { app X := P.map g (𝟙 _) }
+
+/-- Construct a natural transformation between profunctors from a `ProfunctorCore.Hom`. -/
+@[simps]
+def ofHom {P Q : ProfunctorCore.{w} C D} (f : P.Hom Q) : ofCore P ⟶ ofCore Q where
+  app X := { app Y := f.app X (unop Y) }
+
+/-- The identity profunctor from `C` to `C`. This is defined as the Yoneda bifunctor. -/
+@[simps! obj_obj obj_map map_app]
+protected def id : Profunctor C C := yoneda
+
+/-- The opposite of a profunctor. -/
+@[simps! obj_obj obj_map map_app]
+def op (P : Profunctor.{w} C D) : Profunctor.{w} Dᵒᵖ Cᵒᵖ :=
+  .ofCore {
+    obj X Y := (P.obj (unop Y)).obj X
+    map f g := (P.map g.unop).app _ ≫ (P.obj _).map f }
+
+/-- Whisker a profunctor from `C` to `D` with functors into `C` and `D`. -/
+@[simps! obj_obj obj_map map_app]
+def whiskerLeft {A B : Type*} [Category* A] [Category* B]
+    (P : Profunctor.{w} C D) (F : A ⥤ C) (G : B ⥤ D) : Profunctor.{w} A B :=
+  (((Functor.whiskeringLeft₂ _).obj F).obj G.op).obj P
+
+/-- Increase the universe level of a profunctor. -/
+@[pp_with_univ, simps! obj_obj obj_map map_app]
+def ulift (P : Profunctor.{w} C D) : Profunctor.{max w' w} C D :=
+  (Functor.postcompose₂.obj uliftFunctor).obj P
+
+/-- Increase the universe level of a profunctor by one. This enables dot notation `P.ulift1`,
+which is not possible with `Profunctor.ulift`. -/
+abbrev ulift1 (P : Profunctor.{w} C D) : Profunctor.{w + 1} C D :=
+  Profunctor.ulift.{w + 1} P
+
+end Profunctor
+
+/-- Given a functor from `C` to `D`, this is the corresponding profunctor from `C` to `D`. -/
+@[simps! obj_obj obj_map map_app]
+def Functor.toProfunctor (F : C ⥤ D) : Profunctor C D :=
+  (Profunctor.id (C := D)).whiskerLeft F (𝟭 _)
+
+/-- Given a functor from `C` to `D`, this is the corresponding profunctor from `D` to `C`. -/
+@[simps! obj_obj obj_map map_app]
+def Functor.toProfunctorFlip (F : C ⥤ D) : Profunctor D C :=
+  (Profunctor.id (C := D)).whiskerLeft (𝟭 _) F
+
+end CategoryTheory

From 0b4e7af2e516c0a54a5beb3289d2ad3b19c7582c Mon Sep 17 00:00:00 2001
From: Adrian Marti <adrianmarti06@gmail.com>
Date: Wed, 15 Apr 2026 11:19:24 -0600
Subject: [PATCH 02/40] add Adrian Marti as coauthor


From e00691acf1e841a73dfe6bf37d0292e4704ffb90 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 11:23:03 -0600
Subject: [PATCH 03/40] profunctor composition

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 137 ++++++++++++++++++++
 1 file changed, 137 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Profunctor/Comp.lean

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
new file mode 100644
index 00000000000000..24ac49a223f1f4
--- /dev/null
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -0,0 +1,137 @@
+module
+
+public import Mathlib.CategoryTheory.Limits.Shapes.End
+public import Mathlib.CategoryTheory.Limits.Types.Colimits
+public import Mathlib.CategoryTheory.Profunctor.Basic
+
+universe w v u
+
+namespace CategoryTheory
+
+namespace Limits
+
+open Opposite
+
+class ChosenCoends.{v',u'} (C : Type*) [Category* C] where
+  cowedge {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : Cowedge F
+  isCoend {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : IsColimit (cowedge F)
+
+variable {C : Type*} [Category* C] [ChosenCoends.{v, u} C]
+
+section
+
+variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ C)
+
+def chosenCoend : C := (ChosenCoends.cowedge F).pt
+
+def chosenCoend.ι (X : J) : (F.obj (op X)).obj X ⟶ chosenCoend F :=
+  (ChosenCoends.cowedge F).π X
+
+lemma chosenCoend.condition {X X' : J} (f : X ⟶ X') :
+    (F.map f.op).app _ ≫ chosenCoend.ι F X = (F.obj _).map f ≫ chosenCoend.ι F X' :=
+  (ChosenCoends.cowedge F).condition f
+
+variable {F}
+
+@[ext]
+lemma chosenCoend.hom_ext {X : C} {f g : chosenCoend F ⟶ X}
+    (h : ∀ j, chosenCoend.ι F j ≫ f = chosenCoend.ι F j ≫ g) : f = g := by
+  apply (ChosenCoends.isCoend F).hom_ext
+  rintro (a | a)
+  · simpa using _ ≫= h _
+  · exact h _
+
+variable {X : C} (f : ∀ j, (F.obj (op j)).obj j ⟶ X)
+  (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j)
+
+def chosenCoend.desc : chosenCoend F ⟶ X :=
+  Cowedge.IsColimit.desc (ChosenCoends.isCoend F) f hf
+
+@[reassoc (attr := simp)]
+lemma chosenCoend.ι_desc (j : J) : chosenCoend.ι F j ≫ chosenCoend.desc f hf = f j := by
+  apply IsColimit.fac
+
+def chosenCoend.map {G : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) : chosenCoend F ⟶ chosenCoend G :=
+  chosenCoend.desc (fun x ↦ (f.app (op x)).app x ≫ chosenCoend.ι _ _) (fun j j' φ ↦ by
+    simp [chosenCoend.condition])
+
+@[reassoc (attr := simp)]
+lemma chosenCoend.ι_map {G : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (j : J) :
+    chosenCoend.ι F j ≫ chosenCoend.map f = (f.app _).app _ ≫ chosenCoend.ι G j := by
+  simp [chosenCoend.map]
+
+@[simp]
+lemma chosenCoend.map_id : chosenCoend.map (𝟙 F) = 𝟙 _ := by cat_disch
+
+@[reassoc (attr := simp)]
+lemma chosenCoend.map_comp {G H : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (g : G ⟶ H) :
+    chosenCoend.map f ≫ chosenCoend.map g = chosenCoend.map (f ≫ g) := by
+  cat_disch
+
+end
+
+end Limits
+
+namespace Profunctor
+
+universe w' v₁ v₂ v₃ u₁ u₂ u₃
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+  {E : Type u₃} [Category.{v₃} E] [Limits.ChosenCoends.{v₂, u₂} (Type (max w w'))]
+
+open Opposite
+
+@[simps! obj_obj obj_map map_app]
+def compDiagram (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y : E) :
+    Dᵒᵖ ⥤ D ⥤ Type max w w' where
+  obj U := {
+    obj V := ((P.obj X).obj U) × ((Q.obj V).obj (Opposite.op Y))
+    map f := TypeCat.ofHom (Prod.map id ((Q.map f).app _)) }
+  map g := { app U := TypeCat.ofHom (Prod.map ((P.obj _).map g) id) }
+
+@[simps]
+def compDiagramMap (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
+    {X X' : C} {Y Y' : E} (f : X ⟶ X') (g : Y ⟶ Y') :
+    compDiagram P Q X Y' ⟶ compDiagram P Q X' Y where
+  app d := { app d' := TypeCat.ofHom (Prod.map ((P.map f).app d) ((Q.obj d').map g.op)) }
+
+open Limits
+
+abbrev compObj (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y : E) : Type max w w' :=
+  chosenCoend <| compDiagram P Q X Y
+
+noncomputable abbrev compMap (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
+    {X X' : C} {Y Y' : E} (f : X ⟶ X') (g : Y ⟶ Y') :
+    compObj P Q X Y' ⟶ compObj P Q X' Y :=
+  chosenCoend.map <| compDiagramMap P Q f g
+
+@[simp]
+lemma compMap_id (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y : E) :
+    P.compMap Q (𝟙 X) (𝟙 Y) = 𝟙 _ := by
+  convert chosenCoend.map_id
+  cat_disch
+
+@[simp]
+lemma compMap_comp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
+    {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : E} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) :
+    P.compMap Q (f ≫ f') (g ≫ g') = P.compMap Q f g' ≫ P.compMap Q f' g := by
+  convert (chosenCoend.map_comp _ _).symm
+  cat_disch
+
+@[simps! obj_obj obj_map map_app]
+noncomputable def comp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) :
+    Profunctor.{max w w'} C E :=
+  .ofCore { obj X Y := compObj P Q X Y, map f g := compMap P Q f g }
+
+end Profunctor
+
+open Limits in
+@[implicit_reducible]
+noncomputable def chosenCoendsType : ChosenCoends.{v, u} (Type max v u w) where
+  cowedge F := Functor.coconeTypesEquiv _ (multispanIndexCoend F).multispan.coconeTypes
+  isCoend F := Types.TypeMax.colimitCoconeIsColimit (multispanIndexCoend F).multispan
+
+noncomputable instance : Limits.ChosenCoends.{v, u} (Type (max v u)) :=
+  chosenCoendsType
+
+end CategoryTheory

From 9065f37058c59ad28c5458b5475bd4fabb2b7c34 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 11:24:44 -0600
Subject: [PATCH 04/40] mk_all

---
 Mathlib.lean                                | 1 +
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 16f59e19c97341..73b992a1a5ce98 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3182,6 +3182,7 @@ public import Mathlib.CategoryTheory.Products.Basic
 public import Mathlib.CategoryTheory.Products.Bifunctor
 public import Mathlib.CategoryTheory.Products.Unitor
 public import Mathlib.CategoryTheory.Profunctor.Basic
+public import Mathlib.CategoryTheory.Profunctor.Comp
 public import Mathlib.CategoryTheory.Quotient
 public import Mathlib.CategoryTheory.Quotient.Linear
 public import Mathlib.CategoryTheory.Quotient.LocallySmall
diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 24ac49a223f1f4..b2dd8713356a72 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -4,6 +4,8 @@ public import Mathlib.CategoryTheory.Limits.Shapes.End
 public import Mathlib.CategoryTheory.Limits.Types.Colimits
 public import Mathlib.CategoryTheory.Profunctor.Basic
 
+@[expose] public section
+
 universe w v u
 
 namespace CategoryTheory

From 8c69b823d1ef5931ae9ecafe1c3fec1b2a0b91fb Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 11:37:06 -0600
Subject: [PATCH 05/40] cleanup

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 30 +++++++++------------
 1 file changed, 12 insertions(+), 18 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index b2dd8713356a72..4c9c1625b13cd7 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -79,7 +79,7 @@ namespace Profunctor
 universe w' v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
-  {E : Type u₃} [Category.{v₃} E] [Limits.ChosenCoends.{v₂, u₂} (Type (max w w'))]
+  {E : Type u₃} [Category.{v₃} E]
 
 open Opposite
 
@@ -97,33 +97,27 @@ def compDiagramMap (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
     compDiagram P Q X Y' ⟶ compDiagram P Q X' Y where
   app d := { app d' := TypeCat.ofHom (Prod.map ((P.map f).app d) ((Q.obj d').map g.op)) }
 
-open Limits
-
-abbrev compObj (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y : E) : Type max w w' :=
-  chosenCoend <| compDiagram P Q X Y
-
-noncomputable abbrev compMap (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
-    {X X' : C} {Y Y' : E} (f : X ⟶ X') (g : Y ⟶ Y') :
-    compObj P Q X Y' ⟶ compObj P Q X' Y :=
-  chosenCoend.map <| compDiagramMap P Q f g
-
 @[simp]
-lemma compMap_id (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y : E) :
-    P.compMap Q (𝟙 X) (𝟙 Y) = 𝟙 _ := by
-  convert chosenCoend.map_id
+lemma compDiagramMap_id (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y : E) :
+    P.compDiagramMap Q (𝟙 X) (𝟙 Y) = 𝟙 _ := by
   cat_disch
 
 @[simp]
-lemma compMap_comp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
+lemma compDiagramMap_comp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
     {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : E} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) :
-    P.compMap Q (f ≫ f') (g ≫ g') = P.compMap Q f g' ≫ P.compMap Q f' g := by
-  convert (chosenCoend.map_comp _ _).symm
+    P.compDiagramMap Q (f ≫ f') (g ≫ g') = P.compDiagramMap Q f g' ≫ P.compDiagramMap Q f' g := by
   cat_disch
 
+open Limits
+
+variable [Limits.ChosenCoends.{v₂, u₂} (Type (max w w'))]
+
 @[simps! obj_obj obj_map map_app]
 noncomputable def comp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) :
     Profunctor.{max w w'} C E :=
-  .ofCore { obj X Y := compObj P Q X Y, map f g := compMap P Q f g }
+  .ofCore {
+    obj X Y := chosenCoend <| compDiagram P Q X Y
+    map f g := chosenCoend.map <| compDiagramMap P Q f g }
 
 end Profunctor
 

From 4994d154dbfd19de09b7bc59e5be71f8eddd6f2b Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 13:47:09 -0600
Subject: [PATCH 06/40] make coends in type computable

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 60 +++++++++++++++------
 1 file changed, 43 insertions(+), 17 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 4c9c1625b13cd7..75bec8e393611c 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -6,18 +6,51 @@ public import Mathlib.CategoryTheory.Profunctor.Basic
 
 @[expose] public section
 
-universe w v u
+universe w w' v u
 
 namespace CategoryTheory
 
+open Opposite
+
 namespace Limits
 
-open Opposite
+namespace Types
+
+variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ Type u)
+
+inductive coendRel : (W : J) × (F.obj (op W)).obj W → (W : J) × (F.obj (op W)).obj W → Prop where
+  | mk {W W' : J} (f : W ⟶ W') (x : (F.obj (op W')).obj W) :
+    coendRel ⟨_, (F.map f.op).app _ x⟩ ⟨_, (F.obj _).map f x⟩
+
+def coend : Type u := Quot (coendRel F)
+
+def coend.ι (j : J) : (F.obj (op j)).obj j ⟶ coend F := TypeCat.ofHom fun x ↦ Quot.mk _ ⟨j, x⟩
+
+def coend.condition {j j' : J} (f : j ⟶ j') :
+    (F.map f.op).app _ ≫ coend.ι F j = (F.obj _).map f ≫ coend.ι F j' := by
+  ext
+  apply Quot.sound
+  apply coendRel.mk
+
+def cowedge : Cowedge F := Cowedge.mk (coend F) (coend.ι F) (by intros; apply coend.condition F)
+
+def cowedgeIsColimit : IsColimit (cowedge F) where
+  desc := fun (s : Cowedge F) ↦ TypeCat.ofHom <| Quot.lift (fun x ↦ s.π x.fst x.snd) <| by
+    intro ⟨ja, ha⟩ ⟨jb, hb⟩ h
+    cases h with | mk f x => exact ConcreteCategory.congr_hom (s.condition f) _
+  fac s := by rintro (_ | _) <;> cat_disch
+  uniq s m h := by ext ⟨j⟩; exact ConcreteCategory.congr_hom (h (.right j.fst)) j.snd
+
+end Types
 
 class ChosenCoends.{v',u'} (C : Type*) [Category* C] where
   cowedge {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : Cowedge F
   isCoend {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : IsColimit (cowedge F)
 
+instance : Limits.ChosenCoends.{v, u} (Type u) where
+  cowedge := Types.cowedge
+  isCoend := Types.cowedgeIsColimit
+
 variable {C : Type*} [Category* C] [ChosenCoends.{v, u} C]
 
 section
@@ -76,10 +109,8 @@ end Limits
 
 namespace Profunctor
 
-universe w' v₁ v₂ v₃ u₁ u₂ u₃
-
-variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
-  {E : Type u₃} [Category.{v₃} E]
+variable {C : Type*} [Category* C] {D : Type u} [Category.{v} D]
+  {E : Type*} [Category* E]
 
 open Opposite
 
@@ -110,24 +141,19 @@ lemma compDiagramMap_comp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
 
 open Limits
 
-variable [Limits.ChosenCoends.{v₂, u₂} (Type (max w w'))]
+variable [Limits.ChosenCoends.{v, u} (Type (max w w'))]
 
 @[simps! obj_obj obj_map map_app]
-noncomputable def comp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) :
+def univComp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) :
     Profunctor.{max w w'} C E :=
   .ofCore {
     obj X Y := chosenCoend <| compDiagram P Q X Y
     map f g := chosenCoend.map <| compDiagramMap P Q f g }
 
-end Profunctor
-
-open Limits in
-@[implicit_reducible]
-noncomputable def chosenCoendsType : ChosenCoends.{v, u} (Type max v u w) where
-  cowedge F := Functor.coconeTypesEquiv _ (multispanIndexCoend F).multispan.coconeTypes
-  isCoend F := Types.TypeMax.colimitCoconeIsColimit (multispanIndexCoend F).multispan
+@[simps! obj_obj obj_map map_app]
+def comp (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) : Profunctor.{u} C E :=
+  Profunctor.univComp.{u, u} P Q
 
-noncomputable instance : Limits.ChosenCoends.{v, u} (Type (max v u)) :=
-  chosenCoendsType
+end Profunctor
 
 end CategoryTheory

From dfc1c795bc6c3b648bc7c015a206941d84c917e3 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 13:50:32 -0600
Subject: [PATCH 07/40] more general universes

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 75bec8e393611c..c75a28b78bd497 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -16,13 +16,13 @@ namespace Limits
 
 namespace Types
 
-variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ Type u)
+variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ Type max w u)
 
 inductive coendRel : (W : J) × (F.obj (op W)).obj W → (W : J) × (F.obj (op W)).obj W → Prop where
   | mk {W W' : J} (f : W ⟶ W') (x : (F.obj (op W')).obj W) :
     coendRel ⟨_, (F.map f.op).app _ x⟩ ⟨_, (F.obj _).map f x⟩
 
-def coend : Type u := Quot (coendRel F)
+def coend : Type max w u := Quot (coendRel F)
 
 def coend.ι (j : J) : (F.obj (op j)).obj j ⟶ coend F := TypeCat.ofHom fun x ↦ Quot.mk _ ⟨j, x⟩
 
@@ -47,7 +47,7 @@ class ChosenCoends.{v',u'} (C : Type*) [Category* C] where
   cowedge {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : Cowedge F
   isCoend {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : IsColimit (cowedge F)
 
-instance : Limits.ChosenCoends.{v, u} (Type u) where
+instance : Limits.ChosenCoends.{v, u} (Type max w u) where
   cowedge := Types.cowedge
   isCoend := Types.cowedgeIsColimit
 

From 2aa981ab22bea2d875c82de13b522132c1c9e892 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 13:57:09 -0600
Subject: [PATCH 08/40] .

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index c75a28b78bd497..f3cd4082408f04 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -35,9 +35,8 @@ def coend.condition {j j' : J} (f : j ⟶ j') :
 def cowedge : Cowedge F := Cowedge.mk (coend F) (coend.ι F) (by intros; apply coend.condition F)
 
 def cowedgeIsColimit : IsColimit (cowedge F) where
-  desc := fun (s : Cowedge F) ↦ TypeCat.ofHom <| Quot.lift (fun x ↦ s.π x.fst x.snd) <| by
-    intro ⟨ja, ha⟩ ⟨jb, hb⟩ h
-    cases h with | mk f x => exact ConcreteCategory.congr_hom (s.condition f) _
+  desc s := TypeCat.ofHom <| Quot.lift (fun x ↦ Multicofork.π s x.fst x.snd) fun _ _ h ↦ by
+    cases h with | mk f x => exact ConcreteCategory.congr_hom (Cowedge.condition s f) _
   fac s := by rintro (_ | _) <;> cat_disch
   uniq s m h := by ext ⟨j⟩; exact ConcreteCategory.congr_hom (h (.right j.fst)) j.snd
 

From 26797dc037ff217a81e458c074fc7375f04aafff Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 15:37:07 -0600
Subject: [PATCH 09/40] left unitor

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 96 ++++++++++++++++++++-
 1 file changed, 92 insertions(+), 4 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index f3cd4082408f04..5f9885c51ee975 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -1,8 +1,16 @@
+/-
+Copyright (c) 2026 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
 module
 
 public import Mathlib.CategoryTheory.Limits.Shapes.End
 public import Mathlib.CategoryTheory.Limits.Types.Colimits
 public import Mathlib.CategoryTheory.Profunctor.Basic
+/-!
+
+-/
 
 @[expose] public section
 
@@ -46,10 +54,6 @@ class ChosenCoends.{v',u'} (C : Type*) [Category* C] where
   cowedge {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : Cowedge F
   isCoend {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : IsColimit (cowedge F)
 
-instance : Limits.ChosenCoends.{v, u} (Type max w u) where
-  cowedge := Types.cowedge
-  isCoend := Types.cowedgeIsColimit
-
 variable {C : Type*} [Category* C] [ChosenCoends.{v, u} C]
 
 section
@@ -104,10 +108,44 @@ lemma chosenCoend.map_comp {G H : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (g : G ⟶
 
 end
 
+section
+
+instance : Limits.ChosenCoends.{v, u} (Type max w u) where
+  cowedge := Types.cowedge
+  isCoend := Types.cowedgeIsColimit
+
+variable {J : Type u} [Category.{v} J] {F : Jᵒᵖ ⥤ J ⥤ Type max w u}
+
+lemma chosenCoend.ι_apply (j : J) (x : (F.obj (op j)).obj j) :
+    chosenCoend.ι F j x = Quot.mk _ ⟨j, x⟩ :=
+  rfl
+
+lemma chosenCoend.desc_apply {X : Type max w u} (f : ∀ j, (F.obj (op j)).obj j ⟶ X)
+    (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j)
+    (x : chosenCoend F) : chosenCoend.desc f hf x =
+      Quot.lift (fun j ↦ f j.fst j.snd) (fun _ _ h ↦ by
+        cases h with | mk f x => exact ConcreteCategory.congr_hom (hf f) _) x :=
+  rfl
+
+lemma chosenCoend.map_apply {G : Jᵒᵖ ⥤ J ⥤ Type max w u} (f : F ⟶ G) (x : chosenCoend F) :
+    chosenCoend.map f x = Quot.map (fun ⟨j, y⟩ ↦ ⟨j, (f.app _).app _ y⟩) (fun _ _ h ↦ by
+      cases h with | mk g x =>
+        dsimp
+        convert Types.coendRel.mk g ((f.app _).app _ x)
+        · simp only [← NatTrans.comp_app_apply, f.naturality]
+        · simp [← (f.app _).naturality_apply, -NatTrans.naturality_apply]) x :=
+  rfl
+
+end
+
 end Limits
 
 namespace Profunctor
 
+section Composition
+
+section Definition
+
 variable {C : Type*} [Category* C] {D : Type u} [Category.{v} D]
   {E : Type*} [Category* E]
 
@@ -153,6 +191,56 @@ def univComp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) :
 def comp (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) : Profunctor.{u} C E :=
   Profunctor.univComp.{u, u} P Q
 
+end Definition
+
+section LeftUnitor
+
+variable {C : Type u} [Category.{u} C] {D : Type u} [Category* D]
+
+set_option backward.isDefEq.respectTransparency false in
+def leftUnitor (P : Profunctor.{u} C D) : (Profunctor.id (C := C)).comp P ≅ P :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ Equiv.toIso {
+    toFun := Quot.lift (fun ⟨d, f, x⟩ ↦ (P.map f).app _ x) fun _ _ h ↦ by
+      simp only [compDiagram_obj_obj, id_obj_obj, op_unop]
+      cases h with
+      | mk f x =>
+        dsimp
+        rw [← comp_apply, ← NatTrans.comp_app, ← Functor.map_comp]
+    invFun x := Quot.mk _ ⟨X, 𝟙 X, x⟩
+    left_inv x := by
+      obtain ⟨⟨_, f, x⟩, rfl⟩ := Quot.mk_surjective x
+      symm
+      apply Quot.sound
+      dsimp
+      convert Limits.Types.coendRel.mk
+        (F := compDiagram (Profunctor.id.{u} (C := C)) P X (unop Y)) f ⟨𝟙 X, x⟩
+      cat_disch
+    right_inv _ := by simp }) (by
+      dsimp
+      intro x y f
+      ext
+      simp only [compDiagram_obj_obj, id_obj_obj, op_unop, Limits.chosenCoend.ι_map_assoc,
+        compDiagramMap_app_app, Functor.map_id, NatTrans.id_app, Quiver.Hom.op_unop,
+        TypeCat.Fun.toFun_apply, comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
+        Equiv.toIso_hom_hom_apply, Equiv.coe_fn_mk]
+      conv =>
+        enter [1, 3]
+        change Limits.Types.coend.ι _ _ _
+      conv =>
+        enter [2, 2, 3]
+        change Limits.Types.coend.ι _ _ _
+      simp [Limits.Types.coend.ι] )) (by
+      dsimp
+      intro x y f
+      ext _ z
+      simp [Limits.chosenCoend.map_apply, Quot.map]
+      obtain ⟨_, rfl⟩ := Quot.mk_surjective z
+      simp)
+
+end LeftUnitor
+
+end Composition
+
 end Profunctor
 
 end CategoryTheory

From b14790f596b9886c61190403bbc103784cce39c7 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 15:39:55 -0600
Subject: [PATCH 10/40] wip

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 5f9885c51ee975..6bf1baa2d79ed0 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -223,13 +223,8 @@ def leftUnitor (P : Profunctor.{u} C D) : (Profunctor.id (C := C)).comp P ≅ P
         compDiagramMap_app_app, Functor.map_id, NatTrans.id_app, Quiver.Hom.op_unop,
         TypeCat.Fun.toFun_apply, comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
         Equiv.toIso_hom_hom_apply, Equiv.coe_fn_mk]
-      conv =>
-        enter [1, 3]
-        change Limits.Types.coend.ι _ _ _
-      conv =>
-        enter [2, 2, 3]
-        change Limits.Types.coend.ι _ _ _
-      simp [Limits.Types.coend.ι] )) (by
+      erw [Limits.chosenCoend.ι_apply, Limits.chosenCoend.ι_apply] -- TODO: fix
+      simp)) (by
       dsimp
       intro x y f
       ext _ z

From ba83fbc732b46ca31dd3264f2729243680e182ff Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 15 Apr 2026 23:19:57 -0600
Subject: [PATCH 11/40] right unitor

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 85 ++++++++++++++-------
 1 file changed, 58 insertions(+), 27 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 6bf1baa2d79ed0..9b34d1a58baf66 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -199,34 +199,21 @@ variable {C : Type u} [Category.{u} C] {D : Type u} [Category* D]
 
 set_option backward.isDefEq.respectTransparency false in
 def leftUnitor (P : Profunctor.{u} C D) : (Profunctor.id (C := C)).comp P ≅ P :=
-  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ Equiv.toIso {
-    toFun := Quot.lift (fun ⟨d, f, x⟩ ↦ (P.map f).app _ x) fun _ _ h ↦ by
-      simp only [compDiagram_obj_obj, id_obj_obj, op_unop]
-      cases h with
-      | mk f x =>
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents
+    (fun Y ↦ Equiv.toIso {
+      toFun := Quot.lift (fun ⟨d, f, x⟩ ↦ (P.map f).app _ x) fun _ _ h ↦ by cases h; simp
+      invFun x := Quot.mk _ ⟨X, 𝟙 X, x⟩
+      left_inv x := by
+        obtain ⟨⟨_, f, x⟩, rfl⟩ := Quot.mk_surjective x
+        symm
+        apply Quot.sound
         dsimp
-        rw [← comp_apply, ← NatTrans.comp_app, ← Functor.map_comp]
-    invFun x := Quot.mk _ ⟨X, 𝟙 X, x⟩
-    left_inv x := by
-      obtain ⟨⟨_, f, x⟩, rfl⟩ := Quot.mk_surjective x
-      symm
-      apply Quot.sound
-      dsimp
-      convert Limits.Types.coendRel.mk
-        (F := compDiagram (Profunctor.id.{u} (C := C)) P X (unop Y)) f ⟨𝟙 X, x⟩
-      cat_disch
-    right_inv _ := by simp }) (by
-      dsimp
-      intro x y f
-      ext
-      simp only [compDiagram_obj_obj, id_obj_obj, op_unop, Limits.chosenCoend.ι_map_assoc,
-        compDiagramMap_app_app, Functor.map_id, NatTrans.id_app, Quiver.Hom.op_unop,
-        TypeCat.Fun.toFun_apply, comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
-        Equiv.toIso_hom_hom_apply, Equiv.coe_fn_mk]
-      erw [Limits.chosenCoend.ι_apply, Limits.chosenCoend.ι_apply] -- TODO: fix
-      simp)) (by
-      dsimp
-      intro x y f
+        convert Limits.Types.coendRel.mk
+          (F := compDiagram (Profunctor.id.{u} (C := C)) P X (unop Y)) f ⟨𝟙 X, x⟩
+        cat_disch
+      right_inv _ := by simp })
+    (fun f ↦ by dsimp; ext; simp [compDiagram, Limits.chosenCoend.ι_apply _]))
+    (fun f ↦ by
       ext _ z
       simp [Limits.chosenCoend.map_apply, Quot.map]
       obtain ⟨_, rfl⟩ := Quot.mk_surjective z
@@ -234,6 +221,50 @@ def leftUnitor (P : Profunctor.{u} C D) : (Profunctor.id (C := C)).comp P ≅ P
 
 end LeftUnitor
 
+section RightUnitor
+
+variable {C : Type u} [Category* C] {D : Type u} [Category.{u} D]
+
+set_option backward.isDefEq.respectTransparency false in
+def rightUnitor (P : Profunctor.{u} C D) : P.comp (.id (C := D)) ≅ P :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents
+    (fun Y ↦ Equiv.toIso {
+      toFun := Quot.lift (fun ⟨d, x, f⟩ ↦ (P.obj X).map f.op x) fun _ _ h ↦ by cases h; simp
+      invFun x := Quot.mk _ ⟨Y.unop, x, 𝟙 Y.unop⟩
+      left_inv x := by
+        obtain ⟨⟨_, x, f⟩, rfl⟩ := Quot.mk_surjective x
+        apply Quot.sound
+        dsimp
+        convert Limits.Types.coendRel.mk
+          (F := compDiagram P (.id (C := D)) X (unop Y)) f ⟨x, 𝟙 _⟩
+        cat_disch
+      right_inv x := by simp })
+    (fun f ↦ by dsimp; ext; simp [compDiagram, Limits.chosenCoend.ι_apply _]))
+    (fun f ↦ by
+      ext _ z
+      simp [Limits.chosenCoend.map_apply, Quot.map]
+      obtain ⟨_, rfl⟩ := Quot.mk_surjective z
+      simp)
+
+end RightUnitor
+
+section Associator
+
+variable {C D E F : Type u} [Category.{u} C] [Category.{u} D] [Category.{u} E] [Category.{u} F]
+variable (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) (R : Profunctor.{u} E F)
+
+set_option backward.isDefEq.respectTransparency false in
+noncomputable def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ Equiv.toIso {
+    toFun := Quot.lift (fun ⟨e, x⟩ ↦ Quot.mk _ ⟨(Quot.out x.1).1, (Quot.out x.1).2.1,
+      Quot.mk _ ⟨e, (Quot.out x.1).2.2, x.snd⟩⟩) sorry
+    invFun := sorry
+    left_inv := sorry
+    right_inv := sorry
+  }) sorry) sorry
+
+end Associator
+
 end Composition
 
 end Profunctor

From 1a7bb2da561910969a53513a3990cea721096211 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Fri, 17 Apr 2026 08:27:08 -0600
Subject: [PATCH 12/40] Update Mathlib/CategoryTheory/Profunctor/Basic.lean

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
---
 Mathlib/CategoryTheory/Profunctor/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Basic.lean b/Mathlib/CategoryTheory/Profunctor/Basic.lean
index 5e6fd55887f63f..806830028c4055 100644
--- a/Mathlib/CategoryTheory/Profunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Basic.lean
@@ -23,7 +23,7 @@ of a profunctor with functors, and the profunctors in both directions correspond
 ## Future work
 
 - Define composition of profunctors.
-- Define the bicategory of categories where the 1-cells are profunctors.
+- Define the bicategory of categories where the 1-morphisms are profunctors.
 -/
 
 @[expose] public section

From b84027d20e912a59071c0a731466ff824ce8bc7c Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Fri, 17 Apr 2026 08:27:21 -0600
Subject: [PATCH 13/40] Update Mathlib/CategoryTheory/Profunctor/Basic.lean

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
---
 Mathlib/CategoryTheory/Profunctor/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Basic.lean b/Mathlib/CategoryTheory/Profunctor/Basic.lean
index 806830028c4055..2bb0e895e2940b 100644
--- a/Mathlib/CategoryTheory/Profunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Basic.lean
@@ -32,9 +32,9 @@ namespace CategoryTheory
 
 open Opposite
 
-universe w' w
+universe w' w v₁ v₂ u₁ u₂
 
-variable (C D : Type*) [Category* C] [Category* D]
+variable (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Category.{v₂} D]
 
 /-- Custom structure to construct profunctors, i.e. bifunctors `C ⥤ Dᵒᵖ ⥤ Type w`. -/
 @[pp_with_univ]

From 202f7b9a5a711e88e604e2c6d95e1299ccdbdf29 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Fri, 17 Apr 2026 08:33:57 -0600
Subject: [PATCH 14/40] clarify docstring, change name

---
 Mathlib/CategoryTheory/Profunctor/Basic.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Basic.lean b/Mathlib/CategoryTheory/Profunctor/Basic.lean
index 2bb0e895e2940b..36a26fd5232d2d 100644
--- a/Mathlib/CategoryTheory/Profunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Basic.lean
@@ -60,7 +60,8 @@ abbrev Functor.profunctor (F : C ⥤ Dᵒᵖ ⥤ Type w) : Profunctor.{w} C D :=
 
 namespace ProfunctorCore
 
-/-- Custom structure to construct natural transformations between profunctors. -/
+/-- Custom structure to construct natural transformations between profunctors, see
+`CategoryTheory.Profunctor.ofHom`. -/
 structure Hom (P Q : ProfunctorCore.{w} C D) where
   /-- The components of the natural transformation -/
   app (X : C) (Y : D) : P.obj X Y ⟶ Q.obj X Y
@@ -144,7 +145,7 @@ def Functor.toProfunctor (F : C ⥤ D) : Profunctor C D :=
 
 /-- Given a functor from `C` to `D`, this is the corresponding profunctor from `D` to `C`. -/
 @[simps! obj_obj obj_map map_app]
-def Functor.toProfunctorFlip (F : C ⥤ D) : Profunctor D C :=
+def Functor.toProfunctorRev (F : C ⥤ D) : Profunctor D C :=
   (Profunctor.id (C := D)).whiskerLeft (𝟭 _) F
 
 end CategoryTheory

From 945d17e85257478338405f7ec43439bf5295cf19 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Fri, 17 Apr 2026 09:00:13 -0600
Subject: [PATCH 15/40] .

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 9b34d1a58baf66..ee335ce74a2af8 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -130,10 +130,9 @@ lemma chosenCoend.desc_apply {X : Type max w u} (f : ∀ j, (F.obj (op j)).obj j
 lemma chosenCoend.map_apply {G : Jᵒᵖ ⥤ J ⥤ Type max w u} (f : F ⟶ G) (x : chosenCoend F) :
     chosenCoend.map f x = Quot.map (fun ⟨j, y⟩ ↦ ⟨j, (f.app _).app _ y⟩) (fun _ _ h ↦ by
       cases h with | mk g x =>
-        dsimp
         convert Types.coendRel.mk g ((f.app _).app _ x)
         · simp only [← NatTrans.comp_app_apply, f.naturality]
-        · simp [← (f.app _).naturality_apply, -NatTrans.naturality_apply]) x :=
+        · simp [← NatTrans.naturality_apply]) x :=
   rfl
 
 end

From 318376962776c937726ee969bada5bfec362c66c Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Mon, 20 Apr 2026 15:52:30 -0600
Subject: [PATCH 16/40] wip

---
 Mathlib/CategoryTheory/Profunctor/Basic.lean |   4 +-
 Mathlib/CategoryTheory/Profunctor/Comp.lean  | 298 ++++++++++++++++---
 2 files changed, 263 insertions(+), 39 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Basic.lean b/Mathlib/CategoryTheory/Profunctor/Basic.lean
index 36a26fd5232d2d..03a3c7b7328346 100644
--- a/Mathlib/CategoryTheory/Profunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Basic.lean
@@ -140,12 +140,12 @@ end Profunctor
 
 /-- Given a functor from `C` to `D`, this is the corresponding profunctor from `C` to `D`. -/
 @[simps! obj_obj obj_map map_app]
-def Functor.toProfunctor (F : C ⥤ D) : Profunctor C D :=
+def Functor.toProfunctor (F : C ⥤ D) : Profunctor.{v₂} C D :=
   (Profunctor.id (C := D)).whiskerLeft F (𝟭 _)
 
 /-- Given a functor from `C` to `D`, this is the corresponding profunctor from `D` to `C`. -/
 @[simps! obj_obj obj_map map_app]
-def Functor.toProfunctorRev (F : C ⥤ D) : Profunctor D C :=
+def Functor.toProfunctorRev (F : C ⥤ D) : Profunctor.{v₂} D C :=
   (Profunctor.id (C := D)).whiskerLeft (𝟭 _) F
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index ee335ce74a2af8..a14ff2453e118d 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -5,8 +5,12 @@ Authors: Dagur Asgeirsson
 -/
 module
 
+public import Mathlib.CategoryTheory.Adjunction.Mates
+public import Mathlib.CategoryTheory.Adjunction.Whiskering
+public import Mathlib.CategoryTheory.Limits.Final
 public import Mathlib.CategoryTheory.Limits.Shapes.End
 public import Mathlib.CategoryTheory.Limits.Types.Colimits
+public import Mathlib.CategoryTheory.Monoidal.Closed.Types
 public import Mathlib.CategoryTheory.Profunctor.Basic
 /-!
 
@@ -18,6 +22,16 @@ universe w w' v u
 
 namespace CategoryTheory
 
+namespace Functor
+
+variable {A B C D E : Type*} [Category* A] [Category* B] [Category* C] [Category* D] [Category* E]
+
+@[simps!]
+def flipping₃₄₁₂ : (A ⥤ B ⥤ C ⥤ D ⥤ E) ≌ (C ⥤ D ⥤ A ⥤ B ⥤ E) :=
+  (flipping.congrRight.trans flipping).trans (flipping.congrRight.trans flipping).congrRight
+
+end Functor
+
 open Opposite
 
 namespace Limits
@@ -28,7 +42,7 @@ variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ Type max w u)
 
 inductive coendRel : (W : J) × (F.obj (op W)).obj W → (W : J) × (F.obj (op W)).obj W → Prop where
   | mk {W W' : J} (f : W ⟶ W') (x : (F.obj (op W')).obj W) :
-    coendRel ⟨_, (F.map f.op).app _ x⟩ ⟨_, (F.obj _).map f x⟩
+    coendRel ⟨W, ConcreteCategory.hom ((F.map f.op).app _) x⟩ ⟨W', ConcreteCategory.hom ((F.obj _).map f) x⟩
 
 def coend : Type max w u := Quot (coendRel F)
 
@@ -54,10 +68,10 @@ class ChosenCoends.{v',u'} (C : Type*) [Category* C] where
   cowedge {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : Cowedge F
   isCoend {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : IsColimit (cowedge F)
 
-variable {C : Type*} [Category* C] [ChosenCoends.{v, u} C]
-
 section
 
+variable {C : Type*} [Category* C] [ChosenCoends.{v, u} C]
+
 variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ C)
 
 def chosenCoend : C := (ChosenCoends.cowedge F).pt
@@ -98,6 +112,9 @@ lemma chosenCoend.ι_map {G : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (j : J) :
     chosenCoend.ι F j ≫ chosenCoend.map f = (f.app _).app _ ≫ chosenCoend.ι G j := by
   simp [chosenCoend.map]
 
+def chosenCoend.uniq (c : Cowedge F) (hc : IsColimit c) : c.pt ≅ chosenCoend F :=
+  hc.coconePointUniqueUpToIso (ChosenCoends.isCoend _)
+
 @[simp]
 lemma chosenCoend.map_id : chosenCoend.map (𝟙 F) = 𝟙 _ := by cat_disch
 
@@ -106,14 +123,22 @@ lemma chosenCoend.map_comp {G H : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (g : G ⟶
     chosenCoend.map f ≫ chosenCoend.map g = chosenCoend.map (f ≫ g) := by
   cat_disch
 
+@[simps]
+def chosenCoendFunctor : (Jᵒᵖ ⥤ J ⥤ C) ⥤ C where
+  obj := chosenCoend
+  map := chosenCoend.map
+
 end
 
 section
 
+@[simps -isSimp]
 instance : Limits.ChosenCoends.{v, u} (Type max w u) where
   cowedge := Types.cowedge
   isCoend := Types.cowedgeIsColimit
 
+section GeneralUniverse
+
 variable {J : Type u} [Category.{v} J] {F : Jᵒᵖ ⥤ J ⥤ Type max w u}
 
 lemma chosenCoend.ι_apply (j : J) (x : (F.obj (op j)).obj j) :
@@ -135,6 +160,74 @@ lemma chosenCoend.map_apply {G : Jᵒᵖ ⥤ J ⥤ Type max w u} (f : F ⟶ G) (
         · simp [← NatTrans.naturality_apply]) x :=
   rfl
 
+end GeneralUniverse
+
+section Small
+
+open scoped TypeCat
+
+variable {J : Type u} [Category.{u} J]
+
+@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
+def adjoint : Type u ⥤ Jᵒᵖ ⥤ J ⥤ Type u where
+  obj X := (Functor.postcompose₂.obj (yoneda.obj X)).obj
+    (yoneda ⋙ (opOpEquivalence (Type u)).congrRight.inverse ⋙
+      (Functor.opUnopEquiv J (Type uᵒᵖ)).inverse).leftOp
+  map f := { app c := { app d := TypeCat.ofHom fun g ↦ g ≫ f } }
+
+set_option backward.isDefEq.respectTransparency false in
+def chosenCoendAdjunction : chosenCoendFunctor (C := Type u) (J := J) ⊣ adjoint (J := J) where
+  unit := {
+    app F := {
+      app j := { app j' := ↾fun f ↦ ↾fun g ↦ Quot.mk _ ⟨j.unop, (F.obj _).map g f⟩ }
+      naturality _ _ f := by
+        ext j x
+        dsimp
+        ext g
+        dsimp
+        apply Quot.sound
+        have := Types.coendRel.mk f.unop ((F.obj _).map g x)
+        simp_all }
+    naturality F G f := by
+      ext j j' x
+      dsimp
+      ext g
+      dsimp [chosenCoend.map_apply, Quot.map]
+      apply Quot.sound
+      simpa using Types.coendRel.mk (𝟙 (unop j)) ((G.obj _).map g ((f.app _).app _ x)) }
+  counit := {
+    app X := ↾Quot.lift (fun ⟨j, (x : (j ⟶ j) ⟶ X)⟩ ↦ x (𝟙 j)) (fun _ _ h ↦ by induction h; simp) }
+  left_triangle_components := by
+    intro F
+    ext x
+    obtain ⟨x, rfl⟩ := Quot.mk_surjective x
+    simp [chosenCoend.map_apply, Quot.map]
+
+variable {I : Type u} [Category.{u} I] -- (F : Iᵒᵖ ⥤ I ⥤ Jᵒᵖ ⥤ J ⥤ Type u)
+
+def iso' : adjoint (J := I) ⋙ Functor.postcompose₂.obj (adjoint (J := J)) ≅
+    (adjoint (J := J) ⋙ Functor.postcompose₂.obj (adjoint (J := I))) ⋙
+      Functor.flipping₃₄₁₂.inverse :=
+  NatIso.ofComponents fun X ↦ NatIso.ofComponents fun i ↦ NatIso.ofComponents fun i' ↦
+    NatIso.ofComponents fun j ↦ NatIso.ofComponents fun j' ↦ {
+      hom := ↾fun x ↦ ↾fun y ↦ ↾fun z ↦ (x.hom z).hom y
+      inv := ↾fun x ↦ ↾fun y ↦ ↾fun z ↦ (x.hom z).hom y }
+
+def fubini :
+    Functor.postcompose₂.obj (chosenCoendFunctor (J := J) (C := Type u)) ⋙
+      chosenCoendFunctor (J := I) ≅
+    Functor.flipping₃₄₁₂.functor ⋙ Functor.postcompose₂.obj (chosenCoendFunctor (J := I)) ⋙
+      chosenCoendFunctor (J := J) :=
+  (conjugateIsoEquiv (Adjunction.comp Functor.flipping₃₄₁₂.toAdjunction
+    (((chosenCoendAdjunction.whiskerRight _ ).whiskerRight _).comp chosenCoendAdjunction))
+    (((chosenCoendAdjunction.whiskerRight _ ).whiskerRight _).comp chosenCoendAdjunction)).symm <|
+      NatIso.ofComponents fun X ↦ NatIso.ofComponents fun i ↦ NatIso.ofComponents fun i' ↦
+        NatIso.ofComponents fun j ↦ NatIso.ofComponents fun j' ↦ {
+          hom := ↾fun x ↦ ↾fun y ↦ ↾fun z ↦ (x.hom z).hom y
+          inv := ↾fun x ↦ ↾fun y ↦ ↾fun z ↦ (x.hom z).hom y }
+
+end Small
+
 end
 
 end Limits
@@ -145,8 +238,7 @@ section Composition
 
 section Definition
 
-variable {C : Type*} [Category* C] {D : Type u} [Category.{v} D]
-  {E : Type*} [Category* E]
+variable {C : Type*} [Category* C] {D : Type u} [Category.{v} D] {E : Type*} [Category* E]
 
 open Opposite
 
@@ -196,25 +288,25 @@ section LeftUnitor
 
 variable {C : Type u} [Category.{u} C] {D : Type u} [Category* D]
 
+open Limits TypeCat
+
 set_option backward.isDefEq.respectTransparency false in
-def leftUnitor (P : Profunctor.{u} C D) : (Profunctor.id (C := C)).comp P ≅ P :=
-  NatIso.ofComponents (fun X ↦ NatIso.ofComponents
-    (fun Y ↦ Equiv.toIso {
-      toFun := Quot.lift (fun ⟨d, f, x⟩ ↦ (P.map f).app _ x) fun _ _ h ↦ by cases h; simp
-      invFun x := Quot.mk _ ⟨X, 𝟙 X, x⟩
-      left_inv x := by
+def leftUnitor (P : Profunctor.{u} C D) : Profunctor.id.comp P ≅ P :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ {
+      hom := ↾Quot.lift (fun ⟨d, f, x⟩ ↦ (P.map f).app _ x) fun _ _ h ↦ by cases h; simp
+      inv := ↾fun x ↦ Quot.mk _ ⟨X, 𝟙 X, x⟩
+      hom_inv_id := by
+        ext x
         obtain ⟨⟨_, f, x⟩, rfl⟩ := Quot.mk_surjective x
         symm
         apply Quot.sound
         dsimp
-        convert Limits.Types.coendRel.mk
-          (F := compDiagram (Profunctor.id.{u} (C := C)) P X (unop Y)) f ⟨𝟙 X, x⟩
-        cat_disch
-      right_inv _ := by simp })
-    (fun f ↦ by dsimp; ext; simp [compDiagram, Limits.chosenCoend.ι_apply _]))
+        have := Types.coendRel.mk (F := compDiagram Profunctor.id.{u} P X (unop Y)) f ⟨𝟙 X, x⟩
+        cat_disch })
+    (fun f ↦ by dsimp; ext; simp [compDiagram, chosenCoend.ι_apply _]))
     (fun f ↦ by
       ext _ z
-      simp [Limits.chosenCoend.map_apply, Quot.map]
+      simp [chosenCoend.map_apply, Quot.map]
       obtain ⟨_, rfl⟩ := Quot.mk_surjective z
       simp)
 
@@ -222,26 +314,26 @@ end LeftUnitor
 
 section RightUnitor
 
+open Limits TypeCat
+
 variable {C : Type u} [Category* C] {D : Type u} [Category.{u} D]
 
 set_option backward.isDefEq.respectTransparency false in
-def rightUnitor (P : Profunctor.{u} C D) : P.comp (.id (C := D)) ≅ P :=
-  NatIso.ofComponents (fun X ↦ NatIso.ofComponents
-    (fun Y ↦ Equiv.toIso {
-      toFun := Quot.lift (fun ⟨d, x, f⟩ ↦ (P.obj X).map f.op x) fun _ _ h ↦ by cases h; simp
-      invFun x := Quot.mk _ ⟨Y.unop, x, 𝟙 Y.unop⟩
-      left_inv x := by
+def rightUnitor (P : Profunctor.{u} C D) : P.comp .id ≅ P :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ {
+      hom := ↾Quot.lift (fun ⟨d, x, f⟩ ↦ (P.obj X).map f.op x) fun _ _ h ↦ by cases h; simp
+      inv := ↾fun x ↦ Quot.mk _ ⟨Y.unop, x, 𝟙 Y.unop⟩
+      hom_inv_id := by
+        ext x
         obtain ⟨⟨_, x, f⟩, rfl⟩ := Quot.mk_surjective x
         apply Quot.sound
         dsimp
-        convert Limits.Types.coendRel.mk
-          (F := compDiagram P (.id (C := D)) X (unop Y)) f ⟨x, 𝟙 _⟩
-        cat_disch
-      right_inv x := by simp })
-    (fun f ↦ by dsimp; ext; simp [compDiagram, Limits.chosenCoend.ι_apply _]))
+        have := Types.coendRel.mk (F := compDiagram P (.id (C := D)) X (unop Y)) f ⟨x, 𝟙 _⟩
+        cat_disch })
+    (fun f ↦ by dsimp; ext; simp [compDiagram, chosenCoend.ι_apply _]))
     (fun f ↦ by
       ext _ z
-      simp [Limits.chosenCoend.map_apply, Quot.map]
+      simp [chosenCoend.map_apply, Quot.map]
       obtain ⟨_, rfl⟩ := Quot.mk_surjective z
       simp)
 
@@ -252,15 +344,147 @@ section Associator
 variable {C D E F : Type u} [Category.{u} C] [Category.{u} D] [Category.{u} E] [Category.{u} F]
 variable (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) (R : Profunctor.{u} E F)
 
+open TypeCat Limits Types Functor MonoidalCategory
+
+variable (X : C) (Y : F)
+
+@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
+def compDiagram₃ : Dᵒᵖ ⥤ D ⥤ Eᵒᵖ ⥤ E ⥤ Type u where
+  obj U := {
+    obj V := (postcompose₂.obj (tensorLeft ((P.obj X).obj U))).obj <| Q.compDiagram R V Y
+    map f := (postcompose₂.obj (tensorLeft ((P.obj X).obj U))).map (Q.compDiagramMap R f (𝟙 _))
+  }
+  map g := { app U := (postcompose₂.map { app V := (P.obj _).map g ▷ _ }).app _ }
+
+@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
+def compDiagram₃' : Eᵒᵖ ⥤ E ⥤ Dᵒᵖ ⥤ D ⥤ Type u where
+  obj U := {
+    obj V := (postcompose₂.obj (tensorRight ((R.obj V).obj (Opposite.op Y)))).obj <|
+      P.compDiagram Q X (unop U)
+    map f := (postcompose₂.map { app V := _ ◁ (R.map f).app _ }).app _
+  }
+  map g := { app _ := (postcompose₂.obj _).map <| P.compDiagramMap _ (𝟙 _) g.unop }
+
+def compDiagram₃Iso : (compDiagram₃ P Q R X Y) ≅
+    flipping₃₄₁₂.functor.obj (compDiagram₃' P Q R X Y) :=
+  NatIso.ofComponents fun d ↦ NatIso.ofComponents fun d' ↦ NatIso.ofComponents fun e ↦
+    NatIso.ofComponents fun e' ↦ (Equiv.prodAssoc _ _ _).symm.toIso
+
+instance (X : Type u) : IsLeftAdjoint (tensorRight X) :=
+  Functor.isLeftAdjoint_of_iso (BraidedCategory.tensorLeftIsoTensorRight X)
+
+-- attribute [elementwise] Multicofork.condition
+-- attribute [simp] Multicofork.condition_apply
+
+noncomputable def compIso₃ (X : C) (Y : Fᵒᵖ) :
+    (postcompose₂.obj chosenCoendFunctor ⋙ chosenCoendFunctor).obj (compDiagram₃' P Q R X Y.unop) ≅
+      (((P.comp Q).comp R).obj X).obj Y := by
+  refine chosenCoendFunctor.mapIso (NatIso.ofComponents
+      (fun e ↦ NatIso.ofComponents (fun e' ↦ ?_) ?_) ?_)
+  · refine ((ChosenCoends.isCoend
+      (((P.compDiagram₃' Q R X (unop Y)).obj e).obj e'))).coconePointsIsoOfEquivalence
+        (isColimitOfPreserves (tensorRight ((R.obj e').obj Y))
+          (ChosenCoends.isCoend (P.compDiagram Q X (unop e))))
+        Equivalence.refl (NatIso.ofComponents ?_ ?_)
+    · rintro (_ | _)
+      exacts [Iso.refl _, Iso.refl _]
+    · rintro (_ | _) (_ | _) (_ | _ | _)
+      all_goals cat_disch
+  · cat_disch
+  · intro X Y f
+    ext : 2
+    apply chosenCoend.hom_ext
+    intro j
+    dsimp
+    ext x
+    · apply Quot.sound
+      convert coendRel.mk (𝟙 j) _
+      rotate_right
+      · exact (x.1.1, (Q.obj j).map f x.1.2)
+      · apply Prod.ext
+        · simp; rfl
+        · rfl
+      · apply Prod.ext
+        · simp; rfl
+        · simp; rfl
+    · rfl
+
+noncomputable def compIso₃' (X : C) (Y : Fᵒᵖ) :
+    (postcompose₂.obj chosenCoendFunctor ⋙ chosenCoendFunctor).obj (compDiagram₃ P Q R X Y.unop) ≅
+      ((P.comp (Q.comp R)).obj X).obj Y := by
+  refine chosenCoendFunctor.mapIso (NatIso.ofComponents
+      (fun d ↦ NatIso.ofComponents (fun d' ↦ ?_) ?_) ?_)
+  · refine ((ChosenCoends.isCoend
+      (((P.compDiagram₃ Q R X (unop Y)).obj d).obj d'))).coconePointsIsoOfEquivalence
+        (isColimitOfPreserves (tensorLeft ((P.obj X).obj d))
+          (ChosenCoends.isCoend (Q.compDiagram R d' (unop Y))))
+        Equivalence.refl (NatIso.ofComponents ?_ ?_)
+    · rintro (_ | _)
+      exacts [Iso.refl _, Iso.refl _]
+    · rintro (_ | _) (_ | _) (_ | _ | _)
+      all_goals cat_disch
+  · cat_disch
+  · intro X Y f
+    ext : 2
+    apply chosenCoend.hom_ext
+    intro j
+    dsimp
+    ext x
+    · rfl
+    · apply Quot.sound
+      convert coendRel.mk (𝟙 j) _
+      rotate_right
+      · exact (x.2.1, x.2.2)
+      · apply Prod.ext
+        · simp; rfl
+        · rfl
+      · apply Prod.ext
+        · rfl
+        · simp; rfl
+
+noncomputable def associatorComponents (X : C) (Y : Fᵒᵖ) :
+    (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y :=
+  (compIso₃ P Q R X Y).symm ≪≫ fubini.app (P.compDiagram₃' Q R X (unop Y)) ≪≫
+    (_ ⋙ chosenCoendFunctor).mapIso (compDiagram₃Iso P Q R X (unop Y)).symm ≪≫ compIso₃' P Q R X Y
+
+
+noncomputable def associatorComponents' (X : C) (Y : Fᵒᵖ) :
+    (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y where
+  hom := ↾fun x ↦ Quot.mk _ ⟨x.out.2.1.out.1, x.out.2.1.out.2.1,
+      Quot.mk _ ⟨x.out.1, x.out.2.1.out.2.2, x.out.2.2⟩⟩
+  inv := ↾fun x ↦ Quot.mk _ ⟨x.out.2.2.out.1,
+    Quot.mk _ ⟨x.out.1, x.out.2.1, x.out.2.2.out.2.1⟩, x.out.2.2.out.2.2⟩
+  hom_inv_id :=
+    sorry
+  inv_hom_id :=
+    sorry
+
+lemma associatorComponents_apply (X : C) (Y : Fᵒᵖ) (d : D) (e : E)
+    (r : (R.obj e).obj Y) (p : (P.obj X).obj (Opposite.op d)) (q : (Q.obj d).obj (Opposite.op e)) :
+    (associatorComponents P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩) =
+      Quot.mk _ ⟨d, (p, Quot.mk _ ⟨e, (q, r)⟩)⟩ := by
+  sorry
+  -- obtain ⟨⟨d', x⟩, h⟩ := Quot.mk_surjective ((associatorComponents P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩))
+  -- rw [← h]
+  -- apply Quot.sound
+  -- have := coendRel.mk (𝟙 d') x
+
+
+
 set_option backward.isDefEq.respectTransparency false in
-noncomputable def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) :=
-  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ Equiv.toIso {
-    toFun := Quot.lift (fun ⟨e, x⟩ ↦ Quot.mk _ ⟨(Quot.out x.1).1, (Quot.out x.1).2.1,
-      Quot.mk _ ⟨e, (Quot.out x.1).2.2, x.snd⟩⟩) sorry
-    invFun := sorry
-    left_inv := sorry
-    right_inv := sorry
-  }) sorry) sorry
+noncomputable def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) := by
+  refine NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦
+    associatorComponents P Q R X Y) ?_) ?_
+  · intro f f' g
+    ext ⟨e, ⟨d, p, x⟩, r⟩
+    dsimp
+    erw [associatorComponents_apply, associatorComponents_apply]
+    simp [chosenCoend.map_apply, Quot.map]
+  · intro f f' g
+    ext _ ⟨e, ⟨d, p, x⟩, r⟩
+    dsimp
+    erw [associatorComponents_apply, associatorComponents_apply]
+    simp [chosenCoend.map_apply, Quot.map]
 
 end Associator
 

From 873ef4039ca3c80908b3fe173efbfe2e7be275c8 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Mon, 20 Apr 2026 15:53:28 -0600
Subject: [PATCH 17/40] wip

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index a14ff2453e118d..3f55190acde277 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -464,12 +464,6 @@ lemma associatorComponents_apply (X : C) (Y : Fᵒᵖ) (d : D) (e : E)
     (associatorComponents P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩) =
       Quot.mk _ ⟨d, (p, Quot.mk _ ⟨e, (q, r)⟩)⟩ := by
   sorry
-  -- obtain ⟨⟨d', x⟩, h⟩ := Quot.mk_surjective ((associatorComponents P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩))
-  -- rw [← h]
-  -- apply Quot.sound
-  -- have := coendRel.mk (𝟙 d') x
-
-
 
 set_option backward.isDefEq.respectTransparency false in
 noncomputable def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) := by

From 4217f6a1faccae71d5ae280384dffbb21311a366 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Mon, 20 Apr 2026 15:55:15 -0600
Subject: [PATCH 18/40] wip

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 3f55190acde277..e902e4a7f240fe 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -470,12 +470,12 @@ noncomputable def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) := by
   refine NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦
     associatorComponents P Q R X Y) ?_) ?_
   · intro f f' g
-    ext ⟨e, ⟨d, p, x⟩, r⟩
+    ext ⟨e, ⟨d, p, q⟩, r⟩
     dsimp
     erw [associatorComponents_apply, associatorComponents_apply]
     simp [chosenCoend.map_apply, Quot.map]
   · intro f f' g
-    ext _ ⟨e, ⟨d, p, x⟩, r⟩
+    ext _ ⟨e, ⟨d, p, q⟩, r⟩
     dsimp
     erw [associatorComponents_apply, associatorComponents_apply]
     simp [chosenCoend.map_apply, Quot.map]

From 8939f1e060522bdae8a6fdfe480c86b07e54a948 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Mon, 20 Apr 2026 15:56:23 -0600
Subject: [PATCH 19/40] wip

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index e902e4a7f240fe..77d3c5a75b7632 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -451,7 +451,7 @@ noncomputable def associatorComponents (X : C) (Y : Fᵒᵖ) :
 noncomputable def associatorComponents' (X : C) (Y : Fᵒᵖ) :
     (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y where
   hom := ↾fun x ↦ Quot.mk _ ⟨x.out.2.1.out.1, x.out.2.1.out.2.1,
-      Quot.mk _ ⟨x.out.1, x.out.2.1.out.2.2, x.out.2.2⟩⟩
+    Quot.mk _ ⟨x.out.1, x.out.2.1.out.2.2, x.out.2.2⟩⟩
   inv := ↾fun x ↦ Quot.mk _ ⟨x.out.2.2.out.1,
     Quot.mk _ ⟨x.out.1, x.out.2.1, x.out.2.2.out.2.1⟩, x.out.2.2.out.2.2⟩
   hom_inv_id :=

From d2c3bcaecb6189c08c2dd2d56cdfd891badea6b7 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Tue, 21 Apr 2026 12:33:20 -0600
Subject: [PATCH 20/40] sorry free associator

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 176 ++++++++++++++++++--
 1 file changed, 161 insertions(+), 15 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 77d3c5a75b7632..4ae6eb556bc1c5 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -42,7 +42,27 @@ variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ Type max w u)
 
 inductive coendRel : (W : J) × (F.obj (op W)).obj W → (W : J) × (F.obj (op W)).obj W → Prop where
   | mk {W W' : J} (f : W ⟶ W') (x : (F.obj (op W')).obj W) :
-    coendRel ⟨W, ConcreteCategory.hom ((F.map f.op).app _) x⟩ ⟨W', ConcreteCategory.hom ((F.obj _).map f) x⟩
+    coendRel ⟨W, ConcreteCategory.hom ((F.map f.op).app _) x⟩
+      ⟨W', ConcreteCategory.hom ((F.obj _).map f) x⟩
+
+lemma coendRel_iff (W W' : J) (x : (F.obj (op W)).obj W) (y : (F.obj (op W')).obj W') :
+    coendRel F ⟨W, x⟩ ⟨W', y⟩ ↔
+      ∃ (f : W ⟶ W') (z : (F.obj (op W')).obj W),
+        (F.map f.op).app _ z = x ∧ (F.obj _).map f z = y := by
+  constructor
+  · intro h
+    cases h with
+    | mk f x =>
+      use f
+      use x
+  · intro h
+    obtain ⟨f, z, h1, h2⟩ := h
+    rw [← h1, ← h2]
+    exact coendRel.mk f z
+
+lemma eqvGen_coendRel_iff (x y : (W : J) × (F.obj (op W)).obj W) :
+    Relation.EqvGen (coendRel F) x y ↔ coendRel F x y ∨ coendRel F y x :=
+  sorry
 
 def coend : Type max w u := Quot (coendRel F)
 
@@ -442,43 +462,169 @@ noncomputable def compIso₃' (X : C) (Y : Fᵒᵖ) :
         · rfl
         · simp; rfl
 
-noncomputable def associatorComponents (X : C) (Y : Fᵒᵖ) :
+noncomputable def associatorComponents' (X : C) (Y : Fᵒᵖ) :
     (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y :=
   (compIso₃ P Q R X Y).symm ≪≫ fubini.app (P.compDiagram₃' Q R X (unop Y)) ≪≫
     (_ ⋙ chosenCoendFunctor).mapIso (compDiagram₃Iso P Q R X (unop Y)).symm ≪≫ compIso₃' P Q R X Y
 
+lemma associatorComponents'_apply (X : C) (Y : Fᵒᵖ) (d : D) (e : E)
+    (r : (R.obj e).obj Y) (p : (P.obj X).obj (Opposite.op d)) (q : (Q.obj d).obj (Opposite.op e)) :
+    (associatorComponents' P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩) =
+      Quot.mk _ ⟨d, (p, Quot.mk _ ⟨e, (q, r)⟩)⟩ := by
+  sorry
 
-noncomputable def associatorComponents' (X : C) (Y : Fᵒᵖ) :
+lemma relation_map {α β : Type*} (f : α → β) (r : β → β → Prop) (x y : α)
+    (h : Relation.EqvGen (fun x y ↦ r (f x) (f y)) x y) :
+    Relation.EqvGen r (f x) (f y) := by
+  induction h with
+  | rel => exact Relation.EqvGen.rel _ _ (by assumption)
+  | refl => exact Relation.EqvGen.refl _
+  | symm => exact Relation.EqvGen.symm _ _ (by assumption)
+  | trans => exact Relation.EqvGen.trans _ _ _ (by assumption) (by assumption)
+
+@[simp]
+lemma Relation.eqvGen_eqvGen {α : Type*} (r : α → α → Prop) :
+    Relation.EqvGen (Relation.EqvGen r) = Relation.EqvGen r := by
+  ext x y
+  refine ⟨fun h ↦ ?_, fun h ↦ Relation.EqvGen.rel _ _ h⟩
+  induction h with
+  | rel => assumption
+  | refl => exact Relation.EqvGen.refl _
+  | symm => exact Relation.EqvGen.symm _ _ (by assumption)
+  | trans => exact Relation.EqvGen.trans _ _ _ (by assumption) (by assumption)
+
+set_option backward.isDefEq.respectTransparency false in
+def associatorComponents (X : C) (Y : Fᵒᵖ) :
     (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y where
-  hom := ↾fun x ↦ Quot.mk _ ⟨x.out.2.1.out.1, x.out.2.1.out.2.1,
-    Quot.mk _ ⟨x.out.1, x.out.2.1.out.2.2, x.out.2.2⟩⟩
-  inv := ↾fun x ↦ Quot.mk _ ⟨x.out.2.2.out.1,
-    Quot.mk _ ⟨x.out.1, x.out.2.1, x.out.2.2.out.2.1⟩, x.out.2.2.out.2.2⟩
-  hom_inv_id :=
-    sorry
-  inv_hom_id :=
-    sorry
+  hom := by
+    refine ↾Quot.lift (fun ⟨e, x, r⟩ ↦ Quot.map (fun ⟨d, p, q⟩ ↦ ⟨d, p, Quot.mk _ ⟨e, q, r⟩⟩) ?_ x) ?_
+    · intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
+      cases h with
+      | mk f x =>
+        convert coendRel.mk (F := (P.compDiagram (Q.comp R) X (unop Y)))
+          f ⟨x.1, Quot.mk _ ⟨e, x.2, r⟩⟩
+        dsimp
+        ext
+        · rfl
+        · apply Quot.sound
+          convert coendRel.mk (F := Q.compDiagram R d' (unop Y)) (𝟙 e) ⟨(Q.map f).app _ x.2, r⟩
+          · simp
+          · apply Prod.ext
+            · rfl
+            · simp; rfl
+    · rintro ⟨e, ⟨d, p, q⟩, r⟩ ⟨e', ⟨d', p', q'⟩, r'⟩ h
+      dsimp
+      rw [coendRel_iff] at h
+      obtain ⟨f, ⟨x, r''⟩, h₁, h₂⟩ := h
+      simp only [compDiagram_obj_obj, comp_obj_obj, op_unop, compDiagram_map_app, comp_obj_map,
+        Quiver.Hom.unop_op, hom_ofHom, Fun.coe_mk, Prod.map_apply, id_eq, Prod.mk.injEq,
+        compDiagram_obj_map] at h₁ h₂
+      obtain ⟨rfl, rfl⟩ := h₂
+      obtain ⟨h₁, rfl⟩ := h₁
+      simp only [chosenCoend.map_apply, Quot.map, compDiagram_obj_obj, compDiagramMap_app_app,
+        map_id, NatTrans.id_app, ofHom_apply, Prod.map_apply, id_apply] at h₁
+      symm
+      simp only [Quot.map]
+      rw [Quot.eq] at h₁ ⊢
+      have h₁' := relation_map (fun ⟨d, p, q⟩ ↦ ⟨d, (p, Quot.mk _ ⟨e, q, r''⟩)⟩)
+          (Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))) _ _ (h₁.mono <| by
+        intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
+        apply Relation.EqvGen.rel
+        simp only [compDiagram_obj_obj, op_unop, comp_obj_obj, coendRel_iff, compDiagram_map_app,
+          hom_ofHom, Fun.coe_mk, compDiagram_obj_map, comp_map_app, Prod.exists, Prod.map_apply,
+          id_eq, Prod.mk.injEq, ↓existsAndEq, and_true, true_and]
+        rw [coendRel_iff] at h
+        obtain ⟨f, x, h₁, h₂⟩ := h
+        use f
+        simp_all [Prod.ext_iff, chosenCoend.map_apply, Quot.map])
+      simp only [compDiagram_obj_obj, op_unop, comp_obj_obj, Relation.eqvGen_eqvGen] at h₁'
+      refine (Relation.EqvGen.trans _ _ _ ?_ h₁')
+      apply Relation.EqvGen.rel
+      rw [coendRel_iff]
+      use 𝟙 _
+      simp only [compDiagram_obj_obj, op_unop, comp_obj_obj, op_id, map_id, NatTrans.id_app,
+        id_apply, compDiagram_obj_map, ofHom_apply, exists_eq_left, Prod.map_apply, id_eq,
+        Prod.mk.injEq, true_and]
+      symm
+      apply Quot.sound
+      exact coendRel.mk (F := Q.compDiagram R _ _) f (_, _)
+  inv := by
+    refine ↾Quot.lift (fun ⟨d, p, x⟩ ↦ Quot.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d, p, q⟩, r⟩) ?_ x) ?_
+    · intro ⟨e, q, r⟩ ⟨e', q', r'⟩ h
+      cases h with
+      | mk f x =>
+        convert coendRel.mk (F := (P.comp Q).compDiagram R X (unop Y))
+          f ⟨_, _⟩
+        dsimp
+        ext
+        · apply Quot.sound
+          convert coendRel.mk (F := P.compDiagram Q X e) (𝟙 d) ⟨p, (Q.obj _).map f.op x.1⟩
+          · apply Prod.ext
+            · simp
+            · rfl
+          · simp; rfl
+        · rfl
+    · rintro ⟨d, p, e, q, r⟩ ⟨d', p', e', q', r'⟩ h-- ⟨e', ⟨d', p', q'⟩, r'⟩ h
+      dsimp
+      rw [coendRel_iff] at h
+      obtain ⟨f, ⟨p, x⟩, h₁, h₂⟩ := h
+      simp only [compDiagram_obj_obj, op_unop, comp_obj_obj, compDiagram_map_app, hom_ofHom,
+        Fun.coe_mk, Prod.map_apply, id_eq, Prod.mk.injEq, compDiagram_obj_map,
+        comp_map_app] at h₁ h₂
+      obtain ⟨rfl, rfl⟩ := h₁
+      obtain ⟨rfl, h₂⟩ := h₂
+      simp only [chosenCoend.map_apply, Quot.map, compDiagram_obj_obj, op_unop,
+        compDiagramMap_app_app, op_id, map_id, ofHom_apply, Prod.map_apply, id_apply] at h₂
+      dsimp [Quot.map]
+      rw [Quot.eq] at h₂ ⊢
+      have h₂' := relation_map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d', p, q⟩, r⟩)
+          (Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))) _ _ (h₂.mono <| by
+        intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
+        apply Relation.EqvGen.rel
+        simp only [compDiagram_obj_obj, comp_obj_obj, op_unop, coendRel_iff, compDiagram_map_app,
+          comp_obj_map, Quiver.Hom.unop_op, hom_ofHom, Fun.coe_mk, compDiagram_obj_map, Prod.exists,
+          Prod.map_apply, id_eq, Prod.mk.injEq, ↓existsAndEq, and_true, true_and]
+        rw [coendRel_iff] at h
+        obtain ⟨f, x, h₁, h₂⟩ := h
+        use f
+        simp_all [Prod.ext_iff, chosenCoend.map_apply, Quot.map])
+      simp only [compDiagram_obj_obj, comp_obj_obj, op_unop, Relation.eqvGen_eqvGen] at h₂'
+      refine (Relation.EqvGen.trans _ _ _ ?_ h₂')
+      apply Relation.EqvGen.rel
+      rw [coendRel_iff]
+      use 𝟙 _
+      simp only [compDiagram_obj_obj, comp_obj_obj, op_unop, op_id, map_id, NatTrans.id_app,
+        id_apply, compDiagram_obj_map, ofHom_apply, exists_eq_left, Prod.map_apply, id_eq,
+        Prod.mk.injEq, and_true]
+      apply Quot.sound
+      exact coendRel.mk (F := P.compDiagram Q _ _) f (_, _)
+  hom_inv_id := by
+    ext ⟨e, ⟨d, p, q⟩, r⟩
+    simp [Quot.map]
+  inv_hom_id := by
+    ext ⟨d, p, ⟨e, q, r⟩⟩
+    simp [Quot.map]
 
 lemma associatorComponents_apply (X : C) (Y : Fᵒᵖ) (d : D) (e : E)
     (r : (R.obj e).obj Y) (p : (P.obj X).obj (Opposite.op d)) (q : (Q.obj d).obj (Opposite.op e)) :
     (associatorComponents P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩) =
       Quot.mk _ ⟨d, (p, Quot.mk _ ⟨e, (q, r)⟩)⟩ := by
-  sorry
+  rfl
 
 set_option backward.isDefEq.respectTransparency false in
-noncomputable def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) := by
+def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) := by
   refine NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦
     associatorComponents P Q R X Y) ?_) ?_
   · intro f f' g
     ext ⟨e, ⟨d, p, q⟩, r⟩
     dsimp
     erw [associatorComponents_apply, associatorComponents_apply]
-    simp [chosenCoend.map_apply, Quot.map]
+    simp
   · intro f f' g
     ext _ ⟨e, ⟨d, p, q⟩, r⟩
     dsimp
     erw [associatorComponents_apply, associatorComponents_apply]
-    simp [chosenCoend.map_apply, Quot.map]
+    simp
 
 end Associator
 

From f6f5d183560bf5d842725488841aee37e155a3c4 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Tue, 21 Apr 2026 12:58:33 -0600
Subject: [PATCH 21/40] remove wrong lemma

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 4ae6eb556bc1c5..5dd9e9d447bb39 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -60,10 +60,6 @@ lemma coendRel_iff (W W' : J) (x : (F.obj (op W)).obj W) (y : (F.obj (op W')).ob
     rw [← h1, ← h2]
     exact coendRel.mk f z
 
-lemma eqvGen_coendRel_iff (x y : (W : J) × (F.obj (op W)).obj W) :
-    Relation.EqvGen (coendRel F) x y ↔ coendRel F x y ∨ coendRel F y x :=
-  sorry
-
 def coend : Type max w u := Quot (coendRel F)
 
 def coend.ι (j : J) : (F.obj (op j)).obj j ⟶ coend F := TypeCat.ofHom fun x ↦ Quot.mk _ ⟨j, x⟩
@@ -497,7 +493,8 @@ set_option backward.isDefEq.respectTransparency false in
 def associatorComponents (X : C) (Y : Fᵒᵖ) :
     (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y where
   hom := by
-    refine ↾Quot.lift (fun ⟨e, x, r⟩ ↦ Quot.map (fun ⟨d, p, q⟩ ↦ ⟨d, p, Quot.mk _ ⟨e, q, r⟩⟩) ?_ x) ?_
+    refine ↾Quot.lift (fun ⟨e, x, r⟩ ↦
+        Quot.map (fun ⟨d, p, q⟩ ↦ ⟨d, p, Quot.mk _ ⟨e, q, r⟩⟩) ?_ x) ?_
     · intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
       cases h with
       | mk f x =>
@@ -549,7 +546,8 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
       apply Quot.sound
       exact coendRel.mk (F := Q.compDiagram R _ _) f (_, _)
   inv := by
-    refine ↾Quot.lift (fun ⟨d, p, x⟩ ↦ Quot.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d, p, q⟩, r⟩) ?_ x) ?_
+    refine ↾Quot.lift (fun ⟨d, p, x⟩ ↦
+        Quot.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d, p, q⟩, r⟩) ?_ x) ?_
     · intro ⟨e, q, r⟩ ⟨e', q', r'⟩ h
       cases h with
       | mk f x =>

From cecf662a3ee98b1f955f77e3087dc494e19ddfec Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Tue, 21 Apr 2026 13:51:08 -0600
Subject: [PATCH 22/40] bicategory structure

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 143 +++++++++++++++++++-
 1 file changed, 140 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 5dd9e9d447bb39..c2a017cb0b9d04 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -64,7 +64,7 @@ def coend : Type max w u := Quot (coendRel F)
 
 def coend.ι (j : J) : (F.obj (op j)).obj j ⟶ coend F := TypeCat.ofHom fun x ↦ Quot.mk _ ⟨j, x⟩
 
-def coend.condition {j j' : J} (f : j ⟶ j') :
+lemma coend.condition {j j' : J} (f : j ⟶ j') :
     (F.map f.op).app _ ≫ coend.ι F j = (F.obj _).map f ≫ coend.ι F j' := by
   ext
   apply Quot.sound
@@ -307,6 +307,7 @@ variable {C : Type u} [Category.{u} C] {D : Type u} [Category* D]
 open Limits TypeCat
 
 set_option backward.isDefEq.respectTransparency false in
+@[simps! hom_app_app inv_app_app]
 def leftUnitor (P : Profunctor.{u} C D) : Profunctor.id.comp P ≅ P :=
   NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ {
       hom := ↾Quot.lift (fun ⟨d, f, x⟩ ↦ (P.map f).app _ x) fun _ _ h ↦ by cases h; simp
@@ -335,6 +336,7 @@ open Limits TypeCat
 variable {C : Type u} [Category* C] {D : Type u} [Category.{u} D]
 
 set_option backward.isDefEq.respectTransparency false in
+@[simps! hom_app_app inv_app_app]
 def rightUnitor (P : Profunctor.{u} C D) : P.comp .id ≅ P :=
   NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ {
       hom := ↾Quot.lift (fun ⟨d, x, f⟩ ↦ (P.obj X).map f.op x) fun _ _ h ↦ by cases h; simp
@@ -490,6 +492,7 @@ lemma Relation.eqvGen_eqvGen {α : Type*} (r : α → α → Prop) :
   | trans => exact Relation.EqvGen.trans _ _ _ (by assumption) (by assumption)
 
 set_option backward.isDefEq.respectTransparency false in
+@[simps hom inv]
 def associatorComponents (X : C) (Y : Fᵒᵖ) :
     (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y where
   hom := by
@@ -603,6 +606,7 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
     ext ⟨d, p, ⟨e, q, r⟩⟩
     simp [Quot.map]
 
+@[simp]
 lemma associatorComponents_apply (X : C) (Y : Fᵒᵖ) (d : D) (e : E)
     (r : (R.obj e).obj Y) (p : (P.obj X).obj (Opposite.op d)) (q : (Q.obj d).obj (Opposite.op e)) :
     (associatorComponents P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩) =
@@ -610,24 +614,157 @@ lemma associatorComponents_apply (X : C) (Y : Fᵒᵖ) (d : D) (e : E)
   rfl
 
 set_option backward.isDefEq.respectTransparency false in
+@[simps! hom_app_app inv_app_app]
 def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) := by
   refine NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦
     associatorComponents P Q R X Y) ?_) ?_
   · intro f f' g
     ext ⟨e, ⟨d, p, q⟩, r⟩
-    dsimp
+    dsimp [-associatorComponents_hom]
     erw [associatorComponents_apply, associatorComponents_apply]
     simp
   · intro f f' g
     ext _ ⟨e, ⟨d, p, q⟩, r⟩
-    dsimp
+    dsimp [-associatorComponents_hom]
     erw [associatorComponents_apply, associatorComponents_apply]
     simp
 
 end Associator
 
+section WhiskerLeft
+
+open TypeCat Limits Types Functor MonoidalCategory
+
+variable {C D E : Type u} [Category.{u} C] [Category.{u} D] [Category.{u} E]
+variable (P : Profunctor.{u} C D) {Q R : Profunctor.{u} D E} (f : Q ⟶ R)
+
+set_option backward.isDefEq.respectTransparency false in
+@[simps app_app]
+def whiskerLeft' : P.comp Q ⟶ P.comp R where
+  app X := {
+    app Y := chosenCoend.map {
+      app d := {
+        app d' := ↾Prod.map id ((f.app _).app _)
+        naturality := by
+          intro d₁ d₂ g
+          ext
+          dsimp
+          apply Prod.ext
+          · simp
+          · simp [← comp_apply, -types_comp_apply] } }
+    naturality := by
+      intros
+      ext ⟨_, _, _⟩
+      simp [chosenCoend.map_apply, Quot.map] }
+  naturality := by
+    intros
+    ext _ ⟨_, _, _⟩
+    simp [chosenCoend.map_apply, Quot.map]
+
+end WhiskerLeft
+
+section WhiskerRight
+
+open TypeCat Limits Types Functor MonoidalCategory
+
+variable {C D E : Type u} [Category.{u} C] [Category.{u} D] [Category.{u} E]
+variable {P Q : Profunctor.{u} C D} (R : Profunctor.{u} D E) (f : P ⟶ Q)
+
+set_option backward.isDefEq.respectTransparency false in
+@[simps app_app]
+def whiskerRight : P.comp R ⟶ Q.comp R where
+  app X := { app Y := chosenCoend.map { app d := { app d' := ↾Prod.map ((f.app _).app _) id } } }
+  naturality := by
+    intros
+    ext _ ⟨_, _, _⟩
+    dsimp [chosenCoend.map_apply, Quot.map]
+    apply Quot.sound
+    rw [coendRel_iff]
+    use 𝟙 _
+    simp [← comp_apply, -types_comp_apply]
+
+end WhiskerRight
+
 end Composition
 
+section Bicategory
+
+@[nolint checkUnivs]
+structure ProfCat where
+  of ::
+  obj : Type u
+  [str : Category.{v} obj]
+
+instance : CoeSort ProfCat (Type u) :=
+  ⟨ProfCat.obj⟩
+
+attribute [instance] ProfCat.str
+
+open Limits Types
+
+set_option backward.isDefEq.respectTransparency false in
+instance : Bicategory ProfCat.{u, u} where
+  Hom X Y := Profunctor.{u} X Y
+  id X := .id
+  comp P Q := P.comp Q
+  whiskerLeft P _ _ f := P.whiskerLeft' f
+  whiskerRight f R := whiskerRight R f
+  associator P Q R := P.associator Q R
+  leftUnitor P := P.leftUnitor
+  rightUnitor P := P.rightUnitor
+  whiskerLeft_id _ _ := by
+    ext _ _ ⟨_, _, _⟩
+    rfl
+  whiskerLeft_comp _ _ _ _ _ _ := by
+    ext _ _ ⟨_, _, _⟩
+    rfl
+  id_whiskerLeft _ := by
+    ext _ _ ⟨_, f, _⟩
+    dsimp [chosenCoend.map_apply, Quot.map]
+    apply Quot.sound
+    rw [coendRel_iff]
+    use f
+    simp [← comp_apply, -types_comp_apply]
+  comp_whiskerLeft _ _ _ _ _ := by
+    ext _ _ ⟨_, ⟨_, _, _⟩, _⟩
+    rfl
+  id_whiskerRight _ _ := by
+    ext _ _ ⟨_, _, _⟩
+    rfl
+  comp_whiskerRight _ _ _ := by
+    ext _ _ ⟨_, _, _⟩
+    rfl
+  whiskerRight_id _ := by
+    ext _ _ ⟨_, _, f⟩
+    dsimp [chosenCoend.map_apply, Quot.map]
+    symm
+    apply Quot.sound
+    rw [coendRel_iff]
+    use f
+    simp [← comp_apply, -types_comp_apply]
+  whiskerRight_comp _ _ _ := by
+    ext _ _ ⟨_, _, _, _, _⟩
+    rfl
+  whisker_assoc _ _ _ _ _ := by
+    ext _ _ ⟨_, ⟨_, _, _⟩, _⟩
+    rfl
+  whisker_exchange _ _ := by
+    ext _ _ ⟨_, _, _⟩
+    rfl
+  pentagon _ _ _ _ := by
+    ext _ _ ⟨_, ⟨_, ⟨_, _, _⟩, _⟩, _⟩
+    rfl
+  triangle _ _ := by
+    ext _ _ ⟨_, ⟨_, _, f⟩, _⟩
+    dsimp [chosenCoend.map_apply, Quot.map]
+    symm
+    apply Quot.sound
+    rw [coendRel_iff]
+    use f
+    simp
+
+end Bicategory
+
 end Profunctor
 
 end CategoryTheory

From e9506111fcba6b0434fd3afcf1f65d89ac313c02 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Tue, 21 Apr 2026 15:46:00 -0600
Subject: [PATCH 23/40] .

---
 Mathlib/CategoryTheory/Profunctor/Basic.lean | 6 +++---
 Mathlib/CategoryTheory/Profunctor/Comp.lean  | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Basic.lean b/Mathlib/CategoryTheory/Profunctor/Basic.lean
index 03a3c7b7328346..03205cdb133f90 100644
--- a/Mathlib/CategoryTheory/Profunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Basic.lean
@@ -122,7 +122,7 @@ def op (P : Profunctor.{w} C D) : Profunctor.{w} Dᵒᵖ Cᵒᵖ :=
 
 /-- Whisker a profunctor from `C` to `D` with functors into `C` and `D`. -/
 @[simps! obj_obj obj_map map_app]
-def whiskerLeft {A B : Type*} [Category* A] [Category* B]
+def whiskerLeft₂ {A B : Type*} [Category* A] [Category* B]
     (P : Profunctor.{w} C D) (F : A ⥤ C) (G : B ⥤ D) : Profunctor.{w} A B :=
   (((Functor.whiskeringLeft₂ _).obj F).obj G.op).obj P
 
@@ -141,11 +141,11 @@ end Profunctor
 /-- Given a functor from `C` to `D`, this is the corresponding profunctor from `C` to `D`. -/
 @[simps! obj_obj obj_map map_app]
 def Functor.toProfunctor (F : C ⥤ D) : Profunctor.{v₂} C D :=
-  (Profunctor.id (C := D)).whiskerLeft F (𝟭 _)
+  (Profunctor.id (C := D)).whiskerLeft₂ F (𝟭 _)
 
 /-- Given a functor from `C` to `D`, this is the corresponding profunctor from `D` to `C`. -/
 @[simps! obj_obj obj_map map_app]
 def Functor.toProfunctorRev (F : C ⥤ D) : Profunctor.{v₂} D C :=
-  (Profunctor.id (C := D)).whiskerLeft (𝟭 _) F
+  (Profunctor.id (C := D)).whiskerLeft₂ (𝟭 _) F
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index c2a017cb0b9d04..6eaa301b2e4ab6 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -640,7 +640,7 @@ variable (P : Profunctor.{u} C D) {Q R : Profunctor.{u} D E} (f : Q ⟶ R)
 
 set_option backward.isDefEq.respectTransparency false in
 @[simps app_app]
-def whiskerLeft' : P.comp Q ⟶ P.comp R where
+def whiskerLeft : P.comp Q ⟶ P.comp R where
   app X := {
     app Y := chosenCoend.map {
       app d := {
@@ -707,7 +707,7 @@ instance : Bicategory ProfCat.{u, u} where
   Hom X Y := Profunctor.{u} X Y
   id X := .id
   comp P Q := P.comp Q
-  whiskerLeft P _ _ f := P.whiskerLeft' f
+  whiskerLeft P _ _ f := P.whiskerLeft f
   whiskerRight f R := whiskerRight R f
   associator P Q R := P.associator Q R
   leftUnitor P := P.leftUnitor

From 3111103c5cbf62bc4ce97f2ca9d9264820429328 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 22 Apr 2026 08:59:48 -0600
Subject: [PATCH 24/40] .

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 6eaa301b2e4ab6..0b9f5b6d7e822e 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -391,9 +391,6 @@ def compDiagram₃Iso : (compDiagram₃ P Q R X Y) ≅
 instance (X : Type u) : IsLeftAdjoint (tensorRight X) :=
   Functor.isLeftAdjoint_of_iso (BraidedCategory.tensorLeftIsoTensorRight X)
 
--- attribute [elementwise] Multicofork.condition
--- attribute [simp] Multicofork.condition_apply
-
 noncomputable def compIso₃ (X : C) (Y : Fᵒᵖ) :
     (postcompose₂.obj chosenCoendFunctor ⋙ chosenCoendFunctor).obj (compDiagram₃' P Q R X Y.unop) ≅
       (((P.comp Q).comp R).obj X).obj Y := by

From 714b4696393a93cdd6f66acf9fcbe1f10eda9881 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 22 Apr 2026 15:21:20 -0600
Subject: [PATCH 25/40] cleanup

---
 Mathlib/CategoryTheory/Limits/Chosen/End.lean |  95 ++
 Mathlib/CategoryTheory/Limits/Types/End.lean  | 105 +++
 Mathlib/CategoryTheory/Profunctor/Basic.lean  |   2 +-
 .../CategoryTheory/Profunctor/Bicategory.lean |  82 ++
 Mathlib/CategoryTheory/Profunctor/Comp.lean   | 882 +++++-------------
 Mathlib/Logic/Relation.lean                   |  18 +
 6 files changed, 555 insertions(+), 629 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/Limits/Chosen/End.lean
 create mode 100644 Mathlib/CategoryTheory/Limits/Types/End.lean
 create mode 100644 Mathlib/CategoryTheory/Profunctor/Bicategory.lean

diff --git a/Mathlib/CategoryTheory/Limits/Chosen/End.lean b/Mathlib/CategoryTheory/Limits/Chosen/End.lean
new file mode 100644
index 00000000000000..5c04ce12c4033b
--- /dev/null
+++ b/Mathlib/CategoryTheory/Limits/Chosen/End.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+module
+
+public import Mathlib.CategoryTheory.Limits.Shapes.End
+
+/-!
+# Chosen Coends
+
+This file defines a typeclass `ChosenCoends` which contains the data of a chosen coend in `C` for
+each functor `Jᵒᵖ ⥤ J ⥤ C`.
+-/
+
+@[expose] public section
+
+universe v u
+
+open Opposite
+
+namespace CategoryTheory.Limits
+
+/-- The data of chosen coends in `C`. -/
+@[nolint checkUnivs, univ_out_params, pp_with_univ]
+class ChosenCoends (C : Type*) [Category* C] where
+  /-- The chosen cowedge for each functor `Jᵒᵖ ⥤ J ⥤ C`. -/
+  cowedge {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ C) : Cowedge F
+  /-- The chosen cowedge is colimiting. -/
+  isCoend {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ C) : IsColimit (cowedge F)
+
+variable {C : Type*} [Category* C] [ChosenCoends.{v, u} C]
+
+variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ C)
+
+/-- The chosen coend of a functor `Jᵒᵖ ⥤ J ⥤ C`. -/
+def chosenCoend : C := (ChosenCoends.cowedge F).pt
+
+/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the inclusion `(F.obj (op j)).obj j ⟶ chosenCoend F`
+for any `j : J`. -/
+def chosenCoend.ι (j : J) : (F.obj (op j)).obj j ⟶ chosenCoend F :=
+  (ChosenCoends.cowedge F).π j
+
+lemma chosenCoend.condition {i j : J} (f : i ⟶ j) :
+    (F.map f.op).app _ ≫ chosenCoend.ι F i = (F.obj _).map f ≫ chosenCoend.ι F j :=
+  (ChosenCoends.cowedge F).condition f
+
+variable {F}
+
+/-- Morphisms out of the chosen coend are determined by their composites with `chosenCoend.ι`. -/
+@[ext]
+lemma chosenCoend.hom_ext {X : C} {f g : chosenCoend F ⟶ X}
+    (h : ∀ j, chosenCoend.ι F j ≫ f = chosenCoend.ι F j ≫ g) : f = g := by
+  apply (ChosenCoends.isCoend F).hom_ext
+  rintro (a | a)
+  · simpa using _ ≫= h _
+  · exact h _
+
+variable {X : C} (f : ∀ j, (F.obj (op j)).obj j ⟶ X)
+  (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j)
+
+/-- Constructor for morphisms out of the chosen coend of a functor. -/
+def chosenCoend.desc : chosenCoend F ⟶ X :=
+  Cowedge.IsColimit.desc (ChosenCoends.isCoend F) f hf
+
+@[reassoc (attr := simp)]
+lemma chosenCoend.ι_desc (j : J) : chosenCoend.ι F j ≫ chosenCoend.desc f hf = f j := by
+  apply IsColimit.fac
+
+/-- A natural transformation of bifunctors induces a map on chosen coends. -/
+def chosenCoend.map {G : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) : chosenCoend F ⟶ chosenCoend G :=
+  chosenCoend.desc (fun x ↦ (f.app (op x)).app x ≫ chosenCoend.ι _ _) (fun j j' φ ↦ by
+    simp [chosenCoend.condition])
+
+@[reassoc (attr := simp)]
+lemma chosenCoend.ι_map {G : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (j : J) :
+    chosenCoend.ι F j ≫ chosenCoend.map f = (f.app _).app _ ≫ chosenCoend.ι G j := by
+  simp [chosenCoend.map]
+
+@[simp]
+lemma chosenCoend.map_id : chosenCoend.map (𝟙 F) = 𝟙 _ := by cat_disch
+
+@[reassoc (attr := simp)]
+lemma chosenCoend.map_comp {G H : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (g : G ⟶ H) :
+    chosenCoend.map f ≫ chosenCoend.map g = chosenCoend.map (f ≫ g) := by
+  cat_disch
+
+/-- The chosen coend construction as a functor out of the bifunctor category. -/
+@[simps]
+def chosenCoendFunctor : (Jᵒᵖ ⥤ J ⥤ C) ⥤ C where
+  obj := chosenCoend
+  map := chosenCoend.map
+
+end CategoryTheory.Limits
diff --git a/Mathlib/CategoryTheory/Limits/Types/End.lean b/Mathlib/CategoryTheory/Limits/Types/End.lean
new file mode 100644
index 00000000000000..2abeb8b305f512
--- /dev/null
+++ b/Mathlib/CategoryTheory/Limits/Types/End.lean
@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2026 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+module
+
+public import Mathlib.CategoryTheory.Limits.Chosen.End
+
+/-!
+# Coends in Types
+
+This file constructs explicit coends in `Type` as quotients and provides a
+`ChosenCoends` instance using this construction.
+-/
+
+@[expose] public section
+
+universe w v u
+
+namespace CategoryTheory
+
+open Opposite TypeCat ConcreteCategory
+
+namespace Limits.Types
+
+variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ Type max w u)
+
+/-- The relation on the sigma type `(W : J) × (F.obj (op W)).obj W` used to construct explicit
+coends in `Type`. Two terms `⟨j, x⟩` and `⟨j', x'⟩` are related if and only if there is a
+morphism `f : j ⟶ j'` in `J` and an element `y : (F.obj (op j')).obj j` such that
+`(F.map f.op).app j y = x` and `(F.obj _).map f y = x'`, see `coendRel_iff` below. -/
+inductive coendRel : (j : J) × (F.obj (op j)).obj j → (j : J) × (F.obj (op j)).obj j → Prop where
+  | mk {j j' : J} (f : j ⟶ j') (x : (F.obj (op j')).obj j) :
+    coendRel ⟨j, TypeCat.Hom.hom ((F.map f.op).app _) x⟩
+      ⟨j', TypeCat.Hom.hom ((F.obj _).map f) x⟩
+
+lemma coendRel_iff (j j' : J) (x : (F.obj (op j)).obj j) (x' : (F.obj (op j')).obj j') :
+    coendRel F ⟨j, x⟩ ⟨j', x'⟩ ↔
+      ∃ (f : j ⟶ j') (y : (F.obj (op j')).obj j),
+        (F.map f.op).app _ y = x ∧ (F.obj _).map f y = x' := by
+  constructor
+  · rintro ⟨f, x⟩
+    exact ⟨f, x, by simp⟩
+  · rintro ⟨f, y, rfl, rfl⟩
+    exact coendRel.mk f y
+
+/-- The coend of a bifunctor valued in `Type`, defined as a quotient. -/
+abbrev coend : Type max w u := Quot (coendRel F)
+
+/-- Given `F : Jᵒᵖ ⥤ J ⥤ Type*`, this is the inclusion `(F.obj (op j)).obj j ⟶ coend F`
+for any `j : J`, which sends `x` to `Quot.mk _ ⟨j, x⟩` -/
+def coend.ι (j : J) : (F.obj (op j)).obj j ⟶ coend F := ↾fun x ↦ Quot.mk _ ⟨j, x⟩
+
+variable {F}
+
+lemma coend.condition {j j' : J} (f : j ⟶ j') :
+    (F.map f.op).app _ ≫ coend.ι F j = (F.obj _).map f ≫ coend.ι F j' := by
+  ext
+  apply Quot.sound
+  apply coendRel.mk
+
+variable (F)
+
+/-- The cowedge corresponding to the explicit coend in `Type` -/
+def cowedge : Cowedge F := Cowedge.mk (coend F) (coend.ι F) (by intros; apply coend.condition)
+
+/-- The cowedge corresponding to the explicit coend in `Type` is colimiting. -/
+def cowedgeIsColimit : IsColimit (cowedge F) where
+  desc s := TypeCat.ofHom <| Quot.lift (fun x ↦ Multicofork.π s x.fst x.snd) fun _ _ h ↦ by
+    cases h with | mk f x => exact ConcreteCategory.congr_hom (Cowedge.condition s f) _
+  fac s := by rintro (_ | _) <;> cat_disch
+  uniq s m h := by ext ⟨j⟩; exact ConcreteCategory.congr_hom (h (.right j.fst)) j.snd
+
+end Types
+
+/-- A `ChosenCoends` instance on `Type` given by the explicit quotient construction above. -/
+instance : ChosenCoends.{v, u} (Type max w u) where
+  cowedge := Types.cowedge
+  isCoend := Types.cowedgeIsColimit
+
+variable {J : Type u} [Category.{v} J] {F : Jᵒᵖ ⥤ J ⥤ Type max w u}
+
+lemma chosenCoend.ι_apply (j : J) (x : (F.obj (op j)).obj j) :
+    chosenCoend.ι F j x = Quot.mk _ ⟨j, x⟩ :=
+  rfl
+
+lemma chosenCoend.desc_apply {X : Type max w u} (f : ∀ j, (F.obj (op j)).obj j ⟶ X)
+    (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j)
+    (x : chosenCoend F) : chosenCoend.desc f hf x =
+      Quot.lift (fun j ↦ f j.fst j.snd) (fun _ _ h ↦ by
+        cases h with | mk f x => exact ConcreteCategory.congr_hom (hf f) _) x :=
+  rfl
+
+lemma chosenCoend.map_apply {G : Jᵒᵖ ⥤ J ⥤ Type max w u} (f : F ⟶ G) (x : chosenCoend F) :
+    chosenCoend.map f x = Quot.lift (fun ⟨j, y⟩ ↦ Quot.mk _ ⟨j, (f.app _).app _ y⟩) (fun _ _ ↦ by
+      rintro ⟨g, y⟩
+      apply Quot.sound
+      rw [Types.coendRel_iff]
+      refine ⟨g, (f.app _).app _ y, ?_, ?_⟩
+      · simp only [← NatTrans.comp_app_apply, f.naturality]
+      · simp [← NatTrans.naturality_apply]) x :=
+  rfl
+
+end CategoryTheory.Limits
diff --git a/Mathlib/CategoryTheory/Profunctor/Basic.lean b/Mathlib/CategoryTheory/Profunctor/Basic.lean
index 03205cdb133f90..7d9bafc146029c 100644
--- a/Mathlib/CategoryTheory/Profunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Basic.lean
@@ -111,7 +111,7 @@ def ofHom {P Q : ProfunctorCore.{w} C D} (f : P.Hom Q) : ofCore P ⟶ ofCore Q w
 
 /-- The identity profunctor from `C` to `C`. This is defined as the Yoneda bifunctor. -/
 @[simps! obj_obj obj_map map_app]
-protected def id : Profunctor C C := yoneda
+protected abbrev id : Profunctor C C := yoneda
 
 /-- The opposite of a profunctor. -/
 @[simps! obj_obj obj_map map_app]
diff --git a/Mathlib/CategoryTheory/Profunctor/Bicategory.lean b/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
new file mode 100644
index 00000000000000..9fe0b105bc1ef0
--- /dev/null
+++ b/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2026 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+module
+
+public import Mathlib.CategoryTheory.Profunctor.Comp
+
+/-!
+
+# The Profunctor Bicategory
+
+This file defines the bicategory `ProfCat` whose objects are categories and whose 1-morphisms are
+profunctors.
+-/
+
+@[expose] public section
+
+universe w v u
+
+namespace CategoryTheory
+
+/-- The bicategory of categories where the 1-morphisms are profunctors. -/
+@[nolint checkUnivs]
+structure ProfCat where
+  of ::
+  /-- The objects of the bicategory are types... -/
+  obj : Type u
+  /-- ... bundled with a category instance. -/
+  [str : Category.{v} obj]
+
+instance : CoeSort ProfCat (Type u) :=
+  ⟨ProfCat.obj⟩
+
+attribute [instance] ProfCat.str
+
+open Limits Types Profunctor
+
+namespace Profunctor
+
+section
+
+@[reassoc (attr := simp)]
+lemma pentagon {C D E F G : Type u} [Category* C] [Category* D] [Category* E]
+  [Category* F] [Category* G] (P : Profunctor.{max u w} C D) (Q : Profunctor.{max u w} D E)
+    (R : Profunctor.{max u w} E F) (S : Profunctor.{max u w} F G) :
+    whiskerRight S (P.associator Q R).hom ≫
+        (P.associator (Q.comp R) S).hom ≫ P.whiskerLeft (Q.associator R S).hom =
+      ((P.comp Q).associator R S).hom ≫ (P.associator Q (R.comp S)).hom := by
+  ext _ _ ⟨_, ⟨_, ⟨_, _, _⟩, _⟩, _⟩
+  rfl
+
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc (attr := simp)]
+lemma triangle {C D E : Type u} [Category* C] [Category.{u} D] [Category* E]
+    (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) :
+    (P.associator (Profunctor.id (C := D)) Q).hom ≫ P.whiskerLeft (Q.leftUnitor.hom) =
+      whiskerRight Q (P.rightUnitor.hom) := by
+  ext _ _ ⟨_, ⟨_, _, g⟩, _⟩
+  dsimp [chosenCoend.map_apply, Quot.map]
+  symm
+  apply Quot.sound
+  rw [coendRel_iff]
+  exact ⟨g, by simp⟩
+
+end
+
+end Profunctor
+
+set_option backward.isDefEq.respectTransparency false in
+instance : Bicategory ProfCat.{u, u} where
+  Hom X Y := Profunctor.{u} X Y
+  id X := .id
+  comp P Q := P.comp Q
+  whiskerLeft P _ _ f := P.whiskerLeft f
+  whiskerRight f R := whiskerRight R f
+  associator P Q R := P.associator Q R
+  leftUnitor P := P.leftUnitor
+  rightUnitor P := P.rightUnitor
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 0b9f5b6d7e822e..26c83683ddb8c1 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -5,248 +5,39 @@ Authors: Dagur Asgeirsson
 -/
 module
 
-public import Mathlib.CategoryTheory.Adjunction.Mates
-public import Mathlib.CategoryTheory.Adjunction.Whiskering
-public import Mathlib.CategoryTheory.Limits.Final
-public import Mathlib.CategoryTheory.Limits.Shapes.End
-public import Mathlib.CategoryTheory.Limits.Types.Colimits
-public import Mathlib.CategoryTheory.Monoidal.Closed.Types
+public import Mathlib.CategoryTheory.Limits.Types.End
 public import Mathlib.CategoryTheory.Profunctor.Basic
+
 /-!
 
--/
+# Composition of Profunctors
 
-@[expose] public section
+This file defines composition of profunctors. Given profunctors `P : C ⥤ Dᵒᵖ ⥤ Type` and
+`Q : D ⥤ Eᵒᵖ ⥤ Type`, the composite `P.comp Q` is the profunctor `C ⥤ Eᵒᵖ ⥤ Type` given on objects
+`X : C` and `Y : E` by the coend `∫ d, P X d × Q d Y`, where `d` ranges over objects of `D`.
 
-universe w w' v u
+## Main Definitions
 
-namespace CategoryTheory
+(All in the namespace `CategoryTheory.Profunctor`)
 
-namespace Functor
+* `comp` : Composition of profunctors.
+* `whiskerLeft` : Left whiskering of a natural transformation of profunctors.
+* `whiskerRight` : Right whiskering of a natural transformation of profunctors.
+* `leftUnitor` : The left unitor isomorphism `Profunctor.id.comp P ≅ P`.
+* `rightUnitor` : The right unitor isomorphism `P.comp Profunctor.id ≅ P`.
+* `associator` : The associator isomorphism `(P.comp Q).comp R ≅ P.comp (Q.comp R)`.
 
-variable {A B C D E : Type*} [Category* A] [Category* B] [Category* C] [Category* D] [Category* E]
+These satisfy the coherence laws for a bicategory, see the file
+`CategoryTheory.Profunctor.Bicategory`.
+-/
 
-@[simps!]
-def flipping₃₄₁₂ : (A ⥤ B ⥤ C ⥤ D ⥤ E) ≌ (C ⥤ D ⥤ A ⥤ B ⥤ E) :=
-  (flipping.congrRight.trans flipping).trans (flipping.congrRight.trans flipping).congrRight
+@[expose] public section
 
-end Functor
+universe w w' v u
 
 open Opposite
 
-namespace Limits
-
-namespace Types
-
-variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ Type max w u)
-
-inductive coendRel : (W : J) × (F.obj (op W)).obj W → (W : J) × (F.obj (op W)).obj W → Prop where
-  | mk {W W' : J} (f : W ⟶ W') (x : (F.obj (op W')).obj W) :
-    coendRel ⟨W, ConcreteCategory.hom ((F.map f.op).app _) x⟩
-      ⟨W', ConcreteCategory.hom ((F.obj _).map f) x⟩
-
-lemma coendRel_iff (W W' : J) (x : (F.obj (op W)).obj W) (y : (F.obj (op W')).obj W') :
-    coendRel F ⟨W, x⟩ ⟨W', y⟩ ↔
-      ∃ (f : W ⟶ W') (z : (F.obj (op W')).obj W),
-        (F.map f.op).app _ z = x ∧ (F.obj _).map f z = y := by
-  constructor
-  · intro h
-    cases h with
-    | mk f x =>
-      use f
-      use x
-  · intro h
-    obtain ⟨f, z, h1, h2⟩ := h
-    rw [← h1, ← h2]
-    exact coendRel.mk f z
-
-def coend : Type max w u := Quot (coendRel F)
-
-def coend.ι (j : J) : (F.obj (op j)).obj j ⟶ coend F := TypeCat.ofHom fun x ↦ Quot.mk _ ⟨j, x⟩
-
-lemma coend.condition {j j' : J} (f : j ⟶ j') :
-    (F.map f.op).app _ ≫ coend.ι F j = (F.obj _).map f ≫ coend.ι F j' := by
-  ext
-  apply Quot.sound
-  apply coendRel.mk
-
-def cowedge : Cowedge F := Cowedge.mk (coend F) (coend.ι F) (by intros; apply coend.condition F)
-
-def cowedgeIsColimit : IsColimit (cowedge F) where
-  desc s := TypeCat.ofHom <| Quot.lift (fun x ↦ Multicofork.π s x.fst x.snd) fun _ _ h ↦ by
-    cases h with | mk f x => exact ConcreteCategory.congr_hom (Cowedge.condition s f) _
-  fac s := by rintro (_ | _) <;> cat_disch
-  uniq s m h := by ext ⟨j⟩; exact ConcreteCategory.congr_hom (h (.right j.fst)) j.snd
-
-end Types
-
-class ChosenCoends.{v',u'} (C : Type*) [Category* C] where
-  cowedge {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : Cowedge F
-  isCoend {J : Type u'} [Category.{v'} J] (F : Jᵒᵖ ⥤ J ⥤ C) : IsColimit (cowedge F)
-
-section
-
-variable {C : Type*} [Category* C] [ChosenCoends.{v, u} C]
-
-variable {J : Type u} [Category.{v} J] (F : Jᵒᵖ ⥤ J ⥤ C)
-
-def chosenCoend : C := (ChosenCoends.cowedge F).pt
-
-def chosenCoend.ι (X : J) : (F.obj (op X)).obj X ⟶ chosenCoend F :=
-  (ChosenCoends.cowedge F).π X
-
-lemma chosenCoend.condition {X X' : J} (f : X ⟶ X') :
-    (F.map f.op).app _ ≫ chosenCoend.ι F X = (F.obj _).map f ≫ chosenCoend.ι F X' :=
-  (ChosenCoends.cowedge F).condition f
-
-variable {F}
-
-@[ext]
-lemma chosenCoend.hom_ext {X : C} {f g : chosenCoend F ⟶ X}
-    (h : ∀ j, chosenCoend.ι F j ≫ f = chosenCoend.ι F j ≫ g) : f = g := by
-  apply (ChosenCoends.isCoend F).hom_ext
-  rintro (a | a)
-  · simpa using _ ≫= h _
-  · exact h _
-
-variable {X : C} (f : ∀ j, (F.obj (op j)).obj j ⟶ X)
-  (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j)
-
-def chosenCoend.desc : chosenCoend F ⟶ X :=
-  Cowedge.IsColimit.desc (ChosenCoends.isCoend F) f hf
-
-@[reassoc (attr := simp)]
-lemma chosenCoend.ι_desc (j : J) : chosenCoend.ι F j ≫ chosenCoend.desc f hf = f j := by
-  apply IsColimit.fac
-
-def chosenCoend.map {G : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) : chosenCoend F ⟶ chosenCoend G :=
-  chosenCoend.desc (fun x ↦ (f.app (op x)).app x ≫ chosenCoend.ι _ _) (fun j j' φ ↦ by
-    simp [chosenCoend.condition])
-
-@[reassoc (attr := simp)]
-lemma chosenCoend.ι_map {G : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (j : J) :
-    chosenCoend.ι F j ≫ chosenCoend.map f = (f.app _).app _ ≫ chosenCoend.ι G j := by
-  simp [chosenCoend.map]
-
-def chosenCoend.uniq (c : Cowedge F) (hc : IsColimit c) : c.pt ≅ chosenCoend F :=
-  hc.coconePointUniqueUpToIso (ChosenCoends.isCoend _)
-
-@[simp]
-lemma chosenCoend.map_id : chosenCoend.map (𝟙 F) = 𝟙 _ := by cat_disch
-
-@[reassoc (attr := simp)]
-lemma chosenCoend.map_comp {G H : Jᵒᵖ ⥤ J ⥤ C} (f : F ⟶ G) (g : G ⟶ H) :
-    chosenCoend.map f ≫ chosenCoend.map g = chosenCoend.map (f ≫ g) := by
-  cat_disch
-
-@[simps]
-def chosenCoendFunctor : (Jᵒᵖ ⥤ J ⥤ C) ⥤ C where
-  obj := chosenCoend
-  map := chosenCoend.map
-
-end
-
-section
-
-@[simps -isSimp]
-instance : Limits.ChosenCoends.{v, u} (Type max w u) where
-  cowedge := Types.cowedge
-  isCoend := Types.cowedgeIsColimit
-
-section GeneralUniverse
-
-variable {J : Type u} [Category.{v} J] {F : Jᵒᵖ ⥤ J ⥤ Type max w u}
-
-lemma chosenCoend.ι_apply (j : J) (x : (F.obj (op j)).obj j) :
-    chosenCoend.ι F j x = Quot.mk _ ⟨j, x⟩ :=
-  rfl
-
-lemma chosenCoend.desc_apply {X : Type max w u} (f : ∀ j, (F.obj (op j)).obj j ⟶ X)
-    (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j)
-    (x : chosenCoend F) : chosenCoend.desc f hf x =
-      Quot.lift (fun j ↦ f j.fst j.snd) (fun _ _ h ↦ by
-        cases h with | mk f x => exact ConcreteCategory.congr_hom (hf f) _) x :=
-  rfl
-
-lemma chosenCoend.map_apply {G : Jᵒᵖ ⥤ J ⥤ Type max w u} (f : F ⟶ G) (x : chosenCoend F) :
-    chosenCoend.map f x = Quot.map (fun ⟨j, y⟩ ↦ ⟨j, (f.app _).app _ y⟩) (fun _ _ h ↦ by
-      cases h with | mk g x =>
-        convert Types.coendRel.mk g ((f.app _).app _ x)
-        · simp only [← NatTrans.comp_app_apply, f.naturality]
-        · simp [← NatTrans.naturality_apply]) x :=
-  rfl
-
-end GeneralUniverse
-
-section Small
-
-open scoped TypeCat
-
-variable {J : Type u} [Category.{u} J]
-
-@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
-def adjoint : Type u ⥤ Jᵒᵖ ⥤ J ⥤ Type u where
-  obj X := (Functor.postcompose₂.obj (yoneda.obj X)).obj
-    (yoneda ⋙ (opOpEquivalence (Type u)).congrRight.inverse ⋙
-      (Functor.opUnopEquiv J (Type uᵒᵖ)).inverse).leftOp
-  map f := { app c := { app d := TypeCat.ofHom fun g ↦ g ≫ f } }
-
-set_option backward.isDefEq.respectTransparency false in
-def chosenCoendAdjunction : chosenCoendFunctor (C := Type u) (J := J) ⊣ adjoint (J := J) where
-  unit := {
-    app F := {
-      app j := { app j' := ↾fun f ↦ ↾fun g ↦ Quot.mk _ ⟨j.unop, (F.obj _).map g f⟩ }
-      naturality _ _ f := by
-        ext j x
-        dsimp
-        ext g
-        dsimp
-        apply Quot.sound
-        have := Types.coendRel.mk f.unop ((F.obj _).map g x)
-        simp_all }
-    naturality F G f := by
-      ext j j' x
-      dsimp
-      ext g
-      dsimp [chosenCoend.map_apply, Quot.map]
-      apply Quot.sound
-      simpa using Types.coendRel.mk (𝟙 (unop j)) ((G.obj _).map g ((f.app _).app _ x)) }
-  counit := {
-    app X := ↾Quot.lift (fun ⟨j, (x : (j ⟶ j) ⟶ X)⟩ ↦ x (𝟙 j)) (fun _ _ h ↦ by induction h; simp) }
-  left_triangle_components := by
-    intro F
-    ext x
-    obtain ⟨x, rfl⟩ := Quot.mk_surjective x
-    simp [chosenCoend.map_apply, Quot.map]
-
-variable {I : Type u} [Category.{u} I] -- (F : Iᵒᵖ ⥤ I ⥤ Jᵒᵖ ⥤ J ⥤ Type u)
-
-def iso' : adjoint (J := I) ⋙ Functor.postcompose₂.obj (adjoint (J := J)) ≅
-    (adjoint (J := J) ⋙ Functor.postcompose₂.obj (adjoint (J := I))) ⋙
-      Functor.flipping₃₄₁₂.inverse :=
-  NatIso.ofComponents fun X ↦ NatIso.ofComponents fun i ↦ NatIso.ofComponents fun i' ↦
-    NatIso.ofComponents fun j ↦ NatIso.ofComponents fun j' ↦ {
-      hom := ↾fun x ↦ ↾fun y ↦ ↾fun z ↦ (x.hom z).hom y
-      inv := ↾fun x ↦ ↾fun y ↦ ↾fun z ↦ (x.hom z).hom y }
-
-def fubini :
-    Functor.postcompose₂.obj (chosenCoendFunctor (J := J) (C := Type u)) ⋙
-      chosenCoendFunctor (J := I) ≅
-    Functor.flipping₃₄₁₂.functor ⋙ Functor.postcompose₂.obj (chosenCoendFunctor (J := I)) ⋙
-      chosenCoendFunctor (J := J) :=
-  (conjugateIsoEquiv (Adjunction.comp Functor.flipping₃₄₁₂.toAdjunction
-    (((chosenCoendAdjunction.whiskerRight _ ).whiskerRight _).comp chosenCoendAdjunction))
-    (((chosenCoendAdjunction.whiskerRight _ ).whiskerRight _).comp chosenCoendAdjunction)).symm <|
-      NatIso.ofComponents fun X ↦ NatIso.ofComponents fun i ↦ NatIso.ofComponents fun i' ↦
-        NatIso.ofComponents fun j ↦ NatIso.ofComponents fun j' ↦ {
-          hom := ↾fun x ↦ ↾fun y ↦ ↾fun z ↦ (x.hom z).hom y
-          inv := ↾fun x ↦ ↾fun y ↦ ↾fun z ↦ (x.hom z).hom y }
-
-end Small
-
-end
-
-end Limits
+namespace CategoryTheory
 
 namespace Profunctor
 
@@ -256,8 +47,7 @@ section Definition
 
 variable {C : Type*} [Category* C] {D : Type u} [Category.{v} D] {E : Type*} [Category* E]
 
-open Opposite
-
+/-- The bifunctor whose coend defines the composite of two profunctors. -/
 @[simps! obj_obj obj_map map_app]
 def compDiagram (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y : E) :
     Dᵒᵖ ⥤ D ⥤ Type max w w' where
@@ -266,6 +56,7 @@ def compDiagram (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y :
     map f := TypeCat.ofHom (Prod.map id ((Q.map f).app _)) }
   map g := { app U := TypeCat.ofHom (Prod.map ((P.obj _).map g) id) }
 
+/-- The map on composition diagrams induced by morphisms in the outer variables. -/
 @[simps]
 def compDiagramMap (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
     {X X' : C} {Y Y' : E} (f : X ⟶ X') (g : Y ⟶ Y') :
@@ -285,21 +76,101 @@ lemma compDiagramMap_comp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
 
 open Limits
 
-variable [Limits.ChosenCoends.{v, u} (Type (max w w'))]
-
+/-- Composition of profunctors using a chosen coend construction. -/
 @[simps! obj_obj obj_map map_app]
-def univComp (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) :
-    Profunctor.{max w w'} C E :=
+def univComp [Limits.ChosenCoends.{v, u} (Type (max w w'))]
+    (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) : Profunctor.{max w w'} C E :=
   .ofCore {
     obj X Y := chosenCoend <| compDiagram P Q X Y
     map f g := chosenCoend.map <| compDiagramMap P Q f g }
 
+/-- Composition of profunctors in the standard universe configuration. -/
 @[simps! obj_obj obj_map map_app]
-def comp (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) : Profunctor.{u} C E :=
-  Profunctor.univComp.{u, u} P Q
+def comp (P : Profunctor.{max u w} C D) (Q : Profunctor.{max u w} D E) : Profunctor.{max u w} C E :=
+  Profunctor.univComp.{max u w, max u w} P Q
 
 end Definition
 
+section Whisker
+
+open TypeCat Limits Types Functor
+
+variable {C D E : Type u} [Category* C] [Category* D] [Category* E]
+
+section Left
+
+variable (P : Profunctor.{max u w} C D) {Q R : Profunctor.{max u w} D E} (f : Q ⟶ R)
+
+set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] chosenCoend.map_apply in
+/-- Left whiskering of a natural transformation of profunctors. -/
+@[simps app_app]
+def whiskerLeft : P.comp Q ⟶ P.comp R where
+  app X := {
+    app Y := chosenCoend.map { app d := {
+      app d' := ↾Prod.map id ((f.app d').app Y)
+      naturality _ _ _ := by
+        ext
+        dsimp
+        apply Prod.ext <;>
+        simp [← comp_apply, -types_comp_apply] } }
+    naturality _ _ _ := by ext ⟨_, _, _⟩; simp }
+  naturality _ _ _ := by ext _ ⟨_, _, _⟩; simp
+
+variable (Q) in
+@[simp]
+lemma whiskerLeft_id : P.whiskerLeft (𝟙 Q) = 𝟙 (P.comp Q) := by
+  ext _ _ ⟨_, _, _⟩
+  rfl
+
+@[simp]
+lemma whiskerLeft_comp {S : Profunctor.{max u w} D E} (f : Q ⟶ R) (g : R ⟶ S) :
+    P.whiskerLeft (f ≫ g) = P.whiskerLeft f ≫ P.whiskerLeft g := by
+  ext _ _ ⟨_, _, _⟩
+  rfl
+
+end Left
+
+section Right
+
+variable {P Q : Profunctor.{max u w} C D} (R : Profunctor.{max u w} D E) (f : P ⟶ Q)
+
+set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] chosenCoend.map_apply in
+/-- Right whiskering of a natural transformation of profunctors. -/
+@[simps app_app]
+def whiskerRight : P.comp R ⟶ Q.comp R where
+  app X := { app Y := chosenCoend.map { app d := { app d' := ↾Prod.map ((f.app _).app _) id } } }
+  naturality _ _ _ := by
+    ext _ ⟨_, _, _⟩
+    dsimp
+    apply Quot.sound
+    rw [coendRel_iff]
+    exact ⟨𝟙 _, by simp [← comp_apply, -types_comp_apply]⟩
+
+@[simp]
+lemma id_whiskerRight : whiskerRight R (𝟙 P) = 𝟙 (P.comp R) := by
+  ext _ _ ⟨_, _, _⟩
+  rfl
+
+@[simp]
+lemma comp_whiskerRight {R : Profunctor.{max u w} C D} (f : P ⟶ Q) (g : Q ⟶ R)
+    (S : Profunctor.{max u w} D E) :
+    whiskerRight S (f ≫ g) = whiskerRight S f ≫ whiskerRight S g := by
+  ext _ _ ⟨_, _, _⟩
+  rfl
+
+end Right
+
+@[simp]
+lemma whisker_exchange {P Q : Profunctor.{max u w} C D} {R S : Profunctor.{max u w} D E}
+    (f : P ⟶ Q) (g : R ⟶ S) :
+    P.whiskerLeft g ≫ whiskerRight S f = whiskerRight R f ≫ Q.whiskerLeft g := by
+  ext _ _ ⟨_, _, _⟩
+  rfl
+
+end Whisker
+
 section LeftUnitor
 
 variable {C : Type u} [Category.{u} C] {D : Type u} [Category* D]
@@ -307,25 +178,31 @@ variable {C : Type u} [Category.{u} C] {D : Type u} [Category* D]
 open Limits TypeCat
 
 set_option backward.isDefEq.respectTransparency false in
+/-- The left unitor isomorphism `Profunctor.id.comp P ≅ P` for composition of profunctors. -/
 @[simps! hom_app_app inv_app_app]
 def leftUnitor (P : Profunctor.{u} C D) : Profunctor.id.comp P ≅ P :=
   NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ {
-      hom := ↾Quot.lift (fun ⟨d, f, x⟩ ↦ (P.map f).app _ x) fun _ _ h ↦ by cases h; simp
-      inv := ↾fun x ↦ Quot.mk _ ⟨X, 𝟙 X, x⟩
-      hom_inv_id := by
-        ext x
-        obtain ⟨⟨_, f, x⟩, rfl⟩ := Quot.mk_surjective x
-        symm
-        apply Quot.sound
-        dsimp
-        have := Types.coendRel.mk (F := compDiagram Profunctor.id.{u} P X (unop Y)) f ⟨𝟙 X, x⟩
-        cat_disch })
+    hom := ↾Quot.lift (fun ⟨d, f, x⟩ ↦ (P.map f).app _ x) fun _ _ ↦ by rintro ⟨f, x⟩; simp
+    inv := ↾fun x ↦ Quot.mk _ ⟨X, 𝟙 X, x⟩
+    hom_inv_id := by
+      ext ⟨_, f, x⟩
+      symm
+      apply Quot.sound
+      rw [Types.coendRel_iff]
+      exact ⟨f, ⟨𝟙 X, x⟩, by cat_disch⟩ })
     (fun f ↦ by dsimp; ext; simp [compDiagram, chosenCoend.ι_apply _]))
-    (fun f ↦ by
-      ext _ z
-      simp [chosenCoend.map_apply, Quot.map]
-      obtain ⟨_, rfl⟩ := Quot.mk_surjective z
-      simp)
+    (fun f ↦ by ext _ ⟨_, _⟩; simp [chosenCoend.map_apply])
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma id_whiskerLeft {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
+    (Profunctor.id (C := C)).whiskerLeft f =
+      (P.leftUnitor).hom ≫ f ≫ (Q.leftUnitor).inv := by
+  ext _ _ ⟨_, g, _⟩
+  dsimp [chosenCoend.map_apply, Quot.map]
+  apply Quot.sound
+  rw [Types.coendRel_iff]
+  exact ⟨g, by simp [← comp_apply, -types_comp_apply]⟩
 
 end LeftUnitor
 
@@ -336,432 +213,181 @@ open Limits TypeCat
 variable {C : Type u} [Category* C] {D : Type u} [Category.{u} D]
 
 set_option backward.isDefEq.respectTransparency false in
+/-- The right unitor isomorphism `P.comp Profunctor.id ≅ P` for composition of profunctors. -/
 @[simps! hom_app_app inv_app_app]
 def rightUnitor (P : Profunctor.{u} C D) : P.comp .id ≅ P :=
   NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ {
-      hom := ↾Quot.lift (fun ⟨d, x, f⟩ ↦ (P.obj X).map f.op x) fun _ _ h ↦ by cases h; simp
-      inv := ↾fun x ↦ Quot.mk _ ⟨Y.unop, x, 𝟙 Y.unop⟩
-      hom_inv_id := by
-        ext x
-        obtain ⟨⟨_, x, f⟩, rfl⟩ := Quot.mk_surjective x
-        apply Quot.sound
-        dsimp
-        have := Types.coendRel.mk (F := compDiagram P (.id (C := D)) X (unop Y)) f ⟨x, 𝟙 _⟩
-        cat_disch })
+    hom := ↾Quot.lift (fun ⟨d, x, f⟩ ↦ (P.obj X).map f.op x) fun _ _ h ↦ by cases h; simp
+    inv := ↾fun x ↦ Quot.mk _ ⟨Y.unop, x, 𝟙 Y.unop⟩
+    hom_inv_id := by
+      ext ⟨_, x, f⟩
+      apply Quot.sound
+      rw [Types.coendRel_iff]
+      exact ⟨f, ⟨x, 𝟙 (unop Y)⟩, by cat_disch⟩ })
     (fun f ↦ by dsimp; ext; simp [compDiagram, chosenCoend.ι_apply _]))
-    (fun f ↦ by
-      ext _ z
-      simp [chosenCoend.map_apply, Quot.map]
-      obtain ⟨_, rfl⟩ := Quot.mk_surjective z
-      simp)
+    (fun f ↦ by ext _ ⟨_, _⟩; simp [chosenCoend.map_apply])
 
-end RightUnitor
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma whiskerRight_id {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
+    whiskerRight (Profunctor.id (C := D)) f =
+      (P.rightUnitor).hom ≫ f ≫ (Q.rightUnitor).inv := by
+  ext _ _ ⟨_, _, g⟩
+  dsimp [chosenCoend.map_apply, Quot.map]
+  symm
+  apply Quot.sound
+  rw [Types.coendRel_iff]
+  exact ⟨g, by simp⟩
 
-section Associator
 
-variable {C D E F : Type u} [Category.{u} C] [Category.{u} D] [Category.{u} E] [Category.{u} F]
-variable (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) (R : Profunctor.{u} E F)
+end RightUnitor
 
-open TypeCat Limits Types Functor MonoidalCategory
+section Associator
 
-variable (X : C) (Y : F)
+variable {C D E F : Type u} [Category* C] [Category* D] [Category* E] [Category* F]
+  (P : Profunctor.{max w u} C D) (Q : Profunctor.{max w u} D E) (R : Profunctor.{max w u} E F)
 
-@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
-def compDiagram₃ : Dᵒᵖ ⥤ D ⥤ Eᵒᵖ ⥤ E ⥤ Type u where
-  obj U := {
-    obj V := (postcompose₂.obj (tensorLeft ((P.obj X).obj U))).obj <| Q.compDiagram R V Y
-    map f := (postcompose₂.obj (tensorLeft ((P.obj X).obj U))).map (Q.compDiagramMap R f (𝟙 _))
-  }
-  map g := { app U := (postcompose₂.map { app V := (P.obj _).map g ▷ _ }).app _ }
+open TypeCat Limits Types Functor
 
-@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
-def compDiagram₃' : Eᵒᵖ ⥤ E ⥤ Dᵒᵖ ⥤ D ⥤ Type u where
-  obj U := {
-    obj V := (postcompose₂.obj (tensorRight ((R.obj V).obj (Opposite.op Y)))).obj <|
-      P.compDiagram Q X (unop U)
-    map f := (postcompose₂.map { app V := _ ◁ (R.map f).app _ }).app _
-  }
-  map g := { app _ := (postcompose₂.obj _).map <| P.compDiagramMap _ (𝟙 _) g.unop }
-
-def compDiagram₃Iso : (compDiagram₃ P Q R X Y) ≅
-    flipping₃₄₁₂.functor.obj (compDiagram₃' P Q R X Y) :=
-  NatIso.ofComponents fun d ↦ NatIso.ofComponents fun d' ↦ NatIso.ofComponents fun e ↦
-    NatIso.ofComponents fun e' ↦ (Equiv.prodAssoc _ _ _).symm.toIso
-
-instance (X : Type u) : IsLeftAdjoint (tensorRight X) :=
-  Functor.isLeftAdjoint_of_iso (BraidedCategory.tensorLeftIsoTensorRight X)
-
-noncomputable def compIso₃ (X : C) (Y : Fᵒᵖ) :
-    (postcompose₂.obj chosenCoendFunctor ⋙ chosenCoendFunctor).obj (compDiagram₃' P Q R X Y.unop) ≅
-      (((P.comp Q).comp R).obj X).obj Y := by
-  refine chosenCoendFunctor.mapIso (NatIso.ofComponents
-      (fun e ↦ NatIso.ofComponents (fun e' ↦ ?_) ?_) ?_)
-  · refine ((ChosenCoends.isCoend
-      (((P.compDiagram₃' Q R X (unop Y)).obj e).obj e'))).coconePointsIsoOfEquivalence
-        (isColimitOfPreserves (tensorRight ((R.obj e').obj Y))
-          (ChosenCoends.isCoend (P.compDiagram Q X (unop e))))
-        Equivalence.refl (NatIso.ofComponents ?_ ?_)
-    · rintro (_ | _)
-      exacts [Iso.refl _, Iso.refl _]
-    · rintro (_ | _) (_ | _) (_ | _ | _)
-      all_goals cat_disch
-  · cat_disch
-  · intro X Y f
-    ext : 2
-    apply chosenCoend.hom_ext
-    intro j
-    dsimp
-    ext x
-    · apply Quot.sound
-      convert coendRel.mk (𝟙 j) _
-      rotate_right
-      · exact (x.1.1, (Q.obj j).map f x.1.2)
-      · apply Prod.ext
-        · simp; rfl
-        · rfl
-      · apply Prod.ext
-        · simp; rfl
-        · simp; rfl
-    · rfl
-
-noncomputable def compIso₃' (X : C) (Y : Fᵒᵖ) :
-    (postcompose₂.obj chosenCoendFunctor ⋙ chosenCoendFunctor).obj (compDiagram₃ P Q R X Y.unop) ≅
-      ((P.comp (Q.comp R)).obj X).obj Y := by
-  refine chosenCoendFunctor.mapIso (NatIso.ofComponents
-      (fun d ↦ NatIso.ofComponents (fun d' ↦ ?_) ?_) ?_)
-  · refine ((ChosenCoends.isCoend
-      (((P.compDiagram₃ Q R X (unop Y)).obj d).obj d'))).coconePointsIsoOfEquivalence
-        (isColimitOfPreserves (tensorLeft ((P.obj X).obj d))
-          (ChosenCoends.isCoend (Q.compDiagram R d' (unop Y))))
-        Equivalence.refl (NatIso.ofComponents ?_ ?_)
-    · rintro (_ | _)
-      exacts [Iso.refl _, Iso.refl _]
-    · rintro (_ | _) (_ | _) (_ | _ | _)
-      all_goals cat_disch
-  · cat_disch
-  · intro X Y f
-    ext : 2
-    apply chosenCoend.hom_ext
-    intro j
-    dsimp
-    ext x
-    · rfl
-    · apply Quot.sound
-      convert coendRel.mk (𝟙 j) _
-      rotate_right
-      · exact (x.2.1, x.2.2)
-      · apply Prod.ext
-        · simp; rfl
-        · rfl
-      · apply Prod.ext
-        · rfl
-        · simp; rfl
-
-noncomputable def associatorComponents' (X : C) (Y : Fᵒᵖ) :
-    (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y :=
-  (compIso₃ P Q R X Y).symm ≪≫ fubini.app (P.compDiagram₃' Q R X (unop Y)) ≪≫
-    (_ ⋙ chosenCoendFunctor).mapIso (compDiagram₃Iso P Q R X (unop Y)).symm ≪≫ compIso₃' P Q R X Y
-
-lemma associatorComponents'_apply (X : C) (Y : Fᵒᵖ) (d : D) (e : E)
-    (r : (R.obj e).obj Y) (p : (P.obj X).obj (Opposite.op d)) (q : (Q.obj d).obj (Opposite.op e)) :
-    (associatorComponents' P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩) =
-      Quot.mk _ ⟨d, (p, Quot.mk _ ⟨e, (q, r)⟩)⟩ := by
-  sorry
-
-lemma relation_map {α β : Type*} (f : α → β) (r : β → β → Prop) (x y : α)
-    (h : Relation.EqvGen (fun x y ↦ r (f x) (f y)) x y) :
-    Relation.EqvGen r (f x) (f y) := by
-  induction h with
-  | rel => exact Relation.EqvGen.rel _ _ (by assumption)
-  | refl => exact Relation.EqvGen.refl _
-  | symm => exact Relation.EqvGen.symm _ _ (by assumption)
-  | trans => exact Relation.EqvGen.trans _ _ _ (by assumption) (by assumption)
+set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] chosenCoend.map_apply in
+lemma associatorComponents_aux₁ {X : C} {Y : Fᵒᵖ} {e e' : E} {d d' : D}
+    {p : (P.obj X).obj (Opposite.op d)} {q : (Q.obj d).obj (Opposite.op e)}
+    {p' : (P.obj X).obj (Opposite.op d')} {q' : (Q.obj d').obj (Opposite.op e')}
+    {f : e ⟶ e'} {r : (R.obj e).obj Y}
+    (h : Relation.EqvGen (coendRel (P.compDiagram Q X e))
+      ⟨d', p', (Q.obj d').map f.op q'⟩ ⟨d, p, q⟩) :
+    Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))
+      ⟨d', p', Quot.mk _ ⟨e', (q', (R.map f).app Y r)⟩⟩
+      ⟨d, p, Quot.mk _ ⟨e, (q, r)⟩⟩ := by
+  replace h := Relation.EqvGen.map (fun ⟨d, p, q⟩ ↦ ⟨d, (p, Quot.mk _ ⟨e, q, r⟩)⟩)
+      (Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))) _ _ (h.mono <| by
+    intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
+    apply Relation.EqvGen.rel
+    rw [coendRel_iff] at h ⊢
+    obtain ⟨f, x, h₁, h₂⟩ := h
+    use f
+    simp_all [Prod.ext_iff])
+  simp only [Relation.EqvGen.idempotent] at h
+  refine Relation.EqvGen.trans _ _ _ ?_ h
+  apply Relation.EqvGen.rel
+  rw [coendRel_iff]
+  exact ⟨𝟙 _, by simpa using (Quot.sound <| coendRel.mk (F := Q.compDiagram R _ _) f (_, _)).symm⟩
 
-@[simp]
-lemma Relation.eqvGen_eqvGen {α : Type*} (r : α → α → Prop) :
-    Relation.EqvGen (Relation.EqvGen r) = Relation.EqvGen r := by
-  ext x y
-  refine ⟨fun h ↦ ?_, fun h ↦ Relation.EqvGen.rel _ _ h⟩
-  induction h with
-  | rel => assumption
-  | refl => exact Relation.EqvGen.refl _
-  | symm => exact Relation.EqvGen.symm _ _ (by assumption)
-  | trans => exact Relation.EqvGen.trans _ _ _ (by assumption) (by assumption)
+set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] chosenCoend.map_apply in
+lemma associatorComponents_aux₂ {X : C} {Y : Fᵒᵖ} {d d' : D} {e e' : E}
+  {q : (Q.obj d).obj (Opposite.op e)} {r : (R.obj e).obj Y}
+  {q' : (Q.obj d').obj (Opposite.op e')}
+  {r' : (R.obj e').obj Y} {f : d ⟶ d'} {p : (P.obj X).obj (Opposite.op d')}
+  (h : Relation.EqvGen (coendRel (Q.compDiagram R d' (unop Y)))
+    ⟨e, ((ConcreteCategory.hom ((Q.map f).app (Opposite.op e))) q, r)⟩ ⟨e', (q', r')⟩) :
+  Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))
+    ⟨e, (Quot.mk (coendRel (P.compDiagram Q X e)) ⟨d, (P.obj X).map f.op p, q⟩, r)⟩
+    ⟨e', (Quot.mk (coendRel (P.compDiagram Q X e')) ⟨d', (p, q')⟩, r')⟩ := by
+  replace h := Relation.EqvGen.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d', p, q⟩, r⟩)
+      (Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))) _ _ (h.mono <| by
+    intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
+    apply Relation.EqvGen.rel
+    rw [coendRel_iff] at h ⊢
+    obtain ⟨f, x, h₁, h₂⟩ := h
+    exact ⟨f, by simp_all [Prod.ext_iff]⟩)
+  simp only [Relation.EqvGen.idempotent] at h
+  refine (Relation.EqvGen.trans _ _ _ ?_ h)
+  apply Relation.EqvGen.rel
+  rw [coendRel_iff]
+  exact ⟨𝟙 _, by simpa using Quot.sound <| coendRel.mk (F := P.compDiagram Q _ _) f (_, _)⟩
 
 set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] chosenCoend.map_apply in
+/-- The objectwise components of the associator isomorphism
+`(P.comp Q).comp R ≅ P.comp (Q.comp R)`. -/
 @[simps hom inv]
 def associatorComponents (X : C) (Y : Fᵒᵖ) :
     (P.comp Q |>.comp R |>.obj X |>.obj Y) ≅ P.comp (Q.comp R) |>.obj X |>.obj Y where
   hom := by
     refine ↾Quot.lift (fun ⟨e, x, r⟩ ↦
-        Quot.map (fun ⟨d, p, q⟩ ↦ ⟨d, p, Quot.mk _ ⟨e, q, r⟩⟩) ?_ x) ?_
-    · intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
-      cases h with
-      | mk f x =>
-        convert coendRel.mk (F := (P.compDiagram (Q.comp R) X (unop Y)))
-          f ⟨x.1, Quot.mk _ ⟨e, x.2, r⟩⟩
-        dsimp
-        ext
-        · rfl
-        · apply Quot.sound
-          convert coendRel.mk (F := Q.compDiagram R d' (unop Y)) (𝟙 e) ⟨(Q.map f).app _ x.2, r⟩
-          · simp
-          · apply Prod.ext
-            · rfl
-            · simp; rfl
+      Quot.map (fun ⟨d, p, q⟩ ↦ ⟨d, p, Quot.mk _ ⟨e, q, r⟩⟩) ?_ x) ?_
+    · rintro ⟨d, p, q⟩ ⟨d', p', q'⟩ ⟨f, x⟩
+      rw [coendRel_iff]
+      exact ⟨f, by simp⟩
     · rintro ⟨e, ⟨d, p, q⟩, r⟩ ⟨e', ⟨d', p', q'⟩, r'⟩ h
       dsimp
       rw [coendRel_iff] at h
       obtain ⟨f, ⟨x, r''⟩, h₁, h₂⟩ := h
-      simp only [compDiagram_obj_obj, comp_obj_obj, op_unop, compDiagram_map_app, comp_obj_map,
-        Quiver.Hom.unop_op, hom_ofHom, Fun.coe_mk, Prod.map_apply, id_eq, Prod.mk.injEq,
-        compDiagram_obj_map] at h₁ h₂
+      dsimp at h₁ h₂
+      simp only [map_id, NatTrans.id_app, Prod.mk.injEq] at h₁
       obtain ⟨rfl, rfl⟩ := h₂
       obtain ⟨h₁, rfl⟩ := h₁
-      simp only [chosenCoend.map_apply, Quot.map, compDiagram_obj_obj, compDiagramMap_app_app,
-        map_id, NatTrans.id_app, ofHom_apply, Prod.map_apply, id_apply] at h₁
+      dsimp at h₁
       symm
-      simp only [Quot.map]
+      dsimp [Quot.map]
       rw [Quot.eq] at h₁ ⊢
-      have h₁' := relation_map (fun ⟨d, p, q⟩ ↦ ⟨d, (p, Quot.mk _ ⟨e, q, r''⟩)⟩)
-          (Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))) _ _ (h₁.mono <| by
-        intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
-        apply Relation.EqvGen.rel
-        simp only [compDiagram_obj_obj, op_unop, comp_obj_obj, coendRel_iff, compDiagram_map_app,
-          hom_ofHom, Fun.coe_mk, compDiagram_obj_map, comp_map_app, Prod.exists, Prod.map_apply,
-          id_eq, Prod.mk.injEq, ↓existsAndEq, and_true, true_and]
-        rw [coendRel_iff] at h
-        obtain ⟨f, x, h₁, h₂⟩ := h
-        use f
-        simp_all [Prod.ext_iff, chosenCoend.map_apply, Quot.map])
-      simp only [compDiagram_obj_obj, op_unop, comp_obj_obj, Relation.eqvGen_eqvGen] at h₁'
-      refine (Relation.EqvGen.trans _ _ _ ?_ h₁')
-      apply Relation.EqvGen.rel
-      rw [coendRel_iff]
-      use 𝟙 _
-      simp only [compDiagram_obj_obj, op_unop, comp_obj_obj, op_id, map_id, NatTrans.id_app,
-        id_apply, compDiagram_obj_map, ofHom_apply, exists_eq_left, Prod.map_apply, id_eq,
-        Prod.mk.injEq, true_and]
-      symm
-      apply Quot.sound
-      exact coendRel.mk (F := Q.compDiagram R _ _) f (_, _)
+      exact associatorComponents_aux₁ _ _ _ h₁
   inv := by
     refine ↾Quot.lift (fun ⟨d, p, x⟩ ↦
         Quot.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d, p, q⟩, r⟩) ?_ x) ?_
-    · intro ⟨e, q, r⟩ ⟨e', q', r'⟩ h
-      cases h with
-      | mk f x =>
-        convert coendRel.mk (F := (P.comp Q).compDiagram R X (unop Y))
-          f ⟨_, _⟩
-        dsimp
-        ext
-        · apply Quot.sound
-          convert coendRel.mk (F := P.compDiagram Q X e) (𝟙 d) ⟨p, (Q.obj _).map f.op x.1⟩
-          · apply Prod.ext
-            · simp
-            · rfl
-          · simp; rfl
-        · rfl
+    · rintro ⟨e, q, r⟩ ⟨e', q', r'⟩ ⟨f, x⟩
+      rw [coendRel_iff]
+      use f
+      simp
     · rintro ⟨d, p, e, q, r⟩ ⟨d', p', e', q', r'⟩ h-- ⟨e', ⟨d', p', q'⟩, r'⟩ h
       dsimp
       rw [coendRel_iff] at h
       obtain ⟨f, ⟨p, x⟩, h₁, h₂⟩ := h
-      simp only [compDiagram_obj_obj, op_unop, comp_obj_obj, compDiagram_map_app, hom_ofHom,
-        Fun.coe_mk, Prod.map_apply, id_eq, Prod.mk.injEq, compDiagram_obj_map,
-        comp_map_app] at h₁ h₂
+      dsimp at h₁ h₂
+      simp only [map_id, Prod.mk.injEq] at h₂
       obtain ⟨rfl, rfl⟩ := h₁
       obtain ⟨rfl, h₂⟩ := h₂
-      simp only [chosenCoend.map_apply, Quot.map, compDiagram_obj_obj, op_unop,
-        compDiagramMap_app_app, op_id, map_id, ofHom_apply, Prod.map_apply, id_apply] at h₂
+      dsimp at h₂
       dsimp [Quot.map]
       rw [Quot.eq] at h₂ ⊢
-      have h₂' := relation_map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d', p, q⟩, r⟩)
-          (Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))) _ _ (h₂.mono <| by
-        intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
-        apply Relation.EqvGen.rel
-        simp only [compDiagram_obj_obj, comp_obj_obj, op_unop, coendRel_iff, compDiagram_map_app,
-          comp_obj_map, Quiver.Hom.unop_op, hom_ofHom, Fun.coe_mk, compDiagram_obj_map, Prod.exists,
-          Prod.map_apply, id_eq, Prod.mk.injEq, ↓existsAndEq, and_true, true_and]
-        rw [coendRel_iff] at h
-        obtain ⟨f, x, h₁, h₂⟩ := h
-        use f
-        simp_all [Prod.ext_iff, chosenCoend.map_apply, Quot.map])
-      simp only [compDiagram_obj_obj, comp_obj_obj, op_unop, Relation.eqvGen_eqvGen] at h₂'
-      refine (Relation.EqvGen.trans _ _ _ ?_ h₂')
-      apply Relation.EqvGen.rel
-      rw [coendRel_iff]
-      use 𝟙 _
-      simp only [compDiagram_obj_obj, comp_obj_obj, op_unop, op_id, map_id, NatTrans.id_app,
-        id_apply, compDiagram_obj_map, ofHom_apply, exists_eq_left, Prod.map_apply, id_eq,
-        Prod.mk.injEq, and_true]
-      apply Quot.sound
-      exact coendRel.mk (F := P.compDiagram Q _ _) f (_, _)
+      exact associatorComponents_aux₂ _ _ _ h₂
   hom_inv_id := by
-    ext ⟨e, ⟨d, p, q⟩, r⟩
-    simp [Quot.map]
+    ext ⟨_, ⟨_, _, _⟩, _⟩
+    dsimp [Quot.map]
   inv_hom_id := by
-    ext ⟨d, p, ⟨e, q, r⟩⟩
-    simp [Quot.map]
-
-@[simp]
-lemma associatorComponents_apply (X : C) (Y : Fᵒᵖ) (d : D) (e : E)
-    (r : (R.obj e).obj Y) (p : (P.obj X).obj (Opposite.op d)) (q : (Q.obj d).obj (Opposite.op e)) :
-    (associatorComponents P Q R X Y).hom (Quot.mk _ ⟨e, Quot.mk _ ⟨d, (p, q)⟩, r⟩) =
-      Quot.mk _ ⟨d, (p, Quot.mk _ ⟨e, (q, r)⟩)⟩ := by
-  rfl
+    ext ⟨_, _, ⟨_, _, _⟩⟩
+    dsimp [Quot.map]
 
 set_option backward.isDefEq.respectTransparency false in
+/-- The associator isomorphism `(P.comp Q).comp R ≅ P.comp (Q.comp R)` for composition of
+profunctors. -/
 @[simps! hom_app_app inv_app_app]
-def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) := by
-  refine NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦
-    associatorComponents P Q R X Y) ?_) ?_
-  · intro f f' g
-    ext ⟨e, ⟨d, p, q⟩, r⟩
-    dsimp [-associatorComponents_hom]
-    erw [associatorComponents_apply, associatorComponents_apply]
-    simp
-  · intro f f' g
-    ext _ ⟨e, ⟨d, p, q⟩, r⟩
-    dsimp [-associatorComponents_hom]
-    erw [associatorComponents_apply, associatorComponents_apply]
-    simp
-
-end Associator
-
-section WhiskerLeft
-
-open TypeCat Limits Types Functor MonoidalCategory
-
-variable {C D E : Type u} [Category.{u} C] [Category.{u} D] [Category.{u} E]
-variable (P : Profunctor.{u} C D) {Q R : Profunctor.{u} D E} (f : Q ⟶ R)
-
-set_option backward.isDefEq.respectTransparency false in
-@[simps app_app]
-def whiskerLeft : P.comp Q ⟶ P.comp R where
-  app X := {
-    app Y := chosenCoend.map {
-      app d := {
-        app d' := ↾Prod.map id ((f.app _).app _)
-        naturality := by
-          intro d₁ d₂ g
-          ext
-          dsimp
-          apply Prod.ext
-          · simp
-          · simp [← comp_apply, -types_comp_apply] } }
-    naturality := by
-      intros
-      ext ⟨_, _, _⟩
-      simp [chosenCoend.map_apply, Quot.map] }
-  naturality := by
-    intros
-    ext _ ⟨_, _, _⟩
-    simp [chosenCoend.map_apply, Quot.map]
+def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ associatorComponents P Q R X Y)
+    fun _ ↦ by ext ⟨_, ⟨_, _, _⟩, _⟩; simp [chosenCoend.map_apply, Quot.map])
+    fun _ ↦ by ext _ ⟨_, ⟨_, _, _⟩, _⟩; simp [chosenCoend.map_apply, Quot.map]
 
-end WhiskerLeft
-
-section WhiskerRight
-
-open TypeCat Limits Types Functor MonoidalCategory
+@[simp]
+lemma comp_whiskerLeft {S : Profunctor.{max u w} E F} (f : R ⟶ S) :
+    (P.comp Q).whiskerLeft f =
+      (P.associator Q R).hom ≫ P.whiskerLeft (Q.whiskerLeft f) ≫ (P.associator Q S).inv := by
+  ext _ _ ⟨_, ⟨_, _, _⟩, _⟩
+  rfl
 
-variable {C D E : Type u} [Category.{u} C] [Category.{u} D] [Category.{u} E]
-variable {P Q : Profunctor.{u} C D} (R : Profunctor.{u} D E) (f : P ⟶ Q)
+variable {P} in
+@[simp]
+lemma whiskerRight_comp {Q : Profunctor.{max u w} C D} (f : P ⟶ Q)
+    (R : Profunctor.{max u w} D E) (S : Profunctor.{max u w} E F) :
+    whiskerRight (R.comp S) f =
+      (P.associator R S).inv ≫ whiskerRight S (whiskerRight R f) ≫ (Q.associator R S).hom := by
+  ext _ _ ⟨_, _, _, _, _⟩
+  rfl
 
-set_option backward.isDefEq.respectTransparency false in
-@[simps app_app]
-def whiskerRight : P.comp R ⟶ Q.comp R where
-  app X := { app Y := chosenCoend.map { app d := { app d' := ↾Prod.map ((f.app _).app _) id } } }
-  naturality := by
-    intros
-    ext _ ⟨_, _, _⟩
-    dsimp [chosenCoend.map_apply, Quot.map]
-    apply Quot.sound
-    rw [coendRel_iff]
-    use 𝟙 _
-    simp [← comp_apply, -types_comp_apply]
+variable {Q} in
+@[simp]
+lemma whisker_assoc {R : Profunctor.{max u w} D E}
+    (f : Q ⟶ R) (S : Profunctor.{max u w} E F) :
+    whiskerRight S (P.whiskerLeft f) =
+      (P.associator Q S).hom ≫ P.whiskerLeft (whiskerRight S f) ≫ (P.associator R S).inv := by
+  ext _ _ ⟨_, ⟨_, _, _⟩, _⟩
+  rfl
 
-end WhiskerRight
+end Associator
 
 end Composition
 
-section Bicategory
-
-@[nolint checkUnivs]
-structure ProfCat where
-  of ::
-  obj : Type u
-  [str : Category.{v} obj]
-
-instance : CoeSort ProfCat (Type u) :=
-  ⟨ProfCat.obj⟩
-
-attribute [instance] ProfCat.str
-
-open Limits Types
-
-set_option backward.isDefEq.respectTransparency false in
-instance : Bicategory ProfCat.{u, u} where
-  Hom X Y := Profunctor.{u} X Y
-  id X := .id
-  comp P Q := P.comp Q
-  whiskerLeft P _ _ f := P.whiskerLeft f
-  whiskerRight f R := whiskerRight R f
-  associator P Q R := P.associator Q R
-  leftUnitor P := P.leftUnitor
-  rightUnitor P := P.rightUnitor
-  whiskerLeft_id _ _ := by
-    ext _ _ ⟨_, _, _⟩
-    rfl
-  whiskerLeft_comp _ _ _ _ _ _ := by
-    ext _ _ ⟨_, _, _⟩
-    rfl
-  id_whiskerLeft _ := by
-    ext _ _ ⟨_, f, _⟩
-    dsimp [chosenCoend.map_apply, Quot.map]
-    apply Quot.sound
-    rw [coendRel_iff]
-    use f
-    simp [← comp_apply, -types_comp_apply]
-  comp_whiskerLeft _ _ _ _ _ := by
-    ext _ _ ⟨_, ⟨_, _, _⟩, _⟩
-    rfl
-  id_whiskerRight _ _ := by
-    ext _ _ ⟨_, _, _⟩
-    rfl
-  comp_whiskerRight _ _ _ := by
-    ext _ _ ⟨_, _, _⟩
-    rfl
-  whiskerRight_id _ := by
-    ext _ _ ⟨_, _, f⟩
-    dsimp [chosenCoend.map_apply, Quot.map]
-    symm
-    apply Quot.sound
-    rw [coendRel_iff]
-    use f
-    simp [← comp_apply, -types_comp_apply]
-  whiskerRight_comp _ _ _ := by
-    ext _ _ ⟨_, _, _, _, _⟩
-    rfl
-  whisker_assoc _ _ _ _ _ := by
-    ext _ _ ⟨_, ⟨_, _, _⟩, _⟩
-    rfl
-  whisker_exchange _ _ := by
-    ext _ _ ⟨_, _, _⟩
-    rfl
-  pentagon _ _ _ _ := by
-    ext _ _ ⟨_, ⟨_, ⟨_, _, _⟩, _⟩, _⟩
-    rfl
-  triangle _ _ := by
-    ext _ _ ⟨_, ⟨_, _, f⟩, _⟩
-    dsimp [chosenCoend.map_apply, Quot.map]
-    symm
-    apply Quot.sound
-    rw [coendRel_iff]
-    use f
-    simp
-
-end Bicategory
-
 end Profunctor
 
 end CategoryTheory
diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index ae375083e14295..8ae770aff4542e 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -766,6 +766,24 @@ theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : Eq
   | symm a b _ ih => exact EqvGen.symm _ _ ih
   | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
 
+lemma map {α β : Type*} (f : α → β) (r : β → β → Prop) (x y : α)
+    (h : EqvGen (fun x y ↦ r (f x) (f y)) x y) : EqvGen r (f x) (f y) := by
+  induction h with
+  | rel => apply EqvGen.rel; assumption
+  | refl => exact EqvGen.refl _
+  | symm => apply EqvGen.symm; assumption
+  | trans => apply EqvGen.trans <;> assumption
+
+@[simp]
+lemma idempotent {α : Type*} (r : α → α → Prop) : EqvGen (EqvGen r) = EqvGen r := by
+  ext x y
+  refine ⟨fun h ↦ ?_, fun h ↦ EqvGen.rel _ _ h⟩
+  induction h with
+  | rel => assumption
+  | refl => exact EqvGen.refl _
+  | symm => apply EqvGen.symm; assumption
+  | trans => apply EqvGen.trans <;> assumption
+
 end EqvGen
 
 /-- The join of a relation on a single type is a new relation for which

From 4a9ea3e2f311f79310f4119bb7d8d59b70e34814 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 22 Apr 2026 15:21:33 -0600
Subject: [PATCH 26/40] mk_all

---
 Mathlib.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 73b992a1a5ce98..9d0de56d11b4d2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2716,6 +2716,7 @@ public import Mathlib.CategoryTheory.LiftingProperties.Limits
 public import Mathlib.CategoryTheory.LiftingProperties.Over
 public import Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
 public import Mathlib.CategoryTheory.Limits.Bicones
+public import Mathlib.CategoryTheory.Limits.Chosen.End
 public import Mathlib.CategoryTheory.Limits.ColimitLimit
 public import Mathlib.CategoryTheory.Limits.Comma
 public import Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
@@ -2900,6 +2901,7 @@ public import Mathlib.CategoryTheory.Limits.Types.ColimitType
 public import Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
 public import Mathlib.CategoryTheory.Limits.Types.Colimits
 public import Mathlib.CategoryTheory.Limits.Types.Coproducts
+public import Mathlib.CategoryTheory.Limits.Types.End
 public import Mathlib.CategoryTheory.Limits.Types.Equalizers
 public import Mathlib.CategoryTheory.Limits.Types.Filtered
 public import Mathlib.CategoryTheory.Limits.Types.Images
@@ -3182,6 +3184,7 @@ public import Mathlib.CategoryTheory.Products.Basic
 public import Mathlib.CategoryTheory.Products.Bifunctor
 public import Mathlib.CategoryTheory.Products.Unitor
 public import Mathlib.CategoryTheory.Profunctor.Basic
+public import Mathlib.CategoryTheory.Profunctor.Bicategory
 public import Mathlib.CategoryTheory.Profunctor.Comp
 public import Mathlib.CategoryTheory.Quotient
 public import Mathlib.CategoryTheory.Quotient.Linear

From c4c50bd50d8280e7e94f45ca01ba070919bdfa43 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Tue, 12 May 2026 09:12:11 -0600
Subject: [PATCH 27/40] Update End.lean

---
 Mathlib/CategoryTheory/Limits/Types/End.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/CategoryTheory/Limits/Types/End.lean b/Mathlib/CategoryTheory/Limits/Types/End.lean
index 1b818ece7bc803..5c57005fb2a0aa 100644
--- a/Mathlib/CategoryTheory/Limits/Types/End.lean
+++ b/Mathlib/CategoryTheory/Limits/Types/End.lean
@@ -12,6 +12,8 @@ public import Mathlib.CategoryTheory.Limits.Chosen.End
 
 This file constructs explicit coends in `Type` as quotients and provides a
 `ChosenCoends` instance using this construction.
+
+TODO: dualize for ends (done in #38383)
 -/
 
 @[expose] public section

From da677b334a9a60b2753f466c6562a4e58f9acb61 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Tue, 12 May 2026 10:27:54 -0600
Subject: [PATCH 28/40] fix the build

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 23 +++++++++++----------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 26c83683ddb8c1..f0e33e49fdf902 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -102,7 +102,6 @@ section Left
 variable (P : Profunctor.{max u w} C D) {Q R : Profunctor.{max u w} D E} (f : Q ⟶ R)
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] chosenCoend.map_apply in
 /-- Left whiskering of a natural transformation of profunctors. -/
 @[simps app_app]
 def whiskerLeft : P.comp Q ⟶ P.comp R where
@@ -114,8 +113,8 @@ def whiskerLeft : P.comp Q ⟶ P.comp R where
         dsimp
         apply Prod.ext <;>
         simp [← comp_apply, -types_comp_apply] } }
-    naturality _ _ _ := by ext ⟨_, _, _⟩; simp }
-  naturality _ _ _ := by ext _ ⟨_, _, _⟩; simp
+    naturality _ _ _ := by ext ⟨_, _, _⟩; simp [chosenCoend_def, chosenCoend.map_apply] }
+  naturality _ _ _ := by ext _ ⟨_, _, _⟩; simp [chosenCoend_def, chosenCoend.map_apply]
 
 variable (Q) in
 @[simp]
@@ -136,7 +135,7 @@ section Right
 variable {P Q : Profunctor.{max u w} C D} (R : Profunctor.{max u w} D E) (f : P ⟶ Q)
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] chosenCoend.map_apply in
+attribute [local simp] chosenCoend_def chosenCoend.map_apply in
 /-- Right whiskering of a natural transformation of profunctors. -/
 @[simps app_app]
 def whiskerRight : P.comp R ⟶ Q.comp R where
@@ -191,9 +190,10 @@ def leftUnitor (P : Profunctor.{u} C D) : Profunctor.id.comp P ≅ P :=
       rw [Types.coendRel_iff]
       exact ⟨f, ⟨𝟙 X, x⟩, by cat_disch⟩ })
     (fun f ↦ by dsimp; ext; simp [compDiagram, chosenCoend.ι_apply _]))
-    (fun f ↦ by ext _ ⟨_, _⟩; simp [chosenCoend.map_apply])
+    (fun f ↦ by ext _ ⟨_, _⟩; simp [Types.chosenCoend_def, chosenCoend.map_apply])
 
 set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
 @[simp]
 lemma id_whiskerLeft {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
     (Profunctor.id (C := C)).whiskerLeft f =
@@ -225,9 +225,10 @@ def rightUnitor (P : Profunctor.{u} C D) : P.comp .id ≅ P :=
       rw [Types.coendRel_iff]
       exact ⟨f, ⟨x, 𝟙 (unop Y)⟩, by cat_disch⟩ })
     (fun f ↦ by dsimp; ext; simp [compDiagram, chosenCoend.ι_apply _]))
-    (fun f ↦ by ext _ ⟨_, _⟩; simp [chosenCoend.map_apply])
+    (fun f ↦ by ext _ ⟨_, _⟩; simp [Types.chosenCoend_def, chosenCoend.map_apply])
 
 set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
 @[simp]
 lemma whiskerRight_id {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
     whiskerRight (Profunctor.id (C := D)) f =
@@ -250,7 +251,7 @@ variable {C D E F : Type u} [Category* C] [Category* D] [Category* E] [Category*
 open TypeCat Limits Types Functor
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] chosenCoend.map_apply in
+attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
 lemma associatorComponents_aux₁ {X : C} {Y : Fᵒᵖ} {e e' : E} {d d' : D}
     {p : (P.obj X).obj (Opposite.op d)} {q : (Q.obj d).obj (Opposite.op e)}
     {p' : (P.obj X).obj (Opposite.op d')} {q' : (Q.obj d').obj (Opposite.op e')}
@@ -275,7 +276,7 @@ lemma associatorComponents_aux₁ {X : C} {Y : Fᵒᵖ} {e e' : E} {d d' : D}
   exact ⟨𝟙 _, by simpa using (Quot.sound <| coendRel.mk (F := Q.compDiagram R _ _) f (_, _)).symm⟩
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] chosenCoend.map_apply in
+attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
 lemma associatorComponents_aux₂ {X : C} {Y : Fᵒᵖ} {d d' : D} {e e' : E}
   {q : (Q.obj d).obj (Opposite.op e)} {r : (R.obj e).obj Y}
   {q' : (Q.obj d').obj (Opposite.op e')}
@@ -299,7 +300,7 @@ lemma associatorComponents_aux₂ {X : C} {Y : Fᵒᵖ} {d d' : D} {e e' : E}
   exact ⟨𝟙 _, by simpa using Quot.sound <| coendRel.mk (F := P.compDiagram Q _ _) f (_, _)⟩
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] chosenCoend.map_apply in
+attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
 /-- The objectwise components of the associator isomorphism
 `(P.comp Q).comp R ≅ P.comp (Q.comp R)`. -/
 @[simps hom inv]
@@ -356,8 +357,8 @@ profunctors. -/
 @[simps! hom_app_app inv_app_app]
 def associator : (P.comp Q).comp R ≅ P.comp (Q.comp R) :=
   NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ associatorComponents P Q R X Y)
-    fun _ ↦ by ext ⟨_, ⟨_, _, _⟩, _⟩; simp [chosenCoend.map_apply, Quot.map])
-    fun _ ↦ by ext _ ⟨_, ⟨_, _, _⟩, _⟩; simp [chosenCoend.map_apply, Quot.map]
+    fun _ ↦ by ext ⟨_, ⟨_, _, _⟩, _⟩; simp [chosenCoend_def, chosenCoend.map_apply, Quot.map])
+    fun _ ↦ by ext _ ⟨_, ⟨_, _, _⟩, _⟩; simp [chosenCoend_def, chosenCoend.map_apply, Quot.map]
 
 @[simp]
 lemma comp_whiskerLeft {S : Profunctor.{max u w} E F} (f : R ⟶ S) :

From 3162a43ddbfab4777b0cbfa08def4a21fd7c8dd4 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Tue, 12 May 2026 10:44:17 -0600
Subject: [PATCH 29/40] fix the build

---
 Mathlib/CategoryTheory/Profunctor/Bicategory.lean | 1 +
 Mathlib/CategoryTheory/Profunctor/Comp.lean       | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Bicategory.lean b/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
index 9fe0b105bc1ef0..40eb261c179791 100644
--- a/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
@@ -52,6 +52,7 @@ lemma pentagon {C D E F G : Type u} [Category* C] [Category* D] [Category* E]
   rfl
 
 set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] Types.chosenCoend_def in
 @[reassoc (attr := simp)]
 lemma triangle {C D E : Type u} [Category* C] [Category.{u} D] [Category* E]
     (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) :
diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index f0e33e49fdf902..09f4b4bc7d0297 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -193,7 +193,7 @@ def leftUnitor (P : Profunctor.{u} C D) : Profunctor.id.comp P ≅ P :=
     (fun f ↦ by ext _ ⟨_, _⟩; simp [Types.chosenCoend_def, chosenCoend.map_apply])
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
+attribute [local simp] Types.chosenCoend_def in
 @[simp]
 lemma id_whiskerLeft {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
     (Profunctor.id (C := C)).whiskerLeft f =
@@ -228,7 +228,7 @@ def rightUnitor (P : Profunctor.{u} C D) : P.comp .id ≅ P :=
     (fun f ↦ by ext _ ⟨_, _⟩; simp [Types.chosenCoend_def, chosenCoend.map_apply])
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
+attribute [local simp] Types.chosenCoend_def in
 @[simp]
 lemma whiskerRight_id {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
     whiskerRight (Profunctor.id (C := D)) f =

From 33e3bbfe2c5e999c14bf3f05443c97f18ea17747 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 20 May 2026 09:21:03 -0600
Subject: [PATCH 30/40] Apply suggestions from code review

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
---
 Mathlib/CategoryTheory/Profunctor/Bicategory.lean | 4 ++--
 Mathlib/CategoryTheory/Profunctor/Comp.lean       | 1 -
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Bicategory.lean b/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
index 40eb261c179791..74f03ff474d8fd 100644
--- a/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.CategoryTheory.Profunctor.Comp
 
 /-!
-
 # The Profunctor Bicategory
 
 This file defines the bicategory `ProfCat` whose objects are categories and whose 1-morphisms are
@@ -30,6 +29,8 @@ structure ProfCat where
   /-- ... bundled with a category instance. -/
   [str : Category.{v} obj]
 
+initialize_simps_projections ProfCat (-str)
+
 instance : CoeSort ProfCat (Type u) :=
   ⟨ProfCat.obj⟩
 
@@ -69,7 +70,6 @@ end
 
 end Profunctor
 
-set_option backward.isDefEq.respectTransparency false in
 instance : Bicategory ProfCat.{u, u} where
   Hom X Y := Profunctor.{u} X Y
   id X := .id
diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 09f4b4bc7d0297..42640e4c2d87d3 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -9,7 +9,6 @@ public import Mathlib.CategoryTheory.Limits.Types.End
 public import Mathlib.CategoryTheory.Profunctor.Basic
 
 /-!
-
 # Composition of Profunctors
 
 This file defines composition of profunctors. Given profunctors `P : C ⥤ Dᵒᵖ ⥤ Type` and

From d650f126e3ac52dd7b88f38f0c5d04329fbed2cd Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 20 May 2026 09:39:10 -0600
Subject: [PATCH 31/40] chore: remove profunctor bicategory from PR

---
 Mathlib.lean                                  |  1 -
 .../CategoryTheory/Profunctor/Bicategory.lean | 83 -------------------
 2 files changed, 84 deletions(-)
 delete mode 100644 Mathlib/CategoryTheory/Profunctor/Bicategory.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index cd8d2f8a620656..ec991cca60f3a8 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3243,7 +3243,6 @@ public import Mathlib.CategoryTheory.Products.Basic
 public import Mathlib.CategoryTheory.Products.Bifunctor
 public import Mathlib.CategoryTheory.Products.Unitor
 public import Mathlib.CategoryTheory.Profunctor.Basic
-public import Mathlib.CategoryTheory.Profunctor.Bicategory
 public import Mathlib.CategoryTheory.Profunctor.Comp
 public import Mathlib.CategoryTheory.Quotient
 public import Mathlib.CategoryTheory.Quotient.Linear
diff --git a/Mathlib/CategoryTheory/Profunctor/Bicategory.lean b/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
deleted file mode 100644
index 74f03ff474d8fd..00000000000000
--- a/Mathlib/CategoryTheory/Profunctor/Bicategory.lean
+++ /dev/null
@@ -1,83 +0,0 @@
-/-
-Copyright (c) 2026 Dagur Asgeirsson. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Dagur Asgeirsson
--/
-module
-
-public import Mathlib.CategoryTheory.Profunctor.Comp
-
-/-!
-# The Profunctor Bicategory
-
-This file defines the bicategory `ProfCat` whose objects are categories and whose 1-morphisms are
-profunctors.
--/
-
-@[expose] public section
-
-universe w v u
-
-namespace CategoryTheory
-
-/-- The bicategory of categories where the 1-morphisms are profunctors. -/
-@[nolint checkUnivs]
-structure ProfCat where
-  of ::
-  /-- The objects of the bicategory are types... -/
-  obj : Type u
-  /-- ... bundled with a category instance. -/
-  [str : Category.{v} obj]
-
-initialize_simps_projections ProfCat (-str)
-
-instance : CoeSort ProfCat (Type u) :=
-  ⟨ProfCat.obj⟩
-
-attribute [instance] ProfCat.str
-
-open Limits Types Profunctor
-
-namespace Profunctor
-
-section
-
-@[reassoc (attr := simp)]
-lemma pentagon {C D E F G : Type u} [Category* C] [Category* D] [Category* E]
-  [Category* F] [Category* G] (P : Profunctor.{max u w} C D) (Q : Profunctor.{max u w} D E)
-    (R : Profunctor.{max u w} E F) (S : Profunctor.{max u w} F G) :
-    whiskerRight S (P.associator Q R).hom ≫
-        (P.associator (Q.comp R) S).hom ≫ P.whiskerLeft (Q.associator R S).hom =
-      ((P.comp Q).associator R S).hom ≫ (P.associator Q (R.comp S)).hom := by
-  ext _ _ ⟨_, ⟨_, ⟨_, _, _⟩, _⟩, _⟩
-  rfl
-
-set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] Types.chosenCoend_def in
-@[reassoc (attr := simp)]
-lemma triangle {C D E : Type u} [Category* C] [Category.{u} D] [Category* E]
-    (P : Profunctor.{u} C D) (Q : Profunctor.{u} D E) :
-    (P.associator (Profunctor.id (C := D)) Q).hom ≫ P.whiskerLeft (Q.leftUnitor.hom) =
-      whiskerRight Q (P.rightUnitor.hom) := by
-  ext _ _ ⟨_, ⟨_, _, g⟩, _⟩
-  dsimp [chosenCoend.map_apply, Quot.map]
-  symm
-  apply Quot.sound
-  rw [coendRel_iff]
-  exact ⟨g, by simp⟩
-
-end
-
-end Profunctor
-
-instance : Bicategory ProfCat.{u, u} where
-  Hom X Y := Profunctor.{u} X Y
-  id X := .id
-  comp P Q := P.comp Q
-  whiskerLeft P _ _ f := P.whiskerLeft f
-  whiskerRight f R := whiskerRight R f
-  associator P Q R := P.associator Q R
-  leftUnitor P := P.leftUnitor
-  rightUnitor P := P.rightUnitor
-
-end CategoryTheory

From d3ae39be63b4c295de091019a04344ded566ac6f Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 20 May 2026 09:41:15 -0600
Subject: [PATCH 32/40] chore: remove stale comment

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 42640e4c2d87d3..de8c78e23a4a2b 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -331,7 +331,7 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
       rw [coendRel_iff]
       use f
       simp
-    · rintro ⟨d, p, e, q, r⟩ ⟨d', p', e', q', r'⟩ h-- ⟨e', ⟨d', p', q'⟩, r'⟩ h
+    · rintro ⟨d, p, e, q, r⟩ ⟨d', p', e', q', r'⟩ h
       dsimp
       rw [coendRel_iff] at h
       obtain ⟨f, ⟨p, x⟩, h₁, h₂⟩ := h

From 56ace8ff0be228a360d063b34324b95d42294d5b Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 27 May 2026 23:50:15 -0600
Subject: [PATCH 33/40] Apply suggestions from code review

Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 115 ++++++--------------
 1 file changed, 34 insertions(+), 81 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index de8c78e23a4a2b..2e9d0f4abbd5e7 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -197,11 +197,9 @@ attribute [local simp] Types.chosenCoend_def in
 lemma id_whiskerLeft {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
     (Profunctor.id (C := C)).whiskerLeft f =
       (P.leftUnitor).hom ≫ f ≫ (Q.leftUnitor).inv := by
+  rw [← cancel_mono (Q.leftUnitor).hom]
   ext _ _ ⟨_, g, _⟩
-  dsimp [chosenCoend.map_apply, Quot.map]
-  apply Quot.sound
-  rw [Types.coendRel_iff]
-  exact ⟨g, by simp [← comp_apply, -types_comp_apply]⟩
+  simp [-types_comp_apply]
 
 end LeftUnitor
 
@@ -232,12 +230,9 @@ attribute [local simp] Types.chosenCoend_def in
 lemma whiskerRight_id {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
     whiskerRight (Profunctor.id (C := D)) f =
       (P.rightUnitor).hom ≫ f ≫ (Q.rightUnitor).inv := by
+  rw [← cancel_mono (Q.rightUnitor).hom]
   ext _ _ ⟨_, _, g⟩
-  dsimp [chosenCoend.map_apply, Quot.map]
-  symm
-  apply Quot.sound
-  rw [Types.coendRel_iff]
-  exact ⟨g, by simp⟩
+  simp [chosenCoend.map_apply, -types_comp_apply]
 
 
 end RightUnitor
@@ -249,55 +244,6 @@ variable {C D E F : Type u} [Category* C] [Category* D] [Category* E] [Category*
 
 open TypeCat Limits Types Functor
 
-set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
-lemma associatorComponents_aux₁ {X : C} {Y : Fᵒᵖ} {e e' : E} {d d' : D}
-    {p : (P.obj X).obj (Opposite.op d)} {q : (Q.obj d).obj (Opposite.op e)}
-    {p' : (P.obj X).obj (Opposite.op d')} {q' : (Q.obj d').obj (Opposite.op e')}
-    {f : e ⟶ e'} {r : (R.obj e).obj Y}
-    (h : Relation.EqvGen (coendRel (P.compDiagram Q X e))
-      ⟨d', p', (Q.obj d').map f.op q'⟩ ⟨d, p, q⟩) :
-    Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))
-      ⟨d', p', Quot.mk _ ⟨e', (q', (R.map f).app Y r)⟩⟩
-      ⟨d, p, Quot.mk _ ⟨e, (q, r)⟩⟩ := by
-  replace h := Relation.EqvGen.map (fun ⟨d, p, q⟩ ↦ ⟨d, (p, Quot.mk _ ⟨e, q, r⟩)⟩)
-      (Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))) _ _ (h.mono <| by
-    intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
-    apply Relation.EqvGen.rel
-    rw [coendRel_iff] at h ⊢
-    obtain ⟨f, x, h₁, h₂⟩ := h
-    use f
-    simp_all [Prod.ext_iff])
-  simp only [Relation.EqvGen.idempotent] at h
-  refine Relation.EqvGen.trans _ _ _ ?_ h
-  apply Relation.EqvGen.rel
-  rw [coendRel_iff]
-  exact ⟨𝟙 _, by simpa using (Quot.sound <| coendRel.mk (F := Q.compDiagram R _ _) f (_, _)).symm⟩
-
-set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
-lemma associatorComponents_aux₂ {X : C} {Y : Fᵒᵖ} {d d' : D} {e e' : E}
-  {q : (Q.obj d).obj (Opposite.op e)} {r : (R.obj e).obj Y}
-  {q' : (Q.obj d').obj (Opposite.op e')}
-  {r' : (R.obj e').obj Y} {f : d ⟶ d'} {p : (P.obj X).obj (Opposite.op d')}
-  (h : Relation.EqvGen (coendRel (Q.compDiagram R d' (unop Y)))
-    ⟨e, ((ConcreteCategory.hom ((Q.map f).app (Opposite.op e))) q, r)⟩ ⟨e', (q', r')⟩) :
-  Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))
-    ⟨e, (Quot.mk (coendRel (P.compDiagram Q X e)) ⟨d, (P.obj X).map f.op p, q⟩, r)⟩
-    ⟨e', (Quot.mk (coendRel (P.compDiagram Q X e')) ⟨d', (p, q')⟩, r')⟩ := by
-  replace h := Relation.EqvGen.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d', p, q⟩, r⟩)
-      (Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))) _ _ (h.mono <| by
-    intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
-    apply Relation.EqvGen.rel
-    rw [coendRel_iff] at h ⊢
-    obtain ⟨f, x, h₁, h₂⟩ := h
-    exact ⟨f, by simp_all [Prod.ext_iff]⟩)
-  simp only [Relation.EqvGen.idempotent] at h
-  refine (Relation.EqvGen.trans _ _ _ ?_ h)
-  apply Relation.EqvGen.rel
-  rw [coendRel_iff]
-  exact ⟨𝟙 _, by simpa using Quot.sound <| coendRel.mk (F := P.compDiagram Q _ _) f (_, _)⟩
-
 set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
 /-- The objectwise components of the associator isomorphism
@@ -311,19 +257,22 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
     · rintro ⟨d, p, q⟩ ⟨d', p', q'⟩ ⟨f, x⟩
       rw [coendRel_iff]
       exact ⟨f, by simp⟩
-    · rintro ⟨e, ⟨d, p, q⟩, r⟩ ⟨e', ⟨d', p', q'⟩, r'⟩ h
-      dsimp
-      rw [coendRel_iff] at h
-      obtain ⟨f, ⟨x, r''⟩, h₁, h₂⟩ := h
-      dsimp at h₁ h₂
-      simp only [map_id, NatTrans.id_app, Prod.mk.injEq] at h₁
-      obtain ⟨rfl, rfl⟩ := h₂
-      obtain ⟨h₁, rfl⟩ := h₁
-      dsimp at h₁
-      symm
+    · rintro ⟨e, _, _⟩ ⟨e', _, _⟩ ⟨f, ⟨x, r⟩⟩
+      refine Quot.inductionOn x ?_
+      rintro ⟨d, p, q⟩
       dsimp [Quot.map]
-      rw [Quot.eq] at h₁ ⊢
-      exact associatorComponents_aux₁ _ _ _ h₁
+      simp only [map_id, NatTrans.id_app, types_id_apply]
+      -- First use the inner coend condition, then apply the outer quotient constructor.
+      let outer (x : ((Q.comp R).obj d).obj Y) :=
+        chosenCoend.ι (P.compDiagram (Q.comp R) X (unop Y)) d (p, x)
+      have inner_relation :
+          chosenCoend.ι (Q.compDiagram R d (unop Y)) e (((Q.obj d).map f.op q), r) =
+            chosenCoend.ι (Q.compDiagram R d (unop Y)) e' (q, (R.map f).app Y r) := by
+        simpa [types_comp_apply, Prod.map] using
+          types_congr_hom
+            (chosenCoend.condition (F := Q.compDiagram R d (unop Y)) (i := e) (j := e') f)
+            (q, r)
+      exact congrArg outer inner_relation
   inv := by
     refine ↾Quot.lift (fun ⟨d, p, x⟩ ↦
         Quot.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d, p, q⟩, r⟩) ?_ x) ?_
@@ -331,18 +280,22 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
       rw [coendRel_iff]
       use f
       simp
-    · rintro ⟨d, p, e, q, r⟩ ⟨d', p', e', q', r'⟩ h
-      dsimp
-      rw [coendRel_iff] at h
-      obtain ⟨f, ⟨p, x⟩, h₁, h₂⟩ := h
-      dsimp at h₁ h₂
-      simp only [map_id, Prod.mk.injEq] at h₂
-      obtain ⟨rfl, rfl⟩ := h₁
-      obtain ⟨rfl, h₂⟩ := h₂
-      dsimp at h₂
+    · rintro ⟨d, _, _⟩ ⟨d', _, _⟩ ⟨f, ⟨p, x⟩⟩
+      refine Quot.inductionOn x ?_
+      rintro ⟨e, q, r⟩
       dsimp [Quot.map]
-      rw [Quot.eq] at h₂ ⊢
-      exact associatorComponents_aux₂ _ _ _ h₂
+      simp only [map_id, types_id_apply]
+      -- First use the inner coend condition, then apply the outer quotient constructor.
+      let outer (x : ((P.comp Q).obj X).obj (op e)) :=
+        chosenCoend.ι ((P.comp Q).compDiagram R X (unop Y)) e (x, r)
+      have inner_relation :
+          chosenCoend.ι (P.compDiagram Q X e) d (((P.obj X).map f.op p), q) =
+            chosenCoend.ι (P.compDiagram Q X e) d' (p, (Q.map f).app _ q) := by
+        simpa [types_comp_apply, Prod.map] using
+          types_congr_hom
+            (chosenCoend.condition (F := P.compDiagram Q X e) (i := d) (j := d') f)
+            (p, q)
+      exact congrArg outer inner_relation
   hom_inv_id := by
     ext ⟨_, ⟨_, _, _⟩, _⟩
     dsimp [Quot.map]

From 93c306a8aa4f6e4c0bb7ea9ec24c003e2c3ae4af Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 27 May 2026 23:53:09 -0600
Subject: [PATCH 34/40] fix error

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 2e9d0f4abbd5e7..05a60852408eb2 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -197,9 +197,9 @@ attribute [local simp] Types.chosenCoend_def in
 lemma id_whiskerLeft {P Q : Profunctor.{u} C D} (f : P ⟶ Q) :
     (Profunctor.id (C := C)).whiskerLeft f =
       (P.leftUnitor).hom ≫ f ≫ (Q.leftUnitor).inv := by
-  rw [← cancel_mono (Q.leftUnitor).hom]
-  ext _ _ ⟨_, g, _⟩
-  simp [-types_comp_apply]
+  rw [← cancel_epi (P.leftUnitor).inv]
+  ext
+  simp [chosenCoend.map_apply]
 
 end LeftUnitor
 

From 14f4302ff9f4958d08babc47c9fc2b3dc9a82f6a Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Wed, 27 May 2026 23:55:20 -0600
Subject: [PATCH 35/40] Type* -> Sort*

---
 Mathlib/Logic/Relation.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index d58ca90bc7543b..ecf7771366f2e0 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -799,7 +799,7 @@ theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : Eq
   | symm a b _ ih => exact EqvGen.symm _ _ ih
   | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
 
-lemma map {α β : Type*} (f : α → β) (r : β → β → Prop) (x y : α)
+lemma map (f : α → β) (r : β → β → Prop) (x y : α)
     (h : EqvGen (fun x y ↦ r (f x) (f y)) x y) : EqvGen r (f x) (f y) := by
   induction h with
   | rel => apply EqvGen.rel; assumption
@@ -808,7 +808,7 @@ lemma map {α β : Type*} (f : α → β) (r : β → β → Prop) (x y : α)
   | trans => apply EqvGen.trans <;> assumption
 
 @[simp]
-lemma idempotent {α : Type*} (r : α → α → Prop) : EqvGen (EqvGen r) = EqvGen r := by
+lemma idempotent (r : α → α → Prop) : EqvGen (EqvGen r) = EqvGen r := by
   ext x y
   refine ⟨fun h ↦ ?_, fun h ↦ EqvGen.rel _ _ h⟩
   induction h with

From eea168ee94ba57e1e30b974f25ec19335f68a5a2 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Thu, 11 Jun 2026 15:37:48 +0200
Subject: [PATCH 36/40] Update profunctor future work

---
 Mathlib/CategoryTheory/Profunctor/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Basic.lean b/Mathlib/CategoryTheory/Profunctor/Basic.lean
index 63bcf8d1c58d4a..38011913147452 100644
--- a/Mathlib/CategoryTheory/Profunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Basic.lean
@@ -22,8 +22,7 @@ of a profunctor with functors, and the profunctors in both directions correspond
 
 ## Future work
 
-- Define composition of profunctors.
-- Define the bicategory of categories where the 1-morphisms are profunctors.
+- Use profunctor composition to define the bicategory of categories and profunctors.
 -/
 
 @[expose] public section

From 89b75ae7d71d7cd4d8680c20d1658629c2a76d74 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Fri, 12 Jun 2026 16:17:17 +0200
Subject: [PATCH 37/40] temporary fix

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 113 ++++++++++++++------
 1 file changed, 83 insertions(+), 30 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 05a60852408eb2..bcb7187bcc2c32 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -55,6 +55,7 @@ def compDiagram (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E) (X : C) (Y :
     map f := TypeCat.ofHom (Prod.map id ((Q.map f).app _)) }
   map g := { app U := TypeCat.ofHom (Prod.map ((P.obj _).map g) id) }
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The map on composition diagrams induced by morphisms in the outer variables. -/
 @[simps]
 def compDiagramMap (P : Profunctor.{w} C D) (Q : Profunctor.{w'} D E)
@@ -100,6 +101,7 @@ section Left
 
 variable (P : Profunctor.{max u w} C D) {Q R : Profunctor.{max u w} D E} (f : Q ⟶ R)
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- Left whiskering of a natural transformation of profunctors. -/
 @[simps app_app]
@@ -133,6 +135,7 @@ section Right
 
 variable {P Q : Profunctor.{max u w} C D} (R : Profunctor.{max u w} D E) (f : P ⟶ Q)
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] chosenCoend_def chosenCoend.map_apply in
 /-- Right whiskering of a natural transformation of profunctors. -/
@@ -175,6 +178,7 @@ variable {C : Type u} [Category.{u} C] {D : Type u} [Category* D]
 
 open Limits TypeCat
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The left unitor isomorphism `Profunctor.id.comp P ≅ P` for composition of profunctors. -/
 @[simps! hom_app_app inv_app_app]
@@ -191,6 +195,7 @@ def leftUnitor (P : Profunctor.{u} C D) : Profunctor.id.comp P ≅ P :=
     (fun f ↦ by dsimp; ext; simp [compDiagram, chosenCoend.ι_apply _]))
     (fun f ↦ by ext _ ⟨_, _⟩; simp [Types.chosenCoend_def, chosenCoend.map_apply])
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Types.chosenCoend_def in
 @[simp]
@@ -209,6 +214,7 @@ open Limits TypeCat
 
 variable {C : Type u} [Category* C] {D : Type u} [Category.{u} D]
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The right unitor isomorphism `P.comp Profunctor.id ≅ P` for composition of profunctors. -/
 @[simps! hom_app_app inv_app_app]
@@ -224,6 +230,7 @@ def rightUnitor (P : Profunctor.{u} C D) : P.comp .id ≅ P :=
     (fun f ↦ by dsimp; ext; simp [compDiagram, chosenCoend.ι_apply _]))
     (fun f ↦ by ext _ ⟨_, _⟩; simp [Types.chosenCoend_def, chosenCoend.map_apply])
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Types.chosenCoend_def in
 @[simp]
@@ -244,6 +251,58 @@ variable {C D E F : Type u} [Category* C] [Category* D] [Category* E] [Category*
 
 open TypeCat Limits Types Functor
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
+lemma associatorComponents_aux₁ {X : C} {Y : Fᵒᵖ} {e e' : E} {d d' : D}
+    {p : (P.obj X).obj (Opposite.op d)} {q : (Q.obj d).obj (Opposite.op e)}
+    {p' : (P.obj X).obj (Opposite.op d')} {q' : (Q.obj d').obj (Opposite.op e')}
+    {f : e ⟶ e'} {r : (R.obj e).obj Y}
+    (h : Relation.EqvGen (coendRel (P.compDiagram Q X e))
+      ⟨d', p', (Q.obj d').map f.op q'⟩ ⟨d, p, q⟩) :
+    Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))
+      ⟨d', p', Quot.mk _ ⟨e', (q', (R.map f).app Y r)⟩⟩
+      ⟨d, p, Quot.mk _ ⟨e, (q, r)⟩⟩ := by
+  replace h := Relation.EqvGen.map (fun ⟨d, p, q⟩ ↦ ⟨d, (p, Quot.mk _ ⟨e, q, r⟩)⟩)
+      (Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))) _ _ (h.mono <| by
+    intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
+    apply Relation.EqvGen.rel
+    rw [coendRel_iff] at h ⊢
+    obtain ⟨f, x, h₁, h₂⟩ := h
+    use f
+    simp_all [Prod.ext_iff])
+  simp only [Relation.EqvGen.idempotent] at h
+  refine Relation.EqvGen.trans _ _ _ ?_ h
+  apply Relation.EqvGen.rel
+  rw [coendRel_iff]
+  exact ⟨𝟙 _, by simp; exact (Quot.sound <| coendRel.mk (F := Q.compDiagram R _ _) f (_, _)).symm⟩
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
+lemma associatorComponents_aux₂ {X : C} {Y : Fᵒᵖ} {d d' : D} {e e' : E}
+  {q : (Q.obj d).obj (Opposite.op e)} {r : (R.obj e).obj Y}
+  {q' : (Q.obj d').obj (Opposite.op e')}
+  {r' : (R.obj e').obj Y} {f : d ⟶ d'} {p : (P.obj X).obj (Opposite.op d')}
+  (h : Relation.EqvGen (coendRel (Q.compDiagram R d' (unop Y)))
+    ⟨e, ((ConcreteCategory.hom ((Q.map f).app (Opposite.op e))) q, r)⟩ ⟨e', (q', r')⟩) :
+  Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))
+    ⟨e, (Quot.mk (coendRel (P.compDiagram Q X e)) ⟨d, (P.obj X).map f.op p, q⟩, r)⟩
+    ⟨e', (Quot.mk (coendRel (P.compDiagram Q X e')) ⟨d', (p, q')⟩, r')⟩ := by
+  replace h := Relation.EqvGen.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d', p, q⟩, r⟩)
+      (Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))) _ _ (h.mono <| by
+    intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
+    apply Relation.EqvGen.rel
+    rw [coendRel_iff] at h ⊢
+    obtain ⟨f, x, h₁, h₂⟩ := h
+    exact ⟨f, by simp_all [Prod.ext_iff]⟩)
+  simp only [Relation.EqvGen.idempotent] at h
+  refine (Relation.EqvGen.trans _ _ _ ?_ h)
+  apply Relation.EqvGen.rel
+  rw [coendRel_iff]
+  exact ⟨𝟙 _, by simp; exact Quot.sound <| coendRel.mk (F := P.compDiagram Q _ _) f (_, _)⟩
+
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
 /-- The objectwise components of the associator isomorphism
@@ -257,22 +316,19 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
     · rintro ⟨d, p, q⟩ ⟨d', p', q'⟩ ⟨f, x⟩
       rw [coendRel_iff]
       exact ⟨f, by simp⟩
-    · rintro ⟨e, _, _⟩ ⟨e', _, _⟩ ⟨f, ⟨x, r⟩⟩
-      refine Quot.inductionOn x ?_
-      rintro ⟨d, p, q⟩
+    · rintro ⟨e, ⟨d, p, q⟩, r⟩ ⟨e', ⟨d', p', q'⟩, r'⟩ h
+      dsimp
+      rw [coendRel_iff] at h
+      obtain ⟨f, ⟨x, r''⟩, h₁, h₂⟩ := h
+      dsimp at h₁ h₂
+      simp only [map_id, NatTrans.id_app, Prod.mk.injEq] at h₁
+      obtain ⟨rfl, rfl⟩ := h₂
+      obtain ⟨h₁, rfl⟩ := h₁
+      dsimp at h₁
+      symm
       dsimp [Quot.map]
-      simp only [map_id, NatTrans.id_app, types_id_apply]
-      -- First use the inner coend condition, then apply the outer quotient constructor.
-      let outer (x : ((Q.comp R).obj d).obj Y) :=
-        chosenCoend.ι (P.compDiagram (Q.comp R) X (unop Y)) d (p, x)
-      have inner_relation :
-          chosenCoend.ι (Q.compDiagram R d (unop Y)) e (((Q.obj d).map f.op q), r) =
-            chosenCoend.ι (Q.compDiagram R d (unop Y)) e' (q, (R.map f).app Y r) := by
-        simpa [types_comp_apply, Prod.map] using
-          types_congr_hom
-            (chosenCoend.condition (F := Q.compDiagram R d (unop Y)) (i := e) (j := e') f)
-            (q, r)
-      exact congrArg outer inner_relation
+      rw [Quot.eq] at h₁ ⊢
+      exact associatorComponents_aux₁ _ _ _ h₁
   inv := by
     refine ↾Quot.lift (fun ⟨d, p, x⟩ ↦
         Quot.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d, p, q⟩, r⟩) ?_ x) ?_
@@ -280,22 +336,18 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
       rw [coendRel_iff]
       use f
       simp
-    · rintro ⟨d, _, _⟩ ⟨d', _, _⟩ ⟨f, ⟨p, x⟩⟩
-      refine Quot.inductionOn x ?_
-      rintro ⟨e, q, r⟩
+    · rintro ⟨d, p, e, q, r⟩ ⟨d', p', e', q', r'⟩ h
+      dsimp
+      rw [coendRel_iff] at h
+      obtain ⟨f, ⟨p, x⟩, h₁, h₂⟩ := h
+      dsimp at h₁ h₂
+      simp only [map_id, Prod.mk.injEq] at h₂
+      obtain ⟨rfl, rfl⟩ := h₁
+      obtain ⟨rfl, h₂⟩ := h₂
+      dsimp at h₂
       dsimp [Quot.map]
-      simp only [map_id, types_id_apply]
-      -- First use the inner coend condition, then apply the outer quotient constructor.
-      let outer (x : ((P.comp Q).obj X).obj (op e)) :=
-        chosenCoend.ι ((P.comp Q).compDiagram R X (unop Y)) e (x, r)
-      have inner_relation :
-          chosenCoend.ι (P.compDiagram Q X e) d (((P.obj X).map f.op p), q) =
-            chosenCoend.ι (P.compDiagram Q X e) d' (p, (Q.map f).app _ q) := by
-        simpa [types_comp_apply, Prod.map] using
-          types_congr_hom
-            (chosenCoend.condition (F := P.compDiagram Q X e) (i := d) (j := d') f)
-            (p, q)
-      exact congrArg outer inner_relation
+      rw [Quot.eq] at h₂ ⊢
+      exact associatorComponents_aux₂ _ _ _ h₂
   hom_inv_id := by
     ext ⟨_, ⟨_, _, _⟩, _⟩
     dsimp [Quot.map]
@@ -303,6 +355,7 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
     ext ⟨_, _, ⟨_, _, _⟩⟩
     dsimp [Quot.map]
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The associator isomorphism `(P.comp Q).comp R ≅ P.comp (Q.comp R)` for composition of
 profunctors. -/

From 22fa517e8f3789b4faddb960a61d6e4c9d20d094 Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Fri, 12 Jun 2026 16:19:48 +0200
Subject: [PATCH 38/40] better fix

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 92 ++++-----------------
 1 file changed, 18 insertions(+), 74 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index bcb7187bcc2c32..86a386d8b0706b 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -251,57 +251,6 @@ variable {C D E F : Type u} [Category* C] [Category* D] [Category* E] [Category*
 
 open TypeCat Limits Types Functor
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
-lemma associatorComponents_aux₁ {X : C} {Y : Fᵒᵖ} {e e' : E} {d d' : D}
-    {p : (P.obj X).obj (Opposite.op d)} {q : (Q.obj d).obj (Opposite.op e)}
-    {p' : (P.obj X).obj (Opposite.op d')} {q' : (Q.obj d').obj (Opposite.op e')}
-    {f : e ⟶ e'} {r : (R.obj e).obj Y}
-    (h : Relation.EqvGen (coendRel (P.compDiagram Q X e))
-      ⟨d', p', (Q.obj d').map f.op q'⟩ ⟨d, p, q⟩) :
-    Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))
-      ⟨d', p', Quot.mk _ ⟨e', (q', (R.map f).app Y r)⟩⟩
-      ⟨d, p, Quot.mk _ ⟨e, (q, r)⟩⟩ := by
-  replace h := Relation.EqvGen.map (fun ⟨d, p, q⟩ ↦ ⟨d, (p, Quot.mk _ ⟨e, q, r⟩)⟩)
-      (Relation.EqvGen (coendRel (P.compDiagram (Q.comp R) X (unop Y)))) _ _ (h.mono <| by
-    intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
-    apply Relation.EqvGen.rel
-    rw [coendRel_iff] at h ⊢
-    obtain ⟨f, x, h₁, h₂⟩ := h
-    use f
-    simp_all [Prod.ext_iff])
-  simp only [Relation.EqvGen.idempotent] at h
-  refine Relation.EqvGen.trans _ _ _ ?_ h
-  apply Relation.EqvGen.rel
-  rw [coendRel_iff]
-  exact ⟨𝟙 _, by simp; exact (Quot.sound <| coendRel.mk (F := Q.compDiagram R _ _) f (_, _)).symm⟩
-
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
-lemma associatorComponents_aux₂ {X : C} {Y : Fᵒᵖ} {d d' : D} {e e' : E}
-  {q : (Q.obj d).obj (Opposite.op e)} {r : (R.obj e).obj Y}
-  {q' : (Q.obj d').obj (Opposite.op e')}
-  {r' : (R.obj e').obj Y} {f : d ⟶ d'} {p : (P.obj X).obj (Opposite.op d')}
-  (h : Relation.EqvGen (coendRel (Q.compDiagram R d' (unop Y)))
-    ⟨e, ((ConcreteCategory.hom ((Q.map f).app (Opposite.op e))) q, r)⟩ ⟨e', (q', r')⟩) :
-  Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))
-    ⟨e, (Quot.mk (coendRel (P.compDiagram Q X e)) ⟨d, (P.obj X).map f.op p, q⟩, r)⟩
-    ⟨e', (Quot.mk (coendRel (P.compDiagram Q X e')) ⟨d', (p, q')⟩, r')⟩ := by
-  replace h := Relation.EqvGen.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d', p, q⟩, r⟩)
-      (Relation.EqvGen (coendRel ((P.comp Q).compDiagram R X (unop Y)))) _ _ (h.mono <| by
-    intro ⟨d, p, q⟩ ⟨d', p', q'⟩ h
-    apply Relation.EqvGen.rel
-    rw [coendRel_iff] at h ⊢
-    obtain ⟨f, x, h₁, h₂⟩ := h
-    exact ⟨f, by simp_all [Prod.ext_iff]⟩)
-  simp only [Relation.EqvGen.idempotent] at h
-  refine (Relation.EqvGen.trans _ _ _ ?_ h)
-  apply Relation.EqvGen.rel
-  rw [coendRel_iff]
-  exact ⟨𝟙 _, by simp; exact Quot.sound <| coendRel.mk (F := P.compDiagram Q _ _) f (_, _)⟩
-
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
@@ -316,19 +265,16 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
     · rintro ⟨d, p, q⟩ ⟨d', p', q'⟩ ⟨f, x⟩
       rw [coendRel_iff]
       exact ⟨f, by simp⟩
-    · rintro ⟨e, ⟨d, p, q⟩, r⟩ ⟨e', ⟨d', p', q'⟩, r'⟩ h
-      dsimp
-      rw [coendRel_iff] at h
-      obtain ⟨f, ⟨x, r''⟩, h₁, h₂⟩ := h
-      dsimp at h₁ h₂
-      simp only [map_id, NatTrans.id_app, Prod.mk.injEq] at h₁
-      obtain ⟨rfl, rfl⟩ := h₂
-      obtain ⟨h₁, rfl⟩ := h₁
-      dsimp at h₁
-      symm
+    · rintro ⟨e, _, _⟩ ⟨e', _, _⟩ ⟨f, ⟨x, r⟩⟩
+      refine Quot.inductionOn x ?_
+      rintro ⟨d, p, q⟩
       dsimp [Quot.map]
-      rw [Quot.eq] at h₁ ⊢
-      exact associatorComponents_aux₁ _ _ _ h₁
+      simp only [map_id, NatTrans.id_app, types_id_apply]
+      -- First use the inner coend condition, then apply the outer quotient constructor.
+      let outer (x : ((Q.comp R).obj d).obj Y) :=
+        chosenCoend.ι (P.compDiagram (Q.comp R) X (unop Y)) d (p, x)
+      exact congrArg outer
+        (types_congr_hom (chosenCoend.condition (F := Q.compDiagram R d (unop Y)) f) (q, r))
   inv := by
     refine ↾Quot.lift (fun ⟨d, p, x⟩ ↦
         Quot.map (fun ⟨e, q, r⟩ ↦ ⟨e, Quot.mk _ ⟨d, p, q⟩, r⟩) ?_ x) ?_
@@ -336,18 +282,16 @@ def associatorComponents (X : C) (Y : Fᵒᵖ) :
       rw [coendRel_iff]
       use f
       simp
-    · rintro ⟨d, p, e, q, r⟩ ⟨d', p', e', q', r'⟩ h
-      dsimp
-      rw [coendRel_iff] at h
-      obtain ⟨f, ⟨p, x⟩, h₁, h₂⟩ := h
-      dsimp at h₁ h₂
-      simp only [map_id, Prod.mk.injEq] at h₂
-      obtain ⟨rfl, rfl⟩ := h₁
-      obtain ⟨rfl, h₂⟩ := h₂
-      dsimp at h₂
+    · rintro ⟨d, _, _⟩ ⟨d', _, _⟩ ⟨f, ⟨p, x⟩⟩
+      refine Quot.inductionOn x ?_
+      rintro ⟨e, q, r⟩
       dsimp [Quot.map]
-      rw [Quot.eq] at h₂ ⊢
-      exact associatorComponents_aux₂ _ _ _ h₂
+      simp only [map_id, types_id_apply]
+      -- First use the inner coend condition, then apply the outer quotient constructor.
+      let outer (x : ((P.comp Q).obj X).obj (op e)) :=
+        chosenCoend.ι ((P.comp Q).compDiagram R X (unop Y)) e (x, r)
+      exact congrArg outer
+        (types_congr_hom (chosenCoend.condition (F := P.compDiagram Q X e) f) (p, q))
   hom_inv_id := by
     ext ⟨_, ⟨_, _, _⟩, _⟩
     dsimp [Quot.map]

From 262dd9469171aaa5d1a8f70c58b89ce0e92fc7cf Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Sun, 14 Jun 2026 16:05:15 -0600
Subject: [PATCH 39/40] Apply suggestion from @dagurtomas

---
 Mathlib/Logic/Relation.lean | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index 3eb2a161449e50..8607a7d2f4a46c 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -802,24 +802,6 @@ theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : Eq
   | symm a b _ ih => exact EqvGen.symm _ _ ih
   | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
 
-lemma map (f : α → β) (r : β → β → Prop) (x y : α)
-    (h : EqvGen (fun x y ↦ r (f x) (f y)) x y) : EqvGen r (f x) (f y) := by
-  induction h with
-  | rel => apply EqvGen.rel; assumption
-  | refl => exact EqvGen.refl _
-  | symm => apply EqvGen.symm; assumption
-  | trans => apply EqvGen.trans <;> assumption
-
-@[simp]
-lemma idempotent (r : α → α → Prop) : EqvGen (EqvGen r) = EqvGen r := by
-  ext x y
-  refine ⟨fun h ↦ ?_, fun h ↦ EqvGen.rel _ _ h⟩
-  induction h with
-  | rel => assumption
-  | refl => exact EqvGen.refl _
-  | symm => apply EqvGen.symm; assumption
-  | trans => apply EqvGen.trans <;> assumption
-
 end EqvGen
 
 /-- The join of a relation on a single type is a new relation for which

From 90dacf845c281ee054f291d0a57d369c7d47454e Mon Sep 17 00:00:00 2001
From: Dagur Asgeirsson <dagurtomas@gmail.com>
Date: Thu, 2 Jul 2026 12:04:27 +0000
Subject: [PATCH 40/40] Apply suggestion from @dagurtomas

---
 Mathlib/CategoryTheory/Profunctor/Comp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Profunctor/Comp.lean b/Mathlib/CategoryTheory/Profunctor/Comp.lean
index 86a386d8b0706b..b81b7d3031b60a 100644
--- a/Mathlib/CategoryTheory/Profunctor/Comp.lean
+++ b/Mathlib/CategoryTheory/Profunctor/Comp.lean
@@ -27,7 +27,7 @@ This file defines composition of profunctors. Given profunctors `P : C ⥤ Dᵒ
 * `associator` : The associator isomorphism `(P.comp Q).comp R ≅ P.comp (Q.comp R)`.
 
 These satisfy the coherence laws for a bicategory, see the file
-`CategoryTheory.Profunctor.Bicategory`.
+`CategoryTheory.Profunctor.Bicategory` (to be added in a future PR: #39619).
 -/
 
 @[expose] public section