Data/Profunctor/Cayley.idr

@@ -18,50 +18,50 @@ record Cayley {0 k1,k2,k3 : Type} f (p : k1 -> k2 -> k3) a b where
   runCayley : f (p a b)
 
 
-public export
+export
 Functor f => Profunctor p => Profunctor (Cayley f p) where
   dimap f g (MkCayley p) = MkCayley (dimap f g <$> p)
   lmap f (MkCayley p) = MkCayley (lmap f <$> p)
   rmap g (MkCayley p) = MkCayley (rmap g <$> p)
 
-public export
+export
 Functor f => ProfunctorFunctor (Cayley f) where
   promap f (MkCayley p) = MkCayley (map f p)
 
-public export
+export
 Monad m => ProfunctorMonad (Cayley m) where
   propure = MkCayley . pure
   projoin (MkCayley p) = MkCayley $ p >>= runCayley
 
-public export
+export
 Functor f => GenStrong ten p => GenStrong ten (Cayley f p) where
   strongl (MkCayley p) = MkCayley (strongl {ten} <$> p)
   strongr (MkCayley p) = MkCayley (strongr {ten} <$> p)
 
-public export
+export
 Functor f => GenCostrong ten p => GenCostrong ten (Cayley f p) where
   costrongl (MkCayley p) = MkCayley (costrongl {ten} <$> p)
   costrongr (MkCayley p) = MkCayley (costrongr {ten} <$> p)
 
-public export
+export
 Functor f => Closed p => Closed (Cayley f p) where
   closed (MkCayley p) = MkCayley (closed <$> p)
 
-public export
+export
 Functor f => Traversing p => Traversing (Cayley f p) where
   traverse' (MkCayley p) = MkCayley (traverse' <$> p)
   wander f (MkCayley p) = MkCayley (wander f <$> p)
 
-public export
+export
 Functor f => Mapping p => Mapping (Cayley f p) where
   map' (MkCayley p) = MkCayley (map' <$> p)
   roam f (MkCayley p) = MkCayley (roam f <$> p)
 
-public export
+export
 Functor g => Sieve p f => Sieve (Cayley g p) (g . f) using Functor.Compose where
   sieve (MkCayley p) x = ($ x) . sieve <$> p
 
 
-public export
-mapCayley : (forall x. f x -> g x) -> Cayley f p :-> Cayley g p
+export
+mapCayley : (forall x. f x -> g x) -> Cayley f p a b -> Cayley g p a b
 mapCayley f (MkCayley p) = MkCayley (f p)

Data/Profunctor/Closed.idr

@@ -26,26 +26,26 @@ interface Profunctor p => Closed p where
 
 
 ------------------------------------------------------------------------------
--- Implementations
+-- Implementations for existing types
 ------------------------------------------------------------------------------
 
 
-public export
+export
 Closed Morphism where
   closed (Mor f) = Mor (f .)
 
 ||| A named implementation of `Closed` for function types.
 ||| Use this to avoid having to use a type wrapper like `Morphism`.
-public export
+export
 [Function] Closed (\a,b => a -> b) using Profunctor.Function where
   closed = (.)
 
-public export
+export
 Functor f => Closed (Costar f) where
   closed (MkCostar p) = MkCostar $ \f,x => p (map ($ x) f)
 
 
-public export
+export
 curry' : Closed p => p (a, b) c -> p a (b -> c)
 curry' = lmap (,) . closed
 
@@ -71,40 +71,40 @@ record Closure p a b where
   runClosure : forall x. p (x -> a) (x -> b)
 
 
-public export
+export
 Profunctor p => Profunctor (Closure p) where
   dimap f g (MkClosure p) = MkClosure $ dimap (f .) (g .) p
   lmap f (MkClosure p) = MkClosure $ lmap (f .) p
   rmap f (MkClosure p) = MkClosure $ rmap (f .) p
 
-public export
+export
 ProfunctorFunctor Closure where
   promap f (MkClosure p) = MkClosure (f p)
 
-public export
+export
 ProfunctorComonad Closure where
   proextract (MkClosure p) = dimap const ($ ()) p
   produplicate (MkClosure p) = MkClosure $ MkClosure $ dimap uncurry curry p
 
-public export
+export
 Strong p => GenStrong Pair (Closure p) where
   strongl (MkClosure p) = MkClosure $ dimap hither yon $ first p
   strongr (MkClosure p) = MkClosure $ dimap hither yon $ second p
 
-public export
+export
 Profunctor p => Closed (Closure p) where
   closed p = runClosure $ produplicate p
 
-public export
+export
 Profunctor p => Functor (Closure p a) where
   map = rmap
 
 
-public export
+export
 close : Closed p => p :-> q -> p :-> Closure q
 close f p = MkClosure $ f $ closed p
 
-public export
+export
 unclose : Profunctor q => p :-> Closure q -> p :-> q
 unclose f p = dimap const ($ ()) $ runClosure $ f p
 
