From 3d350068c5c590c8197ced3e17239cb2e8d2b7fd Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Tue, 7 Mar 2023 13:16:27 -0500 Subject: [PATCH] Add Sieve implementation for Cayley --- Data/Profunctor/Cayley.idr | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Data/Profunctor/Cayley.idr b/Data/Profunctor/Cayley.idr index 43100c4..802d8cb 100644 --- a/Data/Profunctor/Cayley.idr +++ b/Data/Profunctor/Cayley.idr @@ -54,6 +54,10 @@ Functor f => Mapping p => Mapping (Cayley f p) where map' (MkCayley p) = MkCayley (map' <$> p) roam f (MkCayley p) = MkCayley (roam f <$> p) +export +Functor g => Sieve p f => Sieve (Cayley g p) (g . f) using Functor.Compose where + sieve (MkCayley p) x = ($ x) . sieve <$> p + export mapCayley : (forall x. f x -> g x) -> Cayley f p a b -> Cayley g p a b