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