From 551f238ab7e39062ced3ea353aae3754f2962116 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 5 Mar 2023 17:06:27 -0500
Subject: [PATCH] Add profunctor strength interface

---
 Data/Profunctor/Functor.idr |  3 +--
 Data/Profunctor/Strong.idr  | 42 +++++++++++++++++++++++++++++++++++++
 2 files changed, 43 insertions(+), 2 deletions(-)
 create mode 100644 Data/Profunctor/Strong.idr

diff --git a/Data/Profunctor/Functor.idr b/Data/Profunctor/Functor.idr
index 841e941..b6c8e76 100644
--- a/Data/Profunctor/Functor.idr
+++ b/Data/Profunctor/Functor.idr
@@ -23,7 +23,6 @@ interface ProfunctorFunctor t =>
 
 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
+    ProfunctorAdjunction (0 f, u : (Type -> Type -> Type) -> Type -> Type -> Type) | f, u where
   prounit   : Profunctor p => p :-> u (f p)
   procounit : Profunctor p => f (u p) :-> p
diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr
new file mode 100644
index 0000000..352b705
--- /dev/null
+++ b/Data/Profunctor/Strong.idr
@@ -0,0 +1,42 @@
+module Data.Profunctor.Strong
+
+import Data.Profunctor.Functor
+import Data.Profunctor.Types
+
+%default total
+
+public export
+interface Profunctor p => GenStrong (0 ten : Type -> Type -> Type) p where
+  strongl : p a b -> p (a `ten` c) (b `ten` c)
+  strongr : p a b -> p (c `ten` a) (c `ten` b)
+
+
+public export
+Strong : (p : Type -> Type -> Type) -> Type
+Strong = GenStrong Pair
+
+public export
+first : Strong p => p a b -> p (a, c) (b, c)
+first = strongl {ten=Pair}
+
+public export
+second : Strong p => p a b -> p (c, a) (c, b)
+second = strongr {ten=Pair}
+
+
+
+export
+uncurry' : Strong p => p a (b -> c) -> p (a, b) c
+uncurry' = rmap (uncurry id) . first
+
+
+-- Tambara
+
+public export
+record GenTambara (ten, p : Type -> Type -> Type) where
+  constructor MkTambara
+  getTambara : {0 c : Type} -> p (a `ten` c) (b `ten` c)
+
+public export
+Tambara : (p : Type -> Type -> Type) -> Type
+Tambara = GenTambara Pair