@@ -121,17 +121,17 @@ data Environment : (p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkEnv : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
 
 
-public export
+export
 Profunctor (Environment p) where
   dimap f g (MkEnv l m r) = MkEnv (g . l) m (r . f)
   lmap f (MkEnv l m r) = MkEnv l m (r . f)
   rmap g (MkEnv l m r) = MkEnv (g . l) m r
 
-public export
+export
 ProfunctorFunctor Environment where
   promap f (MkEnv l m r) = MkEnv l (f m) r
 
-public export
+export
 ProfunctorMonad Environment where
   propure p = MkEnv ($ ()) p const
   projoin (MkEnv {x=x',y=y',z=z'} l' (MkEnv {x,y,z} l m r) r') = MkEnv (ll . curry) m rr
@@ -141,12 +141,12 @@ ProfunctorMonad Environment where
       rr : a -> (z', z) -> x
       rr a (b, c) = r (r' a b) c
 
-public export
+export
 ProfunctorAdjunction Environment Closure where
   prounit p = MkClosure (MkEnv id p id)
   procounit (MkEnv l (MkClosure x) r) = dimap r l x
 
-public export
+export
 Closed (Environment p) where
   closed {x=x'} (MkEnv {x,y,z} l m r) = MkEnv l' m r'
     where
@@ -155,15 +155,15 @@ Closed (Environment p) where
       r' : (x' -> a) -> (z, x') -> x
       r' f (z,x) = r (f x) z
 
-public export
+export
 Profunctor p => Functor (Environment p a) where
   map = rmap
 
 
-public export
+export
 environment : Closed q => p :-> q -> Environment p :-> q
 environment f (MkEnv l m r) = dimap r l $ closed (f m)
 
-public export
+export
 unenvironment : Environment p :-> q -> p :-> q
 unenvironment f p = f (MkEnv ($ ()) p const)

Data/Profunctor/Costrong.idr

@@ -80,25 +80,15 @@ unright = costrongr {ten=Either}
 
 
 ------------------------------------------------------------------------------
--- Implementations
+-- Implementations for existing types
 ------------------------------------------------------------------------------
 
 
-public export
+export
 GenCostrong Pair Tagged where
   costrongl (Tag (x,_)) = Tag x
   costrongr (Tag (_,x)) = Tag x
 
-public export
-GenCostrong Either (Forget r) where
-  costrongl (MkForget k) = MkForget (k . Left)
-  costrongr (MkForget k) = MkForget (k . Right)
-
-public export
-GenCostrong Pair (Coforget r) where
-  costrongl (MkCoforget k) = MkCoforget (fst . k)
-  costrongr (MkCoforget k) = MkCoforget (snd . k)
-
 
 ------------------------------------------------------------------------------
 -- Cotambara
@@ -111,27 +101,27 @@ public export
 data GenCotambara : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b
 
-public export
+export
 Profunctor (GenCotambara ten p) where
   lmap f (MkCotambara n p) = MkCotambara n (lmap f p)
   rmap f (MkCotambara n p) = MkCotambara n (rmap f p)
   dimap f g (MkCotambara n p) = MkCotambara n (dimap f g p)
 
-public export
+export
 ProfunctorFunctor (GenCotambara ten) where
   promap f (MkCotambara n p) = MkCotambara (f . n) p
 
-public export
+export
 GenCostrong ten (GenCotambara ten p) where
   costrongl (MkCotambara @{costr} n p) = MkCotambara n (costrongl @{costr} p)
   costrongr (MkCotambara @{costr} n p) = MkCotambara n (costrongr @{costr} p)
 
-public export
+export
 ProfunctorComonad (GenCotambara ten) where
   proextract (MkCotambara n p) = n p
   produplicate (MkCotambara n p) = MkCotambara id (MkCotambara n p)
 
-public export
+export
 Functor (GenCotambara ten p a) where
   map = rmap
 
@@ -153,11 +143,11 @@ CotambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
 CotambaraSum = GenCotambara Either
 
 
-public export
+export
 cotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q
 cotambara f = MkCotambara f
 
-public export
+export
 uncotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q
 uncotambara f p = proextract (f p)
 
@@ -174,27 +164,27 @@ record GenCopastro (ten, p : Type -> Type -> Type) a b where
   constructor MkCopastro
   runCopastro : forall q. GenCostrong ten q => p :-> q -> q a b
 
-public export
+export
 Profunctor (GenCopastro ten p) where
   dimap f g (MkCopastro h) = MkCopastro $ \n => dimap f g (h n)
   lmap f (MkCopastro h) = MkCopastro $ \n => lmap f (h n)
   rmap f (MkCopastro h) = MkCopastro $ \n => rmap f (h n)
 
-public export
+export
 ProfunctorFunctor (GenCopastro ten) where
   promap f (MkCopastro h) = MkCopastro $ \n => h (n . f)
 
-public export
+export
 ProfunctorMonad (GenCopastro ten) where
   propure p = MkCopastro ($ p)
   projoin p = MkCopastro $ \x => runCopastro p (\y => runCopastro y x)
 
-public export
+export
 GenCostrong ten (GenCopastro ten p) where
   costrongl (MkCopastro h) = MkCopastro $ \n => costrongl {ten} (h n)
   costrongr (MkCopastro h) = MkCopastro $ \n => costrongr {ten} (h n)
 
-public export
+export
 ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where
   prounit p = MkCotambara id (propure {t=GenCopastro ten} p)
   procounit (MkCopastro h) = proextract (h id)
@@ -217,10 +207,10 @@ CopastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
 CopastroSum = GenCopastro Either
 
 
-public export
+export
 copastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q
 copastro f (MkCopastro h) = h f
 
-public export
+export
 uncopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q
 uncopastro f x = f (MkCopastro ($ x))

Data/Profunctor/Mapping.idr

@@ -1,5 +1,6 @@
 module Data.Profunctor.Mapping
 
+import Control.Monad.Identity
 import Data.Morphisms
 import Data.Tensor
 import Data.Profunctor
@@ -8,9 +9,6 @@ import Data.Profunctor.Traversing
 %default total
 
 
-functor : Functor (\a => (a -> b) -> t)
-functor = MkFunctor (\f => (. (. f)))
-
 ------------------------------------------------------------------------------
 -- Mapping interface
 ------------------------------------------------------------------------------
@@ -22,7 +20,7 @@ functor = MkFunctor (\f => (. (. f)))
 ||| * `map' . lmap f = lmap (map f) . map'`
 ||| * `map' . rmap f = rmap (map f) . map'`
 ||| * `map' . map' = map' @{Compose}`
-||| * `dimap Id runIdentity . map' = id`
+||| * `dimap Identity runIdentity . map' = id`
 public export
 interface (Traversing p, Closed p) => Mapping p where
   map' : Functor f => p a b -> p (f a) (f b)
@@ -30,21 +28,24 @@ interface (Traversing p, Closed p) => Mapping p where
 
   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)))
 
 
 ------------------------------------------------------------------------------
--- Implementations
+-- Implementations for existing types
 ------------------------------------------------------------------------------
 
 
-public export
+export
 Mapping Morphism where
   map' (Mor f) = Mor (map f)
   roam f (Mor x) = Mor (f x)
 
 ||| A named implementation of `Mapping` for function types.
 ||| Use this to avoid having to use a type wrapper like `Morphism`.
-public export
+export
 [Function] Mapping (\a,b => a -> b)
     using Traversing.Function Closed.Function where
   map' = map
@@ -52,7 +53,7 @@ public export
 
 
 ------------------------------------------------------------------------------
--- CofreeMapping
+-- Implementations for existing types
 ------------------------------------------------------------------------------
 
 
@@ -63,44 +64,47 @@ record CofreeMapping p a b where
   constructor MkCFM
   runCFM : forall f. Functor f => p (f a) (f b)
 
-public export
+export
 Profunctor p => Profunctor (CofreeMapping p) where
   lmap f (MkCFM p) = MkCFM (lmap (map f) p)
   rmap f (MkCFM p) = MkCFM (rmap (map f) p)
   dimap f g (MkCFM p) = MkCFM (dimap (map f) (map g) p)
 
-public export
+export
 Profunctor p => Functor (CofreeMapping p a) where
   map = rmap
 
-public export
+export
 ProfunctorFunctor CofreeMapping where
   promap f (MkCFM p) = MkCFM (f p)
 
-public export
+export
 ProfunctorComonad CofreeMapping where
-  proextract (MkCFM p) = p @{FunctorId}
+  proextract (MkCFM p) = dimap Id runIdentity p
   produplicate (MkCFM p) = MkCFM $ MkCFM $ p @{Compose}
 
-public export
+export
 Symmetric ten => Profunctor p => GenStrong ten (CofreeMapping p) where
   strongr (MkCFM p) = MkCFM (p @{Compose {g=ten c} @{%search} @{MkFunctor mapSnd}})
   strongl (MkCFM p) = MkCFM (p @{Compose {g=(`ten` c)} @{%search} @{MkFunctor mapFst}})
 
-public export
+export
 Profunctor p => Closed (CofreeMapping p) where
   closed (MkCFM p) = MkCFM (p @{Compose {g = \b => x -> b} @{%search} @{MkFunctor (.)}})
 
 roamCofree : Profunctor p => ((a -> b) -> s -> t) -> CofreeMapping p a b -> CofreeMapping p s t
 roamCofree f (MkCFM p) = MkCFM $ dimap (map (flip f)) (map ($ id)) $
       p @{Compose @{%search} @{functor}}
+  where
+    functor : Functor (\a => (a -> b) -> t)
+    functor = MkFunctor (\f => (. (. f)))
 
-public export
+export
 Profunctor p => Traversing (CofreeMapping p) where
   traverse' (MkCFM p) = MkCFM (p @{Compose})
-  wander f = roamCofree $ f @{ApplicativeId}
+  wander f = roamCofree $ (runIdentity .) . f . (Id .)
 
-public export
+export
 Profunctor p => Mapping (CofreeMapping p) where
   map' (MkCFM p) = MkCFM (p @{Compose})
   roam = roamCofree
@@ -115,48 +119,51 @@ public export
 data FreeMapping : (p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkFM : Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b
 
-public export
+export
 Profunctor (FreeMapping p) where
   lmap f (MkFM l m r) = MkFM l m (r . f)
   rmap f (MkFM l m r) = MkFM (f . l) m r
   dimap f g (MkFM l m r) = MkFM (g . l) m (r . f)
 
-public export
+export
 ProfunctorFunctor FreeMapping where
   promap f (MkFM l m r) = MkFM l (f m) r
 
-public export
+export
 ProfunctorMonad FreeMapping where
-  propure p = MkFM @{FunctorId} id p id
+  propure p = MkFM runIdentity p Id
   projoin (MkFM l' (MkFM l m r) r') = MkFM @{Compose} (l' . map l) m (map r . r')
 
-public export
+export
 Functor (FreeMapping p a) where
   map = rmap
 
-public export
+export
 GenStrong Pair (FreeMapping p) where
   strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
   strongl = dimap swap' swap' . strongr {p=FreeMapping p}
 
-public export
+export
 GenStrong Either (FreeMapping p) where
   strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
   strongl = dimap swap' swap' . strongr {p=FreeMapping p}
 
-public export
+export
 Closed (FreeMapping p) where
   closed (MkFM l m r) = dimap Mor applyMor $ MkFM @{Compose} (map l) m (map r)
 
 roamFree : ((a -> b) -> s -> t) -> FreeMapping p a b -> FreeMapping p s t
 roamFree f (MkFM l m r) = MkFM @{Compose @{functor}} (($ id) . map @{functor} l) m (map @{functor} r . flip f)
+  where
+    functor : Functor (\a => (a -> b) -> t)
+    functor = MkFunctor (\f => (. (. f)))
 
-public export
+export
 Traversing (FreeMapping p) where
   traverse' (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
-  wander f = roamFree $ f @{ApplicativeId}
+  wander f = roamFree $ (runIdentity .) . f . (Id .)
 
-public export
+export
 Mapping (FreeMapping p) where
   map' (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
   roam = roamFree

Data/Profunctor/Representable.idr

@@ -1,6 +1,5 @@
 module Data.Profunctor.Representable
 
-import Control.Applicative.Const
 import Control.Monad.Identity
 import Data.Morphisms
 import Data.Profunctor
@@ -21,7 +20,7 @@ interface (Sieve p f, Strong p) => Representable p f | p where
   tabulate : (a -> f b) -> p a b
 
 
-||| A profunctor `p` is corepresentable if it is isomorphic to `Costar f` for some `f`.
+||| A profunctor `p` is representable if it is isomorphic to `Costar f` for some `f`.
 public export
 interface Cosieve p f => Corepresentable p f | p where
   cotabulate : (f a -> b) -> p a b
@@ -50,9 +49,9 @@ Representable Morphism Identity where
 ||| A named implementation of `Representable` for function types.
 ||| Use this to avoid having to use a type wrapper like `Morphism`.
 export
-[Function] Representable (\a,b => a -> b) Prelude.id
+[Function] Representable (\a,b => a -> b) Identity
     using Sieve.Function Strong.Function where
-  tabulate = id
+  tabulate = (runIdentity .)
 
 export
 Functor f => Representable (Kleislimorphism f) f where
@@ -62,25 +61,9 @@ export
 Functor f => Representable (Star f) f where
   tabulate = MkStar
 
-export
-Representable (Forget r) (Const r) where
-  tabulate = MkForget . (runConst .)
-
-export
-Corepresentable Morphism Identity where
-  cotabulate f = Mor (f . Id)
-
-namespace Corepresentable
-  ||| A named implementation of `Corepresentable` for function types.
-  ||| Use this to avoid having to use a type wrapper like `Morphism`.
-  export
-  [Function] Corepresentable (\a,b => a -> b) Prelude.id using Cosieve.Function where
-    cotabulate = id
 
 export
 Functor f => Corepresentable (Costar f) f where
   cotabulate = MkCostar
 
-export
-Corepresentable (Coforget r) (Const r) where
-  cotabulate = MkCoforget . (. MkConst)
+

Data/Profunctor/Sieve.idr

@@ -1,6 +1,5 @@
 module Data.Profunctor.Sieve
 
-import Control.Applicative.Const
 import Control.Monad.Identity
 import Data.Morphisms
 import Data.Profunctor
@@ -30,44 +29,37 @@ interface (Profunctor p, Functor f) => Cosieve p f | p where
 ------------------------------------------------------------------------------
 
 
-public export
+export
 Sieve Morphism Identity where
   sieve (Mor f) = Id . f
 
 ||| A named implementation of `Sieve` for function types.
 ||| Use this to avoid having to use a type wrapper like `Morphism`.
-public export
-[Function] Sieve (\a,b => a -> b) Prelude.id using Profunctor.Function FunctorId where
-  sieve = id
+export
+[Function] Sieve (\a,b => a -> b) Identity using Profunctor.Function where
+  sieve = (Id .)
 
-public export
+export
 Functor f => Sieve (Kleislimorphism f) f where
   sieve = applyKleisli
 
-public export
+export
 Functor f => Sieve (Star f) f where
   sieve = applyStar
 
-public export
-Sieve (Forget r) (Const r) where
-  sieve (MkForget k) = MkConst . k
 
 
-public export
+export
 Cosieve Morphism Identity where
   cosieve (Mor f) = f . runIdentity
 
 namespace Cosieve
   ||| A named implementation of `Cosieve` for function types.
   ||| Use this to avoid having to use a type wrapper like `Morphism`.
-  public export
-  [Function] Cosieve (\a,b => a -> b) Prelude.id using Profunctor.Function FunctorId where
-    cosieve = id
+  export
+  [Function] Cosieve (\a,b => a -> b) Identity using Profunctor.Function where
+    cosieve = (. runIdentity)
 
-public export
+export
 Functor f => Cosieve (Costar f) f where
   cosieve = applyCostar
-
-public export
-Cosieve (Coforget r) (Const r) where
-  cosieve (MkCoforget k) = k . runConst

Data/Profunctor/Strong.idr

@@ -80,73 +80,58 @@ right : Choice p => p a b -> p (Either c a) (Either c b)
 right = strongr {ten=Either}
 
 
-public export
+export
 uncurry' : Strong p => p a (b -> c) -> p (a, b) c
 uncurry' = rmap (uncurry id) . first
 
-public export
+export
 strong : Strong p => (a -> b -> c) -> p a b -> p a c
 strong f = dimap dup (uncurry $ flip f) . first
 
 
 ------------------------------------------------------------------------------
--- Implementations
+-- Implementations for existing types
 ------------------------------------------------------------------------------
 
 
-public export
+export
 Bifunctor ten => GenStrong ten Morphism where
   strongl (Mor f) = Mor (mapFst f)
   strongr (Mor f) = Mor (mapSnd f)
 
 ||| A named implementation of `GenStrong` for function types.
 ||| Use this to avoid having to use a type wrapper like `Morphism`.
-public export
+export
 [Function] Bifunctor ten => GenStrong ten (\a,b => a -> b)
     using Profunctor.Function where
   strongl = mapFst
   strongr = mapSnd
 
-public export
+export
 Functor f => GenStrong Pair (Kleislimorphism f) where
   strongl (Kleisli f) = Kleisli $ \(a,c) => (,c) <$> f a
   strongr (Kleisli f) = Kleisli $ \(c,a) => (c,) <$> f a
 
-public export
+export
 Applicative f => GenStrong Either (Kleislimorphism f) where
   strongl (Kleisli f) = Kleisli $ either (map Left . f) (pure . Right)
   strongr (Kleisli f) = Kleisli $ either (pure . Left) (map Right . f)
 
-public export
+export
 Functor f => GenStrong Pair (Star f) where
   strongl (MkStar f) = MkStar $ \(a,c) => (,c) <$> f a
   strongr (MkStar f) = MkStar $ \(c,a) => (c,) <$> f a
 
-public export
+export
 Applicative f => GenStrong Either (Star f) where
   strongl (MkStar f) = MkStar $ either (map Left . f) (pure . Right)
   strongr (MkStar f) = MkStar $ either (pure . Left) (map Right . f)
 
-public export
+export
 GenStrong Either Tagged where
   strongl (Tag x) = Tag (Left x)
   strongr (Tag x) = Tag (Right x)
 
-public export
-GenStrong Pair (Forget r) where
-  strongl (MkForget k) = MkForget (k . fst)
-  strongr (MkForget k) = MkForget (k . snd)
-
-public export
-Monoid r => GenStrong Either (Forget r) where
-  strongl (MkForget k) = MkForget (either k (const neutral))
-  strongr (MkForget k) = MkForget (either (const neutral) k)
-
-public export
-GenStrong Either (Coforget r) where
-  strongl (MkCoforget k) = MkCoforget (Left . k)
-  strongr (MkCoforget k) = MkCoforget (Right . k)
-
 
 ------------------------------------------------------------------------------
 -- Tambara
@@ -160,26 +145,26 @@ record GenTambara (ten, p : Type -> Type -> Type) a b where
   constructor MkTambara
   runTambara : forall c. p (a `ten` c) (b `ten` c)
 
-public export
+export
 Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p) where
   dimap f g (MkTambara p) = MkTambara $ dimap (mapFst f) (mapFst g) p
 
-public export
+export
 ProfunctorFunctor (GenTambara ten) where
   promap f (MkTambara p) = MkTambara (f p)
 
-public export
+export
 Tensor ten i => ProfunctorComonad (GenTambara ten) where
   proextract (MkTambara p) = dimap unitr.rightToLeft unitr.leftToRight p
   produplicate (MkTambara p) = MkTambara $ MkTambara $ dimap assocr assocl p
 
-public export
+export
 Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p) where
   strongl (MkTambara p) = MkTambara $ dimap assocr assocl p
   strongr (MkTambara p) = MkTambara $ dimap (assocr . mapFst swap')
                                             (mapFst swap' . assocl) p
 
-public export
+export
 Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where
   map = rmap
 
@@ -201,11 +186,11 @@ TambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
 TambaraSum = GenTambara Either
 
 
-public export
+export
 tambara : GenStrong ten p => p :-> q -> p :-> GenTambara ten q
 tambara @{gs} f x = MkTambara $ f $ strongl @{gs} x
 
-public export
+export
 untambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q
 untambara f x = dimap unitr.rightToLeft unitr.leftToRight $ runTambara $ f x
 
@@ -222,17 +207,17 @@ data GenPastro : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkPastro : (y `ten` z -> b) -> p x y -> (a -> x `ten` z) -> GenPastro ten p a b
 
 
-public export
+export
 Profunctor (GenPastro ten p) where
   dimap f g (MkPastro l m r) = MkPastro (g . l) m (r . f)
   lmap f (MkPastro l m r) = MkPastro l m (r . f)
   rmap g (MkPastro l m r) = MkPastro (g . l) m r
 
-public export
+export
 ProfunctorFunctor (GenPastro ten) where
   promap f (MkPastro l m r) = MkPastro l (f m) r
 
-public export
+export
 (Tensor ten i, Symmetric ten) => ProfunctorMonad (GenPastro ten) where
   propure x = MkPastro unitr.leftToRight x unitr.rightToLeft
   projoin (MkPastro {x=x',y=y',z=z'} l' (MkPastro {x,y,z} l m r) r') = MkPastro ll m rr
@@ -243,12 +228,12 @@ public export
       rr : a -> x `ten` (z' `ten` z)
       rr = mapSnd swap' . assocr . mapFst r . r'
 
-public export
+export
 ProfunctorAdjunction (GenPastro ten) (GenTambara ten) where
   prounit x = MkTambara (MkPastro id x id)
   procounit (MkPastro l (MkTambara x) r) = dimap r l x
 
-public export
+export
 (Associative ten, Symmetric ten) => GenStrong ten (GenPastro ten p) where
   strongl (MkPastro {x,y,z} l m r) = MkPastro l' m r'
     where
@@ -281,11 +266,11 @@ PastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
 PastroSum = GenPastro Either
 
 
-public export
+export
 pastro : GenStrong ten q => p :-> q -> GenPastro ten p :-> q
 pastro @{gs} f (MkPastro l m r) = dimap r l (strongl @{gs} (f m))
 
-public export
+export
 unpastro : Tensor ten i => GenPastro ten p :-> q -> p :-> q
 unpastro f x = f (MkPastro unitr.leftToRight x unitr.rightToLeft)
 

Data/Profunctor/Traversing.idr

@@ -1,6 +1,6 @@
 module Data.Profunctor.Traversing
 
-import Control.Applicative.Const
+import Control.Monad.Identity
 import Data.Morphisms
 import Data.Tensor
 import Data.Profunctor
@@ -8,11 +8,6 @@ import Data.Profunctor
 %default total
 
 
-------------------------------------------------------------------------------
--- Default implementation machinery
-------------------------------------------------------------------------------
-
-
 [FoldablePair] Foldable (Pair c) where
   foldr op init (_, x) = x `op` init
   foldl op init (_, x) = init `op` x
@@ -21,6 +16,14 @@ import Data.Profunctor
 [TraversablePair] Traversable (Pair c) using FoldablePair where
   traverse f (l, r) = (l,) <$> f r
 
+[FoldableIdentity] Foldable Identity where
+  foldr f i (Id x) = f x i
+  foldl f i (Id x) = f i x
+  null _ = False
+
+[TraversableIdentity] Traversable Identity using FoldableIdentity where
+  traverse f (Id x) = map Id (f x)
+
 
 record Bazaar a b t where
   constructor MkBazaar
@@ -45,7 +48,7 @@ Functor (Baz t b) where
 
 
 sold : Baz t a a -> t
-sold m = runBaz @{ApplicativeId} m id
+sold m = runIdentity (runBaz m Id)
 
 Foldable (Baz t b) where
   foldr f i bz = runBaz bz @{appEndo} f i
@@ -57,11 +60,6 @@ Foldable (Baz t b) where
 Traversable (Baz t b) where
   traverse f bz = map (\m => MkBaz (runBazaar m)) $ runBaz bz @{Compose} $ \x => sell <$> f x
 
-public export
-wanderDef : Profunctor p => (forall f. Traversable f => p a b -> p (f a) (f b))
-                         -> (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t
-wanderDef tr f = dimap (\s => MkBaz $ \afb => f afb s) sold . tr
-
 
 ------------------------------------------------------------------------------
 -- Traversing interface
@@ -83,41 +81,31 @@ interface (Strong p, Choice p) => Traversing p where
   traverse' = wander traverse
 
   wander : (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t
-  wander = wanderDef traverse'
+  wander f = dimap (\s => MkBaz $ \afb => f afb s) sold . traverse'
 
 
-------------------------------------------------------------------------------
--- Implementations
-------------------------------------------------------------------------------
-
-
-public export
+export
 Traversing Morphism where
   traverse' (Mor f) = Mor (map f)
-  wander f (Mor p) = Mor (f @{ApplicativeId} p)
+  wander f (Mor p) = Mor (runIdentity . (f $ Id . p))
 
 ||| A named implementation of `Traversing` for function types.
 ||| Use this to avoid having to use a type wrapper like `Morphism`.
-public export
+export
 [Function] Traversing (\a,b => a -> b) using Strong.Function where
   traverse' = map
-  wander f = f @{ApplicativeId}
+  wander f g = runIdentity . (f $ Id . g)
 
-public export
+export
 Applicative f => Traversing (Kleislimorphism f) where
   traverse' (Kleisli p) = Kleisli (traverse p)
   wander f (Kleisli p) = Kleisli (f p)
 
-public export
+export
 Applicative f => Traversing (Star f) where
   traverse' (MkStar p) = MkStar (traverse p)
   wander f (MkStar p) = MkStar (f p)
 
-public export
-Monoid r => Traversing (Forget r) where
-  traverse' (MkForget k) = MkForget (foldMap k)
-  wander f (MkForget k) = MkForget (runConst . f (MkConst . k))
-
 
 ------------------------------------------------------------------------------
 -- CofreeTraversing
@@ -131,45 +119,45 @@ record CofreeTraversing p a b where
   constructor MkCFT
   runCFT : forall f. Traversable f => p (f a) (f b)
 
-public export
+export
 Profunctor p => Profunctor (CofreeTraversing p) where
   lmap f (MkCFT p) = MkCFT (lmap (map f) p)
   rmap g (MkCFT p) = MkCFT (rmap (map g) p)
   dimap f g (MkCFT p) = MkCFT (dimap (map f) (map g) p)
 
-public export
+export
 Profunctor p => GenStrong Pair (CofreeTraversing p) where
   strongr (MkCFT p) = MkCFT (p @{Compose @{%search} @{TraversablePair}})
   strongl = dimap swap' swap' . strongr {p=CofreeTraversing p}
 
-public export
+export
 Profunctor p => GenStrong Either (CofreeTraversing p) where
   strongr (MkCFT p) = MkCFT (p @{Compose {f=Either c}})
   strongl = dimap swap' swap' . strongr {p=CofreeTraversing p}
 
-public export
+export
 Profunctor p => Traversing (CofreeTraversing p) where
   traverse' (MkCFT p) = MkCFT (p @{Compose})
 
-public export
+export
 ProfunctorFunctor CofreeTraversing where
   promap f (MkCFT p) = MkCFT (f p)
 
-public export
+export
 ProfunctorComonad CofreeTraversing where
-  proextract (MkCFT p) = p @{TraversableId}
+  proextract (MkCFT p) = dimap Id runIdentity $ p @{TraversableIdentity}
   produplicate (MkCFT p) = MkCFT $ MkCFT $ p @{Compose}
 
-public export
+export
 Profunctor p => Functor (CofreeTraversing p a) where
   map = rmap
 
 
-public export
+export
 cofreeTraversing : Traversing p => p :-> q -> p :-> CofreeTraversing q
 cofreeTraversing f p = MkCFT $ f $ traverse' p
 
-public export
+export
 uncofreeTraversing : Profunctor q => p :-> CofreeTraversing q -> p :-> q
 uncofreeTraversing f p = proextract $ f p
 
@@ -185,40 +173,40 @@ public export
 data FreeTraversing : (p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkFT : Traversable f => (f y -> b) -> p x y -> (a -> f x) -> FreeTraversing p a b
 
-public export
+export
 Profunctor (FreeTraversing p) where
   lmap f (MkFT l m r) = MkFT l m (r . f)
   rmap f (MkFT l m r) = MkFT (f . l) m r
   dimap f g (MkFT l m r) = MkFT (g . l) m (r . f)
 
-public export
+export
 GenStrong Pair (FreeTraversing p) where
   strongr (MkFT l m r) = MkFT @{Compose @{TraversablePair}} (map l) m (map r)
   strongl = dimap swap' swap' . strongr {p=FreeTraversing p}
 
-public export
+export
 GenStrong Either (FreeTraversing p) where
   strongr (MkFT l m r) = MkFT @{Compose {t=Either c}} (map l) m (map r)
   strongl = dimap swap' swap' . strongr {p=FreeTraversing p}
 
-public export
+export
 Traversing (FreeTraversing p) where
   traverse' (MkFT l m r) = MkFT @{Compose} (map l) m (map r)
 
-public export
+export
 ProfunctorFunctor FreeTraversing where
   promap f (MkFT l m r) = MkFT l (f m) r
 
-public export
+export
 ProfunctorMonad FreeTraversing where
-  propure p = MkFT @{TraversableId} id p id
+  propure p = MkFT @{TraversableIdentity} runIdentity p Id
   projoin (MkFT l' (MkFT l m r) r') = MkFT @{Compose} (l' . map l) m (map r . r')
 
 
-public export
+export
 freeTraversing : Traversing q => p :-> q -> FreeTraversing p :-> q
 freeTraversing fn (MkFT {f} l m r) = dimap r l (traverse' {f} (fn m))
 
-public export
+export
 unfreeTraversing : FreeTraversing p :-> q -> p :-> q
-unfreeTraversing f p = f (MkFT @{TraversableId} id p id)
+unfreeTraversing f p = f (MkFT @{TraversableIdentity} runIdentity p Id)

Data/Profunctor/Types.idr

@@ -59,7 +59,7 @@ p :-> q = forall a, b. p a b -> q a b
 ------------------------------------------------------------------------------
 
 
-public export
+export
 Profunctor Morphism where
   dimap f g (Mor h) = Mor (g . h . f)
   lmap f (Mor g) = Mor (g . f)
@@ -68,13 +68,13 @@ Profunctor Morphism where
 namespace Profunctor
   ||| A named implementation of `Profunctor` for function types.
   ||| Use this to avoid having to use a type wrapper like `Morphism`.
-  public export
+  export
   [Function] Profunctor (\a,b => a -> b) where
     dimap f g h = g . h . f
     lmap = flip (.)
     rmap = (.)
 
-public export
+export
 Functor f => Profunctor (Kleislimorphism f) where
   dimap f g (Kleisli h) = Kleisli (map g . h . f)
   lmap f (Kleisli g) = Kleisli (g . f)
@@ -82,7 +82,7 @@ Functor f => Profunctor (Kleislimorphism f) where
 
 
 ------------------------------------------------------------------------------
--- New profunctor types
+-- Implementations for existing types
 ------------------------------------------------------------------------------
 
 
@@ -95,27 +95,27 @@ record Star {0 k : Type} (f : k -> Type) a (b : k) where
   constructor MkStar
   applyStar : a -> f b
 
-public export
+export
 Functor f => Functor (Star f a) where
   map f (MkStar g) = MkStar (map f . g)
 
-public export
+export
 Applicative f => Applicative (Star f a) where
   pure = MkStar . const . pure
   MkStar f <*> MkStar g = MkStar (\x => f x <*> g x)
 
-public export
+export
 Monad f => Monad (Star f a) where
   MkStar f >>= g = MkStar $ \x => do
     a <- f x
     applyStar (g a) x
 
-public export
+export
 Contravariant f => Contravariant (Star f a) where
   contramap f (MkStar g) = MkStar (contramap f . g)
 
 
-public export
+export
 Functor f => Profunctor (Star f) where
   dimap f g (MkStar h) = MkStar (map g . h . f)
   lmap f (MkStar g) = MkStar (g . f)
@@ -128,20 +128,20 @@ record Costar {0 k : Type} (f : k -> Type) (a : k) b where
   constructor MkCostar
   applyCostar : f a -> b
 
-public export
+export
 Functor (Costar f a) where
   map f (MkCostar g) = MkCostar (f . g)
 
-public export
+export
 Applicative (Costar f a) where
   pure = MkCostar . const
   MkCostar f <*> MkCostar g = MkCostar (\x => f x (g x))
 
-public export
+export
 Monad (Costar f a) where
   MkCostar f >>= g = MkCostar (\x => applyCostar (g (f x)) x)
 
-public export
+export
 Functor f => Profunctor (Costar f) where
   dimap f g (MkCostar h) = MkCostar (g . h . map f)
   lmap f (MkCostar g) = MkCostar (g . map f)
@@ -160,21 +160,21 @@ public export
 retag : Tagged a c -> Tagged b c
 retag (Tag x) = Tag x
 
-public export
+export
 Functor (Tagged a) where
   map f (Tag x) = Tag (f x)
 
-public export
+export
 Applicative (Tagged a) where
   pure = Tag
   Tag f <*> Tag x = Tag (f x)
 
-public export
+export
 Monad (Tagged a) where
   join = runTagged
   Tag x >>= f = f x
 
-public export
+export
 Foldable (Tagged a) where
   foldr f x (Tag y) = f y x
   foldl f x (Tag y) = f x y
@@ -183,130 +183,12 @@ Foldable (Tagged a) where
   toList (Tag x) = [x]
   foldMap f (Tag x) = f x
 
-public export
+export
 Traversable (Tagged a) where
   traverse f (Tag x) = map Tag (f x)
 
-public export
+export
 Profunctor Tagged where
   dimap _ f (Tag x) = Tag (f x)
   lmap = const retag
   rmap f (Tag x) = Tag (f x)
-
-
-||| `Forget r` is equivalent to `Star (Const r)`.
-public export
-record Forget {0 k : Type} r a (b : k) where
-  constructor MkForget
-  runForget : a -> r
-
-public export
-reforget : Forget r a b -> Forget r a c
-reforget (MkForget k) = MkForget k
-
-public export
-Functor (Forget r a) where
-  map _ = reforget
-
-public export
-Contravariant (Forget {k=Type} r a) where
-  contramap _ = reforget
-
-public export
-Monoid r => Applicative (Forget r a) where
-  pure _ = MkForget (const neutral)
-  MkForget f <*> MkForget g = MkForget (f <+> g)
-
-public export
-Monoid r => Monad (Forget {k=Type} r a) where
-  join = reforget
-  (>>=) = reforget .: const
-
-public export
-Foldable (Forget r a) where
-  foldr _ x _ = x
-  foldl _ x _ = x
-  null = const True
-  foldlM _ x _ = pure x
-  toList _ = []
-  foldMap _ _ = neutral
-
-public export
-Traversable (Forget r a) where
-  traverse _ = pure . reforget
-
-public export
-Profunctor (Forget r) where
-  dimap f _ (MkForget k) = MkForget (k . f)
-  lmap f (MkForget k) = MkForget (k . f)
-  rmap = map
-
-
-||| `Coforget r` is equivalent to `Costar (Const r)`.
-public export
-record Coforget {0 k : Type} r (a : k) b where
-  constructor MkCoforget
-  runCoforget : r -> b
-
-public export
-recoforget : Coforget r a c -> Coforget r b c
-recoforget (MkCoforget k) = MkCoforget k
-
-public export
-Functor (Coforget r a) where
-  map f (MkCoforget k) = MkCoforget (f . k)
-
-public export
-Bifunctor (Coforget r) where
-  bimap _ f (MkCoforget k) = MkCoforget (f . k)
-  mapFst _ = recoforget
-  mapSnd = map
-
-public export
-Applicative (Coforget r a) where
-  pure = MkCoforget . const
-  MkCoforget f <*> MkCoforget g = MkCoforget (\r => f r (g r))
-
-public export
-Monad (Coforget r a) where
-  MkCoforget k >>= f = MkCoforget (\r => runCoforget (f $ k r) r)
-
-public export
-Profunctor (Coforget r) where
-  dimap _ f (MkCoforget k) = MkCoforget (f . k)
-  lmap _ = recoforget
-  rmap = map
-
-
-------------------------------------------------------------------------------
--- Identity functor
-------------------------------------------------------------------------------
-
--- A few convenience definitions for use in other modules.
-
-public export
-[FunctorId] Functor Prelude.id where
-  map = id
-
-public export
-[ApplicativeId] Applicative Prelude.id using FunctorId where
-  pure = id
-  (<*>) = id
-
-public export
-[MonadId] Monad Prelude.id using ApplicativeId where
-  join = id
-  (>>=) = flip id
-
-public export
-[FoldableId] Foldable Prelude.id where
-  foldr = flip
-  foldl = id
-  null _ = False
-  foldlM = id
-  toList = pure
-  foldMap = id
-
-public export
-[TraversableId] Traversable Prelude.id using FunctorId FoldableId where
-  traverse = id

Data/Profunctor/Yoneda.idr

@@ -20,69 +20,69 @@ record Yoneda p a b where
   constructor MkYoneda
   runYoneda : forall x, y. (x -> a) -> (b -> y) -> p x y
 
-public export
+export
 Profunctor (Yoneda p) where
   lmap f (MkYoneda p) = MkYoneda $ \l,r => p (f . l) r
   rmap f (MkYoneda p) = MkYoneda $ \l,r => p l (r . f)
   dimap f g (MkYoneda p) = MkYoneda $ \l,r => p (f . l) (r . g)
 
-public export
+export
 ProfunctorFunctor Yoneda where
   promap f (MkYoneda p) = MkYoneda $ f .: p
 
-public export
+export
 ProfunctorMonad Yoneda where
   propure p = MkYoneda $ \l,r => dimap l r p
   projoin (MkYoneda p) = p id id
 
-public export
+export
 ProfunctorComonad Yoneda where
   proextract (MkYoneda p) = p id id
   produplicate p = MkYoneda $ \l,r => dimap l r p
 
 ||| A witness that `Yoneda p` and `p` are equivalent when `p` is a profunctor.
-public export
+export
 yonedaEqv : Profunctor p => p a b <=> Yoneda p a b
 yonedaEqv = MkEquivalence propure proextract
 
-public export
+export
 yonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p =>
               p (q a b) (r a' b') -> p (Yoneda q a b) (Yoneda r a' b')
 yonedaIso = dimap proextract propure
 
-public export
+export
 Functor (Yoneda p a) where
   map = rmap
 
-public export
+export
 GenStrong ten p => GenStrong ten (Yoneda p) where
   strongl = propure . strongl {ten,p} . proextract
   strongr = propure . strongr {ten,p} . proextract
 
-public export
+export
 GenCostrong ten p => GenCostrong ten (Yoneda p) where
   costrongl = propure . costrongl {ten,p} . proextract
   costrongr = propure . costrongr {ten,p} . proextract
 
-public export
+export
 Closed p => Closed (Yoneda p) where
   closed = propure . closed . proextract
 
-public export
+export
 Traversing p => Traversing (Yoneda p) where
   traverse' = propure . traverse' . proextract
   wander f = propure . wander f . proextract
 
-public export
+export
 Mapping p => Mapping (Yoneda p) where
   map' = propure . map' . proextract
   roam f = propure . roam f . proextract
 
-public export
+export
 Sieve p f => Sieve (Yoneda p) f where
   sieve = sieve . proextract
 
-public export
+export
 Cosieve p f => Cosieve (Yoneda p) f where
   cosieve = cosieve . proextract
 
@@ -98,68 +98,68 @@ data Coyoneda : (p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkCoyoneda : (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b
 
 
-public export
+export
 Profunctor (Coyoneda p) where
   lmap f (MkCoyoneda l r p) = MkCoyoneda (l . f) r p
   rmap f (MkCoyoneda l r p) = MkCoyoneda l (f . r) p
   dimap f g (MkCoyoneda l r p) = MkCoyoneda (l . f) (g . r) p
 
-public export
+export
 ProfunctorFunctor Coyoneda where
   promap f (MkCoyoneda l r p) = MkCoyoneda l r (f p)
 
-public export
+export
 ProfunctorMonad Coyoneda where
   propure = MkCoyoneda id id
   projoin (MkCoyoneda l r p) = dimap l r p
 
-public export
+export
 ProfunctorComonad Coyoneda where
   proextract (MkCoyoneda l r p) = dimap l r p
   produplicate = MkCoyoneda id id
 
 ||| A witness that `Coyoneda p` and `p` are equivalent when `p` is a profunctor.
-public export
+export
 coyonedaEqv : Profunctor p => p a b <=> Coyoneda p a b
 coyonedaEqv = MkEquivalence propure proextract
 
-public export
+export
 coyonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p =>
               p (q a b) (r a' b') -> p (Coyoneda q a b) (Coyoneda r a' b')
 coyonedaIso = dimap proextract propure
 
-public export
+export
 Functor (Coyoneda p a) where
   map = rmap
 
-public export
+export
 GenStrong ten p => GenStrong ten (Coyoneda p) where
   strongl = propure . strongl {ten,p} . proextract
   strongr = propure . strongr {ten,p} . proextract
 
-public export
+export
 GenCostrong ten p => GenCostrong ten (Coyoneda p) where
   costrongl = propure . costrongl {ten,p} . proextract
   costrongr = propure . costrongr {ten,p} . proextract
 
-public export
+export
 Closed p => Closed (Coyoneda p) where
   closed = propure . closed . proextract
 
-public export
+export
 Traversing p => Traversing (Coyoneda p) where
   traverse' = propure . traverse' . proextract
   wander f = propure . wander f . proextract
 
-public export
+export
 Mapping p => Mapping (Coyoneda p) where
   map' = propure . map' . proextract
   roam f = propure . roam f . proextract
 
-public export
+export
 Sieve p f => Sieve (Coyoneda p) f where
   sieve = sieve . proextract
 
-public export
+export
 Cosieve p f => Cosieve (Coyoneda p) f where
   cosieve = cosieve . proextract

Data/Tensor.idr

@@ -58,16 +58,16 @@ interface Associative ten => Tensor ten i | ten where
 ------------------------------------------------------------------------------
 
 
-public export
+export
 Associative Pair where
   assocl (x,(y,z)) = ((x,y),z)
   assocr ((x,y),z) = (x,(y,z))
 
-public export
+export
 Symmetric Pair where
   swap' = swap
 
-public export
+export
 Tensor Pair () where
   unitl = MkEquivalence snd ((),)
   unitr = MkEquivalence fst (,())
@@ -78,7 +78,7 @@ Tensor Pair () where
 ------------------------------------------------------------------------------
 
 
-public export
+export
 Associative Either where
   assocl (Left x) = Left (Left x)
   assocl (Right (Left x)) = Left (Right x)
@@ -88,11 +88,11 @@ Associative Either where
   assocr (Left (Right x)) = Right (Left x)
   assocr (Right x) = Right (Right x)
 
-public export
+export
 Symmetric Either where
   swap' = either Right Left
 
-public export
+export
 Tensor Either Void where
   unitl = MkEquivalence (either absurd id) Right
   unitr = MkEquivalence (either id absurd) Left

profunctors.ipkg

@@ -1,7 +1,5 @@
 package profunctors
-version = 1.1.2
-
-brief = "Profunctors for Idris2"
+version = 1.0.0
 
 authors = "Kiana Sheibani"
 license = "MIT"