From f24cbd0db0810a3396a19f32833b427efd258502 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 6 Mar 2023 22:47:03 -0500
Subject: [PATCH] Create Data.Profunctor.Costrong

---
 Data/Profunctor/Costrong.idr | 179 +++++++++++++++++++++++++++++++++++
 Data/Profunctor/Yoneda.idr   |  11 +++
 2 files changed, 190 insertions(+)
 create mode 100644 Data/Profunctor/Costrong.idr

diff --git a/Data/Profunctor/Costrong.idr b/Data/Profunctor/Costrong.idr
new file mode 100644
index 0000000..3a13354
--- /dev/null
+++ b/Data/Profunctor/Costrong.idr
@@ -0,0 +1,179 @@
+module Data.Profunctor.Costrong
+
+import Data.Morphisms
+import Data.Tensor
+import Data.Profunctor.Functor
+import Data.Profunctor.Types
+
+%default total
+
+public export
+interface Profunctor p => GenCostrong (0 ten : Type -> Type -> Type) p where
+  costrongl : p (a `ten` c) (b `ten` c) -> p a b
+  costrongr : p (c `ten` a) (c `ten` b) -> p a b
+
+
+public export
+Costrong : (p : Type -> Type -> Type) -> Type
+Costrong = GenCostrong Pair
+
+public export
+unfirst : Costrong p => p (a, c) (b, c) -> p a b
+unfirst = costrongl {ten=Pair}
+
+public export
+unsecond : Costrong p => p (c, a) (c, b) -> p a b
+unsecond = costrongr {ten=Pair}
+
+public export
+Cochoice : (p : Type -> Type -> Type) -> Type
+Cochoice = GenCostrong Either
+
+public export
+unleft : Cochoice p => p (Either a c) (Either b c) -> p a b
+unleft = costrongl {ten=Either}
+
+public export
+unright : Cochoice p => p (Either c a) (Either c b) -> p a b
+unright = costrongr {ten=Either}
+
+-- Implementations
+
+export
+GenCostrong Pair Tagged where
+  costrongl (Tag (x,_)) = Tag x
+  costrongr (Tag (_,x)) = Tag x
+
+
+-- Tambara
+
+public export
+data GenCotambara : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
+  MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b
+
+export
+Profunctor (GenCotambara ten p) where
+  lmap f (MkCotambara n p) = MkCotambara n (lmap f p)
+  rmap f (MkCotambara n p) = MkCotambara n (rmap f p)
+  dimap f g (MkCotambara n p) = MkCotambara n (dimap f g p)
+
+export
+ProfunctorFunctor (GenCotambara ten) where
+  promap f (MkCotambara n p) = MkCotambara (f . n) p
+
+export
+GenCostrong ten (GenCotambara ten p) where
+  costrongl (MkCotambara @{costr} n p) = MkCotambara n (costrongl @{costr} p)
+  costrongr (MkCotambara @{costr} n p) = MkCotambara n (costrongr @{costr} p)
+
+export
+ProfunctorComonad (GenCotambara ten) where
+  proextract (MkCotambara n p) = n p
+  produplicate (MkCotambara n p) = MkCotambara id (MkCotambara n p)
+
+export
+Functor (GenCotambara ten p a) where
+  map = rmap
+
+
+export
+gencotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q
+gencotambara f = MkCotambara f
+
+export
+ungencotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q
+ungencotambara f p = proextract (f p)
+
+
+public export
+Cotambara : (p : Type -> Type -> Type) -> Type -> Type -> Type
+Cotambara = GenCotambara Pair
+
+export
+cotambara : Costrong p => p :-> q -> p :-> Cotambara q
+cotambara = gencotambara
+
+export
+uncotambara : Profunctor q => p :-> Cotambara q -> p :-> q
+uncotambara = ungencotambara
+
+
+public export
+CotambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
+CotambaraSum = GenCotambara Either
+
+export
+cotambaraSum : Cochoice p => p :-> q -> p :-> CotambaraSum q
+cotambaraSum = gencotambara
+
+export
+uncotambaraSum : Profunctor q => p :-> CotambaraSum q -> p :-> q
+uncotambaraSum = ungencotambara
+
+
+-- Copastro
+
+public export
+record GenCopastro (ten, p : Type -> Type -> Type) a b where
+  constructor MkCopastro
+  runCopastro : forall q. GenCostrong ten q => p :-> q -> q a b
+
+export
+Profunctor (GenCopastro ten p) where
+  dimap f g (MkCopastro h) = MkCopastro $ \n => dimap f g (h n)
+  lmap f (MkCopastro h) = MkCopastro $ \n => lmap f (h n)
+  rmap f (MkCopastro h) = MkCopastro $ \n => rmap f (h n)
+
+export
+ProfunctorFunctor (GenCopastro ten) where
+  promap f (MkCopastro h) = MkCopastro $ \n => h (n . f)
+
+export
+ProfunctorMonad (GenCopastro ten) where
+  propure p = MkCopastro ($ p)
+  projoin p = MkCopastro $ \x => runCopastro p (\y => runCopastro y x)
+
+export
+GenCostrong ten (GenCopastro ten p) where
+  costrongl (MkCopastro h) = MkCopastro $ \n => costrongl {ten} (h n)
+  costrongr (MkCopastro h) = MkCopastro $ \n => costrongr {ten} (h n)
+
+export
+ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where
+  prounit p = MkCotambara id (propure {t=GenCopastro ten} p)
+  procounit (MkCopastro h) = proextract (h id)
+
+
+export
+gencopastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q
+gencopastro f (MkCopastro h) = h f
+
+export
+ungencopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q
+ungencopastro f x = f (MkCopastro ($ x))
+
+
+public export
+Copastro : (p : Type -> Type -> Type) -> Type -> Type -> Type
+Copastro = GenCopastro Pair
+
+export
+copastro : Costrong q => p :-> q -> Copastro p :-> q
+copastro = gencopastro
+
+export
+uncopastro : Copastro p :-> q -> p :-> q
+uncopastro = ungencopastro
+
+
+public export
+CopastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
+CopastroSum = GenCopastro Either
+
+export
+copastroSum : Cochoice q => p :-> q -> CopastroSum p :-> q
+copastroSum = gencopastro
+
+export
+uncopastroSum : CopastroSum p :-> q -> p :-> q
+uncopastroSum = ungencopastro
diff --git a/Data/Profunctor/Yoneda.idr b/Data/Profunctor/Yoneda.idr
index 7cd035f..08edd93 100644
--- a/Data/Profunctor/Yoneda.idr
+++ b/Data/Profunctor/Yoneda.idr
@@ -1,6 +1,7 @@
 module Data.Profunctor.Yoneda
 
 import Data.Profunctor
+import Data.Profunctor.Costrong
 import Data.Profunctor.Traversing
 import Data.Profunctor.Mapping
 import Data.Profunctor.Sieve
@@ -46,6 +47,11 @@ GenStrong ten p => GenStrong ten (Yoneda p) where
   strongl = propure . strongl {ten,p} . proextract
   strongr = propure . strongr {ten,p} . proextract
 
+export
+GenCostrong ten p => GenCostrong ten (Yoneda p) where
+  costrongl = propure . costrongl {ten,p} . proextract
+  costrongr = propure . costrongr {ten,p} . proextract
+
 export
 Closed p => Closed (Yoneda p) where
   closed = propure . closed . proextract
@@ -107,6 +113,11 @@ GenStrong ten p => GenStrong ten (Coyoneda p) where
   strongl = propure . strongl {ten,p} . proextract
   strongr = propure . strongr {ten,p} . proextract
 
+export
+GenCostrong ten p => GenCostrong ten (Coyoneda p) where
+  costrongl = propure . costrongl {ten,p} . proextract
+  costrongr = propure . costrongr {ten,p} . proextract
+
 export
 Closed p => Closed (Coyoneda p) where
   closed = propure . closed . proextract