From 4b8e8b2f8bbfc0cfb06adbe2876fa6cd90b1f13f Mon Sep 17 00:00:00 2001
From: Adrian Marti <25987878+adrianmartir@users.noreply.github.com>
Date: Mon, 2 Mar 2026 12:31:38 +0100
Subject: [PATCH 1/8] Add profunctors and a basic API for them

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

diff --git a/Mathlib/CategoryTheory/Profunctor.lean b/Mathlib/CategoryTheory/Profunctor.lean
new file mode 100644
index 00000000000000..697ea450e898a3
--- /dev/null
+++ b/Mathlib/CategoryTheory/Profunctor.lean
@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2026 Adrian Marti. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adrian Marti, Aristotle
+-/
+module
+
+public import Mathlib.CategoryTheory.Category.Basic
+public import Mathlib.CategoryTheory.EqToHom
+public import Mathlib.Tactic.CategoryTheory.CategoryStar
+
+/-!
+# Profunctors and Natural Transformations
+
+In this file we define profunctors between two categories and natural transformations between profunctors.
+
+Profunctors are defined as a structure with a mapping operation `map` that lets us map on both sides of the profunctor at once. We also provide operations `mapL` and `mapR` to map only on one side.
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+universe w
+
+structure Profunctor (C : Type*) [Category* C] (D : Type*) [Category* D] where
+  obj : D → C → Type w
+  map {X X' : D} {Y Y' : C} (f : X' ⟶ X) (g : Y ⟶ Y') :
+    obj X Y → obj X' Y'
+  map_id (X : D) (Y : C) (e : obj X Y) : map (𝟙 _) (𝟙 _) e = e
+  map_comp {X X' X'' : D} {Y Y' Y'' : C}
+    (f' : X'' ⟶ X') (f : X' ⟶ X)
+    (g : Y ⟶ Y') (g' : Y' ⟶ Y'')
+    (e : obj X Y) :
+    map (f' ≫ f) (g ≫ g') e = map f' g' (map f g e)
+
+
+variable {C : Type*} [Category C] {D : Type*} [Category D]
+
+namespace Profunctor
+
+/-! ### Left and right mapping -/
+
+/-- Apply a profunctor to a morphism on the left (contravariant) side,
+    keeping the right (covariant) side fixed. -/
+def mapL (h : Profunctor.{w} C D) {X X' : D} (f : X ⟶ X') {Y : C} :
+    h.obj X' Y → h.obj X Y :=
+  h.map f (𝟙 Y)
+
+/-- Apply a profunctor to a morphism on the right (covariant) side,
+    keeping the left (contravariant) side fixed. -/
+def mapR (h : Profunctor.{w} C D) {X : D} {Y Y' : C} (g : Y ⟶ Y') :
+    h.obj X Y → h.obj X Y' :=
+  h.map (𝟙 X) g
+
+@[simp]
+theorem mapL_id (h : Profunctor.{w} C D) (X : D) (Y : C) (e : h.obj X Y) :
+    h.mapL (𝟙 X) e = e :=
+  h.map_id X Y e
+
+@[simp]
+theorem mapR_id (h : Profunctor.{w} C D) (X : D) (Y : C) (e : h.obj X Y) :
+    h.mapR (𝟙 Y) e = e :=
+  h.map_id X Y e
+
+theorem mapL_comp (h : Profunctor.{w} C D) {X X' X'' : D} (f : X ⟶ X') (f' : X' ⟶ X'')
+    {Y : C} (e : h.obj X'' Y) :
+    h.mapL (f ≫ f') e = h.mapL f (h.mapL f' e) := by
+  simp only [mapL, ← h.map_comp, Category.comp_id]
+
+theorem mapR_comp (h : Profunctor.{w} C D) {X : D} {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'')
+    (e : h.obj X Y) :
+    h.mapR (g ≫ g') e = h.mapR g' (h.mapR g e) := by
+  simp only [mapR, ← h.map_comp, Category.comp_id]
+
+theorem map_eq_mapL_mapR (h : Profunctor.{w} C D) {X X' : D} {Y Y' : C}
+    (f : X ⟶ X') (g : Y ⟶ Y') (e : h.obj X' Y) :
+    h.map f g e = h.mapR g (h.mapL f e) := by
+  simp only [mapL, mapR, ← h.map_comp, Category.id_comp]
+
+theorem map_eq_mapR_mapL (h : Profunctor.{w} C D) {X X' : D} {Y Y' : C}
+    (f : X ⟶ X') (g : Y ⟶ Y') (e : h.obj X' Y) :
+    h.map f g e = h.mapL f (h.mapR g e) := by
+  simp only [mapL, mapR, ← h.map_comp, Category.comp_id]
+
+def mpRight (h : Profunctor.{w} C D) {a b c} (p : b = c) (f : h.obj a b) : h.obj a c :=
+  h.mapR (eqToHom p) f
+
+def mpLeft (h : Profunctor.{w} C D) {a b c} (p : a = b) (f : h.obj b c) : h.obj a c :=
+  h.mapL (eqToHom p) f
+
+/-- A natural transformation between profunctors `h` and `k`. -/
+structure NatTrans (h k : Profunctor.{w} C D) where
+  /-- The component of the natural transformation at each pair of objects. -/
+  app (X : D) (Y : C) : h.obj X Y → k.obj X Y
+  /-- Naturality: the transformation commutes with `map`. -/
+  naturality {X X' : D} {Y Y' : C} (f : X' ⟶ X) (g : Y ⟶ Y') (e : h.obj X Y) :
+    app X' Y' (h.map f g e) = k.map f g (app X Y e)
+
+namespace NatTrans
+
+/-- The identity natural transformation. -/
+@[simps]
+def id (h : Profunctor.{w} C D) : NatTrans h h where
+  app _ _ e := e
+  naturality _ _ _ := rfl
+
+/-- Composition of natural transformations between profunctors. -/
+@[simps]
+def comp {h k R : Profunctor.{w} C D} (β : NatTrans k R) (α : NatTrans h k) :
+    NatTrans h R where
+  app X Y e := β.app X Y (α.app X Y e)
+  naturality f g e := by rw [α.naturality, β.naturality]
+
+@[ext]
+theorem ext {h k : Profunctor.{w} C D} {α β : NatTrans h k}
+    (h : ∀ (X : D) (Y : C) (e : h.obj X Y), α.app X Y e = β.app X Y e) :
+    α = β := by
+  cases α
+  cases β
+  congr
+  funext X Y e
+  exact h X Y e
+
+@[simp]
+theorem id_comp {h k : Profunctor.{w} C D} (α : NatTrans h k) :
+    (NatTrans.id k).comp α = α := by
+  ext
+  simp [comp, id]
+
+@[simp]
+theorem comp_id {h k : Profunctor.{w} C D} (α : NatTrans h k) :
+    α.comp (NatTrans.id h) = α := by
+  ext
+  simp [comp, id]
+
+theorem comp_assoc {h k R S : Profunctor.{w} C D}
+    (γ : NatTrans R S) (β : NatTrans k R) (α : NatTrans h k) :
+    (γ.comp β).comp α = γ.comp (β.comp α) :=
+  rfl
+
+/-- Naturality with respect to `mapL`. -/
+theorem naturality_mapL {h k : Profunctor.{w} C D} (α : NatTrans h k)
+    {X X' : D} (f : X ⟶ X') {Y : C} (e : h.obj X' Y) :
+    α.app X Y (h.mapL f e) = k.mapL f (α.app X' Y e) := by
+  simp only [mapL]
+  exact α.naturality f (𝟙 Y) e
+
+/-- Naturality with respect to `mapR`. -/
+theorem naturality_mapR {h k : Profunctor.{w} C D} (α : NatTrans h k)
+    {X : D} {Y Y' : C} (g : Y ⟶ Y') (e : h.obj X Y) :
+    α.app X Y' (h.mapR g e) = k.mapR g (α.app X Y e) := by
+  simp only [mapR]
+  exact α.naturality (𝟙 X) g e
+
+end NatTrans
+
+/-! ### Category instance for profunctors -/
+
+/-- The category of profunctors from `D` to `C`, with natural transformations as morphisms. -/
+instance instCategory : Category (Profunctor.{w} C D) where
+  Hom h k := NatTrans h k
+  id h := NatTrans.id h
+  comp α β := β.comp α
+  id_comp := NatTrans.comp_id
+  comp_id := NatTrans.id_comp
+  assoc _ _ _ := (NatTrans.comp_assoc _ _ _).symm
+
+end Profunctor
+
+end CategoryTheory

From d3f755a5fcd92d6fcf9095557a677e7361ba1c25 Mon Sep 17 00:00:00 2001
From: Adrian Marti <25987878+adrianmartir@users.noreply.github.com>
Date: Mon, 2 Mar 2026 12:40:29 +0100
Subject: [PATCH 2/8] Fix variable naming

---
 Mathlib/CategoryTheory/Profunctor.lean | 128 ++++++++++++-------------
 1 file changed, 64 insertions(+), 64 deletions(-)

diff --git a/Mathlib/CategoryTheory/Profunctor.lean b/Mathlib/CategoryTheory/Profunctor.lean
index 697ea450e898a3..90a45e15a6bb0e 100644
--- a/Mathlib/CategoryTheory/Profunctor.lean
+++ b/Mathlib/CategoryTheory/Profunctor.lean
@@ -43,113 +43,113 @@ namespace Profunctor
 
 /-- Apply a profunctor to a morphism on the left (contravariant) side,
     keeping the right (covariant) side fixed. -/
-def mapL (h : Profunctor.{w} C D) {X X' : D} (f : X ⟶ X') {Y : C} :
-    h.obj X' Y → h.obj X Y :=
-  h.map f (𝟙 Y)
+def mapL (H : Profunctor.{w} C D) {X X' : D} (f : X ⟶ X') {Y : C} :
+    H.obj X' Y → H.obj X Y :=
+  H.map f (𝟙 Y)
 
 /-- Apply a profunctor to a morphism on the right (covariant) side,
     keeping the left (contravariant) side fixed. -/
-def mapR (h : Profunctor.{w} C D) {X : D} {Y Y' : C} (g : Y ⟶ Y') :
-    h.obj X Y → h.obj X Y' :=
-  h.map (𝟙 X) g
+def mapR (H : Profunctor.{w} C D) {X : D} {Y Y' : C} (g : Y ⟶ Y') :
+    H.obj X Y → H.obj X Y' :=
+  H.map (𝟙 X) g
 
 @[simp]
-theorem mapL_id (h : Profunctor.{w} C D) (X : D) (Y : C) (e : h.obj X Y) :
-    h.mapL (𝟙 X) e = e :=
-  h.map_id X Y e
+theorem mapL_id (H : Profunctor.{w} C D) (X : D) (Y : C) (e : H.obj X Y) :
+    H.mapL (𝟙 X) e = e :=
+  H.map_id X Y e
 
 @[simp]
-theorem mapR_id (h : Profunctor.{w} C D) (X : D) (Y : C) (e : h.obj X Y) :
-    h.mapR (𝟙 Y) e = e :=
-  h.map_id X Y e
-
-theorem mapL_comp (h : Profunctor.{w} C D) {X X' X'' : D} (f : X ⟶ X') (f' : X' ⟶ X'')
-    {Y : C} (e : h.obj X'' Y) :
-    h.mapL (f ≫ f') e = h.mapL f (h.mapL f' e) := by
-  simp only [mapL, ← h.map_comp, Category.comp_id]
-
-theorem mapR_comp (h : Profunctor.{w} C D) {X : D} {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'')
-    (e : h.obj X Y) :
-    h.mapR (g ≫ g') e = h.mapR g' (h.mapR g e) := by
-  simp only [mapR, ← h.map_comp, Category.comp_id]
-
-theorem map_eq_mapL_mapR (h : Profunctor.{w} C D) {X X' : D} {Y Y' : C}
-    (f : X ⟶ X') (g : Y ⟶ Y') (e : h.obj X' Y) :
-    h.map f g e = h.mapR g (h.mapL f e) := by
-  simp only [mapL, mapR, ← h.map_comp, Category.id_comp]
-
-theorem map_eq_mapR_mapL (h : Profunctor.{w} C D) {X X' : D} {Y Y' : C}
-    (f : X ⟶ X') (g : Y ⟶ Y') (e : h.obj X' Y) :
-    h.map f g e = h.mapL f (h.mapR g e) := by
-  simp only [mapL, mapR, ← h.map_comp, Category.comp_id]
-
-def mpRight (h : Profunctor.{w} C D) {a b c} (p : b = c) (f : h.obj a b) : h.obj a c :=
-  h.mapR (eqToHom p) f
-
-def mpLeft (h : Profunctor.{w} C D) {a b c} (p : a = b) (f : h.obj b c) : h.obj a c :=
-  h.mapL (eqToHom p) f
-
-/-- A natural transformation between profunctors `h` and `k`. -/
-structure NatTrans (h k : Profunctor.{w} C D) where
+theorem mapR_id (H : Profunctor.{w} C D) (X : D) (Y : C) (e : H.obj X Y) :
+    H.mapR (𝟙 Y) e = e :=
+  H.map_id X Y e
+
+theorem mapL_comp (H : Profunctor.{w} C D) {X X' X'' : D} (f : X ⟶ X') (f' : X' ⟶ X'')
+    {Y : C} (e : H.obj X'' Y) :
+    H.mapL (f ≫ f') e = H.mapL f (H.mapL f' e) := by
+  simp only [mapL, ← H.map_comp, Category.comp_id]
+
+theorem mapR_comp (H : Profunctor.{w} C D) {X : D} {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'')
+    (e : H.obj X Y) :
+    H.mapR (g ≫ g') e = H.mapR g' (H.mapR g e) := by
+  simp only [mapR, ← H.map_comp, Category.comp_id]
+
+theorem map_eq_mapL_mapR (H : Profunctor.{w} C D) {X X' : D} {Y Y' : C}
+    (f : X ⟶ X') (g : Y ⟶ Y') (e : H.obj X' Y) :
+    H.map f g e = H.mapR g (H.mapL f e) := by
+  simp only [mapL, mapR, ← H.map_comp, Category.id_comp]
+
+theorem map_eq_mapR_mapL (H : Profunctor.{w} C D) {X X' : D} {Y Y' : C}
+    (f : X ⟶ X') (g : Y ⟶ Y') (e : H.obj X' Y) :
+    H.map f g e = H.mapL f (H.mapR g e) := by
+  simp only [mapL, mapR, ← H.map_comp, Category.comp_id]
+
+def mpRight (H : Profunctor.{w} C D) {a b c} (p : b = c) (f : H.obj a b) : H.obj a c :=
+  H.mapR (eqToHom p) f
+
+def mpLeft (H : Profunctor.{w} C D) {a b c} (p : a = b) (f : H.obj b c) : H.obj a c :=
+  H.mapL (eqToHom p) f
+
+/-- A natural transformation between profunctors `H` and `K`. -/
+structure NatTrans (H K : Profunctor.{w} C D) where
   /-- The component of the natural transformation at each pair of objects. -/
-  app (X : D) (Y : C) : h.obj X Y → k.obj X Y
+  app (X : D) (Y : C) : H.obj X Y → K.obj X Y
   /-- Naturality: the transformation commutes with `map`. -/
-  naturality {X X' : D} {Y Y' : C} (f : X' ⟶ X) (g : Y ⟶ Y') (e : h.obj X Y) :
-    app X' Y' (h.map f g e) = k.map f g (app X Y e)
+  naturality {X X' : D} {Y Y' : C} (f : X' ⟶ X) (g : Y ⟶ Y') (e : H.obj X Y) :
+    app X' Y' (H.map f g e) = K.map f g (app X Y e)
 
 namespace NatTrans
 
 /-- The identity natural transformation. -/
 @[simps]
-def id (h : Profunctor.{w} C D) : NatTrans h h where
+def id (H : Profunctor.{w} C D) : NatTrans H H where
   app _ _ e := e
   naturality _ _ _ := rfl
 
 /-- Composition of natural transformations between profunctors. -/
 @[simps]
-def comp {h k R : Profunctor.{w} C D} (β : NatTrans k R) (α : NatTrans h k) :
-    NatTrans h R where
+def comp {H K R : Profunctor.{w} C D} (β : NatTrans K R) (α : NatTrans H K) :
+    NatTrans H R where
   app X Y e := β.app X Y (α.app X Y e)
   naturality f g e := by rw [α.naturality, β.naturality]
 
 @[ext]
-theorem ext {h k : Profunctor.{w} C D} {α β : NatTrans h k}
-    (h : ∀ (X : D) (Y : C) (e : h.obj X Y), α.app X Y e = β.app X Y e) :
+theorem ext {H K : Profunctor.{w} C D} {α β : NatTrans H K}
+    (H : ∀ (X : D) (Y : C) (e : H.obj X Y), α.app X Y e = β.app X Y e) :
     α = β := by
   cases α
   cases β
   congr
   funext X Y e
-  exact h X Y e
+  exact H X Y e
 
 @[simp]
-theorem id_comp {h k : Profunctor.{w} C D} (α : NatTrans h k) :
-    (NatTrans.id k).comp α = α := by
+theorem id_comp {H K : Profunctor.{w} C D} (α : NatTrans H K) :
+    (NatTrans.id K).comp α = α := by
   ext
   simp [comp, id]
 
 @[simp]
-theorem comp_id {h k : Profunctor.{w} C D} (α : NatTrans h k) :
-    α.comp (NatTrans.id h) = α := by
+theorem comp_id {H K : Profunctor.{w} C D} (α : NatTrans H K) :
+    α.comp (NatTrans.id H) = α := by
   ext
   simp [comp, id]
 
-theorem comp_assoc {h k R S : Profunctor.{w} C D}
-    (γ : NatTrans R S) (β : NatTrans k R) (α : NatTrans h k) :
+theorem comp_assoc {H K L M : Profunctor.{w} C D}
+    (γ : NatTrans R S) (β : NatTrans K R) (α : NatTrans H K) :
     (γ.comp β).comp α = γ.comp (β.comp α) :=
   rfl
 
 /-- Naturality with respect to `mapL`. -/
-theorem naturality_mapL {h k : Profunctor.{w} C D} (α : NatTrans h k)
-    {X X' : D} (f : X ⟶ X') {Y : C} (e : h.obj X' Y) :
-    α.app X Y (h.mapL f e) = k.mapL f (α.app X' Y e) := by
+theorem naturality_mapL {H K : Profunctor.{w} C D} (α : NatTrans H K)
+    {X X' : D} (f : X ⟶ X') {Y : C} (e : H.obj X' Y) :
+    α.app X Y (H.mapL f e) = K.mapL f (α.app X' Y e) := by
   simp only [mapL]
   exact α.naturality f (𝟙 Y) e
 
 /-- Naturality with respect to `mapR`. -/
-theorem naturality_mapR {h k : Profunctor.{w} C D} (α : NatTrans h k)
-    {X : D} {Y Y' : C} (g : Y ⟶ Y') (e : h.obj X Y) :
-    α.app X Y' (h.mapR g e) = k.mapR g (α.app X Y e) := by
+theorem naturality_mapR {H K : Profunctor.{w} C D} (α : NatTrans H K)
+    {X : D} {Y Y' : C} (g : Y ⟶ Y') (e : H.obj X Y) :
+    α.app X Y' (H.mapR g e) = K.mapR g (α.app X Y e) := by
   simp only [mapR]
   exact α.naturality (𝟙 X) g e
 
@@ -159,8 +159,8 @@ end NatTrans
 
 /-- The category of profunctors from `D` to `C`, with natural transformations as morphisms. -/
 instance instCategory : Category (Profunctor.{w} C D) where
-  Hom h k := NatTrans h k
-  id h := NatTrans.id h
+  Hom H K := NatTrans H K
+  id H := NatTrans.id H
   comp α β := β.comp α
   id_comp := NatTrans.comp_id
   comp_id := NatTrans.id_comp

From b5e0f92a8c21e477a60a2ee4d3367316dc378109 Mon Sep 17 00:00:00 2001
From: Adrian Marti <25987878+adrianmartir@users.noreply.github.com>
Date: Mon, 2 Mar 2026 12:55:54 +0100
Subject: [PATCH 3/8] Fix universes and variable naming

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

diff --git a/Mathlib/CategoryTheory/Profunctor.lean b/Mathlib/CategoryTheory/Profunctor.lean
index 90a45e15a6bb0e..15efb550e62480 100644
--- a/Mathlib/CategoryTheory/Profunctor.lean
+++ b/Mathlib/CategoryTheory/Profunctor.lean
@@ -35,7 +35,7 @@ structure Profunctor (C : Type*) [Category* C] (D : Type*) [Category* D] where
     map (f' ≫ f) (g ≫ g') e = map f' g' (map f g e)
 
 
-variable {C : Type*} [Category C] {D : Type*} [Category D]
+variable {C : Type*} [Category* C] {D : Type*} [Category* D]
 
 namespace Profunctor
 
@@ -135,7 +135,7 @@ theorem comp_id {H K : Profunctor.{w} C D} (α : NatTrans H K) :
   simp [comp, id]
 
 theorem comp_assoc {H K L M : Profunctor.{w} C D}
-    (γ : NatTrans R S) (β : NatTrans K R) (α : NatTrans H K) :
+    (γ : NatTrans L M) (β : NatTrans K L) (α : NatTrans H K) :
     (γ.comp β).comp α = γ.comp (β.comp α) :=
   rfl
 

From 30714c8e9f18b7a1a471c1ad23d473dff99aa819 Mon Sep 17 00:00:00 2001
From: Adrian Marti <25987878+adrianmartir@users.noreply.github.com>
Date: Mon, 2 Mar 2026 14:07:51 +0100
Subject: [PATCH 4/8] Wrap lines

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

diff --git a/Mathlib/CategoryTheory/Profunctor.lean b/Mathlib/CategoryTheory/Profunctor.lean
index 15efb550e62480..71cfcf5618378e 100644
--- a/Mathlib/CategoryTheory/Profunctor.lean
+++ b/Mathlib/CategoryTheory/Profunctor.lean
@@ -12,9 +12,11 @@ public import Mathlib.Tactic.CategoryTheory.CategoryStar
 /-!
 # Profunctors and Natural Transformations
 
-In this file we define profunctors between two categories and natural transformations between profunctors.
+In this file we define profunctors between two categories and natural transformations between
+profunctors.
 
-Profunctors are defined as a structure with a mapping operation `map` that lets us map on both sides of the profunctor at once. We also provide operations `mapL` and `mapR` to map only on one side.
+Profunctors are defined as a structure with a mapping operation `map` that lets us map on both sides
+of the profunctor at once. We also provide operations `mapL` and `mapR` to map only on one side.
 -/
 
 @[expose] public section

From 5539fd9d8afbc1626cd13f6afb42cb31623f0460 Mon Sep 17 00:00:00 2001
From: Adrian Marti <25987878+adrianmartir@users.noreply.github.com>
Date: Mon, 2 Mar 2026 20:28:21 +0100
Subject: [PATCH 5/8] Add 'CategoryTheory/Profunctor' to 'Mathlib.lean'

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

diff --git a/Mathlib.lean b/Mathlib.lean
index 7c0496751085f8..dc8f5d64b578d7 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3082,6 +3082,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
 public import Mathlib.CategoryTheory.Quotient
 public import Mathlib.CategoryTheory.Quotient.Linear
 public import Mathlib.CategoryTheory.Quotient.LocallySmall

From c4c5de5ae56b1751279f289661e1f78638ef9262 Mon Sep 17 00:00:00 2001
From: Adrian Marti <25987878+adrianmartir@users.noreply.github.com>
Date: Mon, 2 Mar 2026 21:26:27 +0100
Subject: [PATCH 6/8] Add docstrings to definitions

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

diff --git a/Mathlib/CategoryTheory/Profunctor.lean b/Mathlib/CategoryTheory/Profunctor.lean
index 71cfcf5618378e..c9f1ea86c9f7ea 100644
--- a/Mathlib/CategoryTheory/Profunctor.lean
+++ b/Mathlib/CategoryTheory/Profunctor.lean
@@ -25,11 +25,17 @@ namespace CategoryTheory
 
 universe w
 
+/-- A profunctor between two categories `C` and `D` is a functor from `Cᵒᵖ × D` to the category of
+types. We encode this data as a structure. -/
 structure Profunctor (C : Type*) [Category* C] (D : Type*) [Category* D] where
+  /-- Apply a profunctor to a pair of objects. -/
   obj : D → C → Type w
+  /-- Apply a profunctor to a pair of maps. -/
   map {X X' : D} {Y Y' : C} (f : X' ⟶ X) (g : Y ⟶ Y') :
     obj X Y → obj X' Y'
+  /-- Identity law for profunctors. -/
   map_id (X : D) (Y : C) (e : obj X Y) : map (𝟙 _) (𝟙 _) e = e
+  /-- Composition law for profunctors. -/
   map_comp {X X' X'' : D} {Y Y' Y'' : C}
     (f' : X'' ⟶ X') (f : X' ⟶ X)
     (g : Y ⟶ Y') (g' : Y' ⟶ Y'')
@@ -85,12 +91,14 @@ theorem map_eq_mapR_mapL (H : Profunctor.{w} C D) {X X' : D} {Y Y' : C}
     H.map f g e = H.mapL f (H.mapR g e) := by
   simp only [mapL, mapR, ← H.map_comp, Category.comp_id]
 
-def mpRight (H : Profunctor.{w} C D) {a b c} (p : b = c) (f : H.obj a b) : H.obj a c :=
-  H.mapR (eqToHom p) f
-
+/-- Transport a profunctor along an equality on the left. -/
 def mpLeft (H : Profunctor.{w} C D) {a b c} (p : a = b) (f : H.obj b c) : H.obj a c :=
   H.mapL (eqToHom p) f
 
+/-- Transport a profunctor along an equality on the right. -/
+def mpRight (H : Profunctor.{w} C D) {a b c} (p : b = c) (f : H.obj a b) : H.obj a c :=
+  H.mapR (eqToHom p) f
+
 /-- A natural transformation between profunctors `H` and `K`. -/
 structure NatTrans (H K : Profunctor.{w} C D) where
   /-- The component of the natural transformation at each pair of objects. -/

From a5f0dbda3757e7e71dd0b3380c1db113d6c4ae8b Mon Sep 17 00:00:00 2001
From: Adrian Marti <25987878+adrianmartir@users.noreply.github.com>
Date: Tue, 3 Mar 2026 12:04:33 +0100
Subject: [PATCH 7/8] Add grind and simp attributes

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

diff --git a/Mathlib/CategoryTheory/Profunctor.lean b/Mathlib/CategoryTheory/Profunctor.lean
index c9f1ea86c9f7ea..e6664be887c366 100644
--- a/Mathlib/CategoryTheory/Profunctor.lean
+++ b/Mathlib/CategoryTheory/Profunctor.lean
@@ -42,6 +42,9 @@ structure Profunctor (C : Type*) [Category* C] (D : Type*) [Category* D] where
     (e : obj X Y) :
     map (f' ≫ f) (g ≫ g') e = map f' g' (map f g e)
 
+attribute [simp] Profunctor.map_id Profunctor.map_comp
+attribute [grind =] Profunctor.map_id
+attribute [grind _=_] Profunctor.map_comp
 
 variable {C : Type*} [Category* C] {D : Type*} [Category* D]
 

From b27a52d61133ba828a907457b6a4ae12b13640c7 Mon Sep 17 00:00:00 2001
From: Adrian Marti <25987878+adrianmartir@users.noreply.github.com>
Date: Tue, 3 Mar 2026 12:05:58 +0100
Subject: [PATCH 8/8] Fix 'Profunctor' docstring

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

diff --git a/Mathlib/CategoryTheory/Profunctor.lean b/Mathlib/CategoryTheory/Profunctor.lean
index e6664be887c366..fede8bea7083c0 100644
--- a/Mathlib/CategoryTheory/Profunctor.lean
+++ b/Mathlib/CategoryTheory/Profunctor.lean
@@ -25,7 +25,7 @@ namespace CategoryTheory
 
 universe w
 
-/-- A profunctor between two categories `C` and `D` is a functor from `Cᵒᵖ × D` to the category of
+/-- A profunctor between two categories `C` and `D` is a functor from `Dᵒᵖ × C` to the category of
 types. We encode this data as a structure. -/
 structure Profunctor (C : Type*) [Category* C] (D : Type*) [Category* D] where
   /-- Apply a profunctor to a pair of objects. -/