From 36f5c18f0f138d33aa52d4226e89ba6007a9ab06 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 6 Mar 2023 21:38:42 -0500
Subject: [PATCH] Create Data.Profunctor.Mapping

---
 Data/Profunctor/Mapping.idr | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 Data/Profunctor/Mapping.idr

diff --git a/Data/Profunctor/Mapping.idr b/Data/Profunctor/Mapping.idr
new file mode 100644
index 0000000..00bde0a
--- /dev/null
+++ b/Data/Profunctor/Mapping.idr
@@ -0,0 +1,18 @@
+module Data.Profunctor.Mapping
+
+import Data.Profunctor
+import Data.Profunctor.Traversing
+
+%default total
+
+
+public export
+interface (Traversing p, Closed p) => Mapping p where
+  map' : Functor f => p a b -> p (f a) (f b)
+  map' = roam map
+
+  roam : ((a -> b) -> s -> t) -> p a b -> p s t
+  roam f = dimap (flip f) ($ id) . map' @{%search} @{functor}
+    where
+      functor : Functor (\a => (a -> b) -> t)
+      functor = MkFunctor (\f => (. (. f)))