From 22da62a6f52efc968112824c944215354c973a43 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 6 Mar 2023 21:36:44 -0500
Subject: [PATCH] Implement Traversing profunctors

---
 Data/Profunctor/Closed.idr | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/Data/Profunctor/Closed.idr b/Data/Profunctor/Closed.idr
index 12a44ec..f7dbd6f 100644
--- a/Data/Profunctor/Closed.idr
+++ b/Data/Profunctor/Closed.idr
@@ -1,5 +1,6 @@
 module Data.Profunctor.Closed
 
+import Data.Morphisms
 import Data.Profunctor.Types
 import Data.Profunctor.Functor
 import Data.Profunctor.Strong
@@ -12,6 +13,19 @@ interface Profunctor p => Closed p where
   closed : p a b -> p (x -> a) (x -> b)
 
 
+export
+Closed Morphism where
+  closed (Mor f) = Mor (f .)
+
+export
+[Function] Closed (\a,b => a -> b) using Profunctor.Function where
+  closed = (.)
+
+export
+Functor f => Closed (Costar f) where
+  closed (MkCostar p) = MkCostar $ \f,x => p (map ($ x) f)
+
+
 export
 curry' : Closed p => p (a, b) c -> p a (b -> c)
 curry' = lmap (,) . closed
@@ -24,7 +38,6 @@ yon : (s -> a, s -> b) -> s -> (a,b)
 yon h s = (fst h s, snd h s)
 
 
-
 -- Closure
 
 public export