From 80fb506448f4ce14bc497cb95dc35f32321e6178 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 5 Mar 2023 00:00:50 -0500
Subject: [PATCH] Define profunctor adjunctions

---
 Data/Profunctor/Functor.idr | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/Data/Profunctor/Functor.idr b/Data/Profunctor/Functor.idr
index 6ae53df..841e941 100644
--- a/Data/Profunctor/Functor.idr
+++ b/Data/Profunctor/Functor.idr
@@ -10,11 +10,20 @@ interface ProfunctorFunctor (0 t : (Type -> Type -> Type) -> k -> k' -> Type) wh
   promap : Profunctor p => p :-> q -> t p :-> t q
 
 public export
-interface ProfunctorFunctor t => ProfunctorMonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
+interface ProfunctorFunctor t =>
+    ProfunctorMonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
   propure : Profunctor p => p :-> t p
   projoin : Profunctor p => t (t p) :-> t p
 
 public export
-interface ProfunctorFunctor t => ProfunctorComonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
+interface ProfunctorFunctor t =>
+    ProfunctorComonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
   proextract : Profunctor p => t p :-> p
   produplicate : Profunctor p => t p :-> t (t p)
+
+public export
+interface (ProfunctorFunctor f, ProfunctorFunctor u) =>
+    ProfunctorAdjunction (0 f : (Type -> Type -> Type) -> Type -> Type -> Type)
+                         (0 u : (Type -> Type -> Type) -> Type -> Type -> Type) | f, u where
+  prounit   : Profunctor p => p :-> u (f p)
+  procounit : Profunctor p => f (u p) :-> p