From f60914d41f4bfd13f43748fd2ffa80f13e331706 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Mon, 6 Mar 2023 21:39:12 -0500 Subject: [PATCH] Implement Mapping profunctors --- Data/Profunctor/Mapping.idr | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Data/Profunctor/Mapping.idr b/Data/Profunctor/Mapping.idr index 00bde0a..56d3d67 100644 --- a/Data/Profunctor/Mapping.idr +++ b/Data/Profunctor/Mapping.idr @@ -16,3 +16,15 @@ interface (Traversing p, Closed p) => Mapping p where where functor : Functor (\a => (a -> b) -> t) functor = MkFunctor (\f => (. (. f))) + + +export +Mapping Morphism where + map' (Mor f) = Mor (map f) + roam f (Mor x) = Mor (f x) + +export +[Function] Mapping (\a,b => a -> b) + using Traversing.Function Closed.Function where + map' = map + roam = id