diff --git a/.gitignore b/.gitignore
index c28bc7c..f33345a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,4 @@
 *.ibc
 *.o
+target/
+elba.lock
\ No newline at end of file
diff --git a/README.md b/README.md
index e52efd1..57f08a3 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
-Idris Profunctors
-=================
+Idris2 Profunctors
+==================
 
-This is a profunctor library for idris based off the excellent [Haskell Profunctors](https://github.com/ekmett/profunctors) package from Edward Kmett.  Contributions, bug reports, and feature requests are welcome.
+This is a profunctor library for Idris2 based off the excellent [Haskell Profunctors](https://github.com/ekmett/profunctors) package from Edward Kmett.  Contributions, bug reports, and feature requests are welcome.
 
 Contains
 --------
@@ -16,9 +16,14 @@ Contains
 
   * Prisms
 
+Misses
+------
+
+  * Proofs for algebraic properties of Folds.
+
 Installation
 ------------
 
-Run `idris --install profunctors.ipkg` from inside this directory, and then if
+Run `idris2 --install profunctors.ipkg` from inside this directory, and then if
 you want to use it with anything, invoke idris with `-p profunctors` (i.e.
-`idris -p profunctors hack_the_planet.idr`)
+`idris2 -p profunctors hack_the_planet.idr`)
diff --git a/elba.toml b/elba.toml
new file mode 100644
index 0000000..8eb955a
--- /dev/null
+++ b/elba.toml
@@ -0,0 +1,27 @@
+[package]
+name = "japesinator/Idris-Profunctors"
+version = "0.1.0"
+authors = []
+
+[dependencies]
+"japesinator/Idris-Bifunctors" = { git = "https://github.com/andrevidela/Idris-Bifunctors" }
+
+[targets.lib]
+path = "src"
+name = "profunctors"
+mods = [ "Data.Profunctor"
+       , "Data.Profunctor.Cayley"
+       , "Data.Profunctor.Closed"
+       , "Data.Profunctor.Codensity"
+       , "Data.Profunctor.Composition"
+       , "Data.Profunctor.Fold"
+       , "Data.Profunctor.Iso"
+       , "Data.Profunctor.Lens"
+       , "Data.Profunctor.Lens.At"
+       , "Data.Profunctor.Prism"
+       , "Data.Profunctor.Trace"
+       , "Data.Profunctor.Traversal"
+       , "Data.Profunctor.Traversal.Index"
+       , "Data.Verified.Profunctor"
+       ]
+idris_opts = ["-p", "contrib"]
diff --git a/profunctors.ipkg b/profunctors.ipkg
index 20992d3..fbf7c8f 100644
--- a/profunctors.ipkg
+++ b/profunctors.ipkg
@@ -1,17 +1,33 @@
 package profunctors
 
-sourcedir = src
+sourcedir = "src"
 
 modules = Data.Profunctor
         , Data.Profunctor.Cayley
+        , Data.Profunctor.Choice
         , Data.Profunctor.Closed
         , Data.Profunctor.Codensity
         , Data.Profunctor.Composition
+        , Data.Profunctor.Comonad
         , Data.Profunctor.Fold
+        , Data.Profunctor.Grate
         , Data.Profunctor.Iso
         , Data.Profunctor.Lens
+        , Data.Profunctor.Lens.At
+        , Data.Profunctor.Monad
         , Data.Profunctor.Prism
+        , Data.Profunctor.Ran
+        , Data.Profunctor.Rep
+        , Data.Profunctor.Sieve
+        , Data.Profunctor.Strong
         , Data.Profunctor.Trace
+        , Data.Profunctor.Traversal
+        , Data.Profunctor.Traversal.Index
+        , Data.Profunctor.Unsafe
+        , Data.Profunctor.Wander
+        , Data.Proxy
         , Data.Verified.Profunctor
 
-opts = "-p contrib"
+depends = comonad
+
+opts = "-p contrib comonad"
diff --git a/src/Data/Profunctor.idr b/src/Data/Profunctor.idr
index a999c7b..5b44c70 100644
--- a/src/Data/Profunctor.idr
+++ b/src/Data/Profunctor.idr
@@ -1,14 +1,18 @@
 module Data.Profunctor
 
+import Control.Monad.Identity
 import Control.Arrow
 import Control.Category
+import Control.Comonad
+import Data.Either
 import Data.Morphisms
 
-%access public export
+%default total
 
 ||| Profunctors
 ||| @p The action of the Profunctor on pairs of objects
-interface Profunctor (p : Type -> Type -> Type) where
+public export
+interface Profunctor (0 p : Type -> Type -> Type) where
   ||| Map over both arguments
   |||
   ||| ````idris example
@@ -36,48 +40,34 @@ interface Profunctor (p : Type -> Type -> Type) where
   rmap : (a -> b) -> p c a -> p c b
   rmap = dimap id
 
+export
 implementation Monad m => Profunctor (Kleislimorphism m) where
-  dimap f g (Kleisli h) = Kleisli $ liftA g . h . f
+  dimap f g (Kleisli h) = Kleisli $ map g . h . f
 
-||| An injective (->)
-|||
-||| ````idris example
-||| believe_me : Arr a b
-||| ````
-|||
-record Arr a b where
-  constructor MkArr
-  runArr : (a -> b)
-
-implementation Category Arr where
-  id  = assert_total id
-  (.) = assert_total (.)
-
-implementation Arrow Arr where
-  arrow                   = MkArr
-  first                   = MkArr . (\f,(a,b) => (f a,b)) . runArr
-  second                  = MkArr . (\f,(a,b) => (a,f b)) . runArr
-  (MkArr f) *** (MkArr g) = MkArr $ \(a,b) => (f a, g b)
-  (MkArr f) &&& (MkArr g) = MkArr $ \a => (f a, g a)
-
-implementation Profunctor Arr where
-  dimap f g (MkArr h) = MkArr $ g . h . f
-
-implementation Functor (Arr a) where
-  map = rmap
+export
+implementation Profunctor Morphism where
+  dimap f g (Mor h) = Mor $ g . h . f
 
 ||| A method of attaching a phantom type as a "tag"
+public export
 record Tagged a b where
   constructor Tag
   runTagged : b
 
+export
 implementation Profunctor Tagged where
   lmap   = const $ Tag . runTagged
   rmap f = Tag . f . runTagged
 
+export
 implementation Functor (Tagged a) where
   map = rmap
 
+export
+implementation Comonad (Tagged a) where
+  duplicate = Tag
+  extract = runTagged
+
 -- UpStar
 -- {{{
 
@@ -87,20 +77,30 @@ implementation Functor (Tagged a) where
 ||| UpStar $ \x => Just $ isDigit x
 ||| ````
 |||
+public export
 record UpStarred (f : Type -> Type) d c where
   constructor UpStar
   runUpStar : d -> f c
 
+export
 implementation Functor f => Profunctor (UpStarred f) where
-  dimap ab cd (UpStar bfc) = UpStar $ map cd . bfc . ab
+  dimap ab cd (UpStar bfc) = UpStar $ \a => map cd $ bfc $ ab a
 
+export
 implementation Functor f => Functor (UpStarred f a) where
   map = rmap
 
+export
 implementation Applicative f => Applicative (UpStarred f a) where
   pure                        = UpStar . const . pure
   (UpStar ff) <*> (UpStar fx) = UpStar $ \a => ff a <*> fx a
 
+export
+implementation Alternative f => Alternative (UpStarred f a) where
+  empty = UpStar $ const empty
+  (UpStar fa) <|> (UpStar fb) = UpStar $ \x => (fa x) <|> (fb x)
+
+export
 implementation Monad f => Monad (UpStarred f a) where
   (UpStar m) >>= f = UpStar $ \e => m e >>= flip runUpStar e . f
 
@@ -114,20 +114,25 @@ implementation Monad f => Monad (UpStarred f a) where
 ||| DownStar $ show
 ||| ````
 |||
+public export
 record DownStarred (f : Type -> Type) d c where
   constructor DownStar
   runDownStar : f d -> c
 
+export
 implementation Functor f => Profunctor (DownStarred f) where
   dimap ab cd (DownStar fbc) = DownStar $ cd . fbc . map ab
 
+export
 implementation Functor (DownStarred f a) where
   map = (DownStar .) . (. runDownStar) . (.)
 
+export
 implementation Applicative (DownStarred f a) where
   pure                            = DownStar . const
   (DownStar ff) <*> (DownStar fx) = DownStar $ \a => ff a $ fx a
 
+export
 implementation Monad (DownStarred f a) where
   (DownStar m) >>= f = DownStar $ \x => runDownStar (f $ m x) x
 
@@ -141,14 +146,17 @@ implementation Monad (DownStarred f a) where
 ||| WrapArrow $ arrow ((+) 1)
 ||| ````
 |||
+public export
 record WrappedArrow (p : Type -> Type -> Type) a b where
   constructor WrapArrow
   unwrapArrow : p a b
 
+export
 implementation Category p => Category (WrappedArrow p) where
   (WrapArrow f) . (WrapArrow g) = WrapArrow $ f . g
   id                            = WrapArrow id
 
+export
 implementation Arrow p => Arrow (WrappedArrow p) where
   arrow                           = WrapArrow . arrow
   first                           = WrapArrow . first  . unwrapArrow
@@ -156,9 +164,10 @@ implementation Arrow p => Arrow (WrappedArrow p) where
   (WrapArrow a) *** (WrapArrow b) = WrapArrow $ a *** b
   (WrapArrow a) &&& (WrapArrow b) = WrapArrow $ a &&& b
 
+export
 implementation Arrow p => Profunctor (WrappedArrow p) where
   lmap = (>>>) . arrow
-  rmap = (.)   . arrow
+  rmap f = (arrow f .)
 
 -- }}}
 -- Forget
@@ -170,110 +179,33 @@ implementation Arrow p => Profunctor (WrappedArrow p) where
 ||| Forget ((+) 1)
 ||| ````
 |||
-record Forgotten r a b where
+public export
+record Forgotten (r : Type) (a : Type) (b : Type) where
   constructor Forget
   runForget : a -> r
 
+export
 implementation Profunctor (Forgotten r) where
   dimap f _ (Forget k) = Forget $ k . f
 
+export
 implementation Functor (Forgotten r a) where
   map = const $ Forget . runForget
 
+export
 implementation Foldable (Forgotten r a) where
   foldr = const const
 
+export
 implementation Traversable (Forgotten r a) where
   traverse = const $ pure . Forget . runForget
 
--- }}}
--- Strong
--- {{{
-
-||| Generalized UpStar of a Strong Functor
-interface Profunctor p => Strong (p : Type -> Type -> Type) where
-  ||| Create a new Profunctor of tuples with first element from the original
-  |||
-  ||| ````idris example
-  ||| first' (Kleisli $ \x => Just $ reverse x)
-  ||| ````
-  |||
-  first'  : p a b -> p (a, c) (b, c)
-  first'  = dimap (\x => (snd x, fst x)) (\x => (snd x, fst x)) . second'
-
-  ||| Create a new Profunctor of tuples with second element from the original
-  |||
-  ||| ````idris example
-  ||| second' (Kleisli $ \x => Just $ reverse x)
-  ||| ````
-  |||
-  second' : p a b -> p (c, a) (c, b)
-  second' = dimap (\x => (snd x, fst x)) (\x => (snd x, fst x)) . first'
-
-implementation Monad m => Strong (Kleislimorphism m) where
-  first'  (Kleisli f) = Kleisli $ \ac => f (fst ac) >>= \b => pure (b, snd ac)
-  second' (Kleisli f) = Kleisli $ \ca => f (snd ca) >>= pure . MkPair (fst ca)
-
-implementation Strong Arr where
-  first'  (MkArr f) = MkArr $ \(a,c) => (f a, c)
-  second' (MkArr f) = MkArr $ \(c,a) => (c, f a)
-
-implementation Functor m => Strong (UpStarred m) where
-  first'  (UpStar f) = UpStar $ \ac => map (\b' => (b', snd ac)) . f $ fst ac
-  second' (UpStar f) = UpStar $ \ca => map (MkPair $    fst ca)  . f $ snd ca
-
-implementation Arrow p => Strong (WrappedArrow p) where
-  first'  = WrapArrow . first  . unwrapArrow
-  second' = WrapArrow . second . unwrapArrow
-
-implementation Strong (Forgotten r) where
-  first'  (Forget k) = Forget $ k . fst
-  second' (Forget k) = Forget $ k . snd
-
--- }}}
--- Choice
--- {{{
-
-||| Generalized DownStar of a Costrong Functor
-interface Profunctor p => Choice (p : Type -> Type -> Type) where
-  ||| Like first' but with sum rather than product types
-  |||
-  ||| ````idris example
-  ||| left' (Kleisli $ \x => Just $ reverse x)
-  ||| ````
-  |||
-  left' : p a b -> p (Either a c) (Either b c)
-  left' = dimap mirror mirror . right'
-
-  ||| Like second' but with sum rather than product types
-  |||
-  ||| ````idris example
-  ||| right' (Kleisli $ \x => Just $ reverse x)
-  ||| ````
-  |||
-  right' : p a b -> p (Either c a) (Either c b)
-  right' = dimap mirror mirror . left'
-
-implementation Monad m => Choice (Kleislimorphism m) where
-  left'  f = Kleisli $ either (applyKleisli $ f        >>> arrow Left)
-                              (applyKleisli $ arrow id >>> arrow Right)
-  right' f = Kleisli $ either (applyKleisli $ arrow id >>> arrow Left)
-                              (applyKleisli $ f        >>> arrow Right)
-
-implementation Choice Arr where
-  left'  (MkArr f) = MkArr $ either (Left . f) Right
-  right' (MkArr f) = MkArr $ either Left (Right . f)
-
-implementation Choice Tagged where
-  left'  = Tag . Left  . runTagged
-  right' = Tag . Right . runTagged
-
-implementation Applicative f => Choice (UpStarred f) where
-  left'  (UpStar f) = UpStar $ either (map Left . f   ) (map Right . pure)
-  right' (UpStar f) = UpStar $ either (map Left . pure) (map Right . f   )
-
-implementation Monoid r => Choice (Forgotten r) where
-  left'  (Forget k) = Forget .      either k $ const neutral
-  right' (Forget k) = Forget . flip either k $ const neutral
+public export
+record Zipping a b where
+  constructor MkZipping
+  runZipping : a -> a -> b
 
+export
+implementation Profunctor Zipping where
+  dimap f g (MkZipping h) = MkZipping $ \a1, a2 => g $ h (f a1) (f a2)
 -- }}}
diff --git a/src/Data/Profunctor/Cayley.idr b/src/Data/Profunctor/Cayley.idr
index 432703c..2cf1cb3 100644
--- a/src/Data/Profunctor/Cayley.idr
+++ b/src/Data/Profunctor/Cayley.idr
@@ -3,58 +3,69 @@ module Data.Profunctor.Cayley
 import Control.Arrow
 import Control.Category
 import Data.Profunctor
+import Data.Profunctor.Strong
+import Data.Profunctor.Choice
 import Data.Profunctor.Unsafe
 
-%access public export
-
 ||| Converts Monads on standard types to Monads on Profunctors
+||| ````idris example
+||| Cayley $ Just $ Kleisli $ \x => Just $ reverse x
+||| ````
+public export
 record Cayleyed (f : Type -> Type) (p : Type -> Type -> Type) a b where
-  ||| ````idris example
-  ||| Cayley $ Just $ Kleisli $ \x => Just $ reverse x
-  ||| ````
   constructor Cayley
   runCayley : f (p a b)
 
+export
 implementation (Functor f, Profunctor p) => Profunctor (Cayleyed f p) where
   dimap f g = Cayley . map (dimap f g) . runCayley
   lmap  f   = Cayley . map (lmap  f  ) . runCayley
   rmap    g = Cayley . map (rmap    g) . runCayley
 
+export
 implementation (UnsafeProfunctor p, Functor f) =>
          UnsafeProfunctor (Cayleyed f p) where
   w          #. (Cayley p) = Cayley $ map (w #.) p
   (Cayley p) .# w          = Cayley $ map (.# w) p
 
+export
 implementation (Functor f, Strong p) => Strong (Cayleyed f p) where
   first'  = Cayley . map first'  . runCayley
   second' = Cayley . map second' . runCayley
 
+export
 implementation (Functor f, Choice p) => Choice (Cayleyed f p) where
   left'  = Cayley . map left'  . runCayley
   right' = Cayley . map right' . runCayley
 
+export
 implementation (Applicative f, Category p) => Category (Cayleyed f p) where
   id                            = Cayley $ pure id
-  (Cayley fpbc) . (Cayley fpab) = Cayley $ liftA2 (.) fpbc fpab
+  (Cayley fpbc) . (Cayley fpab) = Cayley $ (.) <$> fpbc <*> fpab
 
+export
 implementation (Applicative f, Arrow p) => Arrow (Cayleyed f p) where
   arrow                       = Cayley . pure . arrow
   first                       = Cayley . map first  . runCayley
   second                      = Cayley . map second . runCayley
-  (Cayley ab) *** (Cayley cd) = Cayley $ liftA2 (***) ab cd
-  (Cayley ab) &&& (Cayley ac) = Cayley $ liftA2 (&&&) ab ac
+  (Cayley ab) *** (Cayley cd) = Cayley $ (***) <$> ab <*> cd
+  (Cayley ab) &&& (Cayley ac) = Cayley $ (&&&) <$> ab <*> ac
 
+export
 implementation (Applicative f, ArrowChoice p) => ArrowChoice (Cayleyed f p) where
   left                        = Cayley . map left . runCayley
   right                       = Cayley . map right . runCayley
-  (Cayley ab) +++ (Cayley cd) = Cayley $ liftA2 (+++) ab cd
-  (Cayley ac) \|/ (Cayley bc) = Cayley $ liftA2 (\|/) ac bc
+  (Cayley ab) +++ (Cayley cd) = Cayley $ (+++) <$> ab <*> cd
+  (Cayley ac) \|/ (Cayley bc) = Cayley $ (\|/) <$> ac <*> bc
 
+export
 implementation (Applicative f, ArrowLoop p) => ArrowLoop (Cayleyed f p) where
   loop = Cayley . map loop . runCayley
 
+export
 implementation (Applicative f, ArrowZero p) => ArrowZero (Cayleyed f p) where
   zeroArrow = Cayley $ pure zeroArrow
 
+export
 implementation (Applicative f, ArrowPlus p) => ArrowPlus (Cayleyed f p) where
-  (Cayley f) <++> (Cayley g) = Cayley $ liftA2 (<++>) f g
+  (Cayley f) <++> (Cayley g) = Cayley $ (<++>) <$> f <*> g
diff --git a/src/Data/Profunctor/Choice.idr b/src/Data/Profunctor/Choice.idr
new file mode 100644
index 0000000..0e4b72f
--- /dev/null
+++ b/src/Data/Profunctor/Choice.idr
@@ -0,0 +1,61 @@
+module Data.Profunctor.Choice
+
+import Data.Either
+import Data.Morphisms
+import Data.Profunctor
+import Control.Arrow
+import Control.Category
+
+%default total
+
+-- }}}
+-- Choice
+-- {{{
+
+||| Generalized DownStar of a Costrong Functor
+public export
+interface Profunctor p => Choice (0 p : Type -> Type -> Type) where
+  ||| Like first' but with sum rather than product types
+  |||
+  ||| ````idris example
+  ||| left' (Kleisli $ \x => Just $ reverse x)
+  ||| ````
+  |||
+  left' : p a b -> p (Either a c) (Either b c)
+  left' = dimap mirror mirror . right'
+
+  ||| Like second' but with sum rather than product types
+  |||
+  ||| ````idris example
+  ||| right' (Kleisli $ \x => Just $ reverse x)
+  ||| ````
+  |||
+  right' : p a b -> p (Either c a) (Either c b)
+  right' = dimap mirror mirror . left'
+
+export
+implementation Monad m => Choice (Kleislimorphism m) where
+  left'  f = Kleisli $ either (applyKleisli       $ f        >>> arrow Left)
+                              (applyKleisli {f=m} $ arrow id >>> arrow Right)
+  right' f = Kleisli $ either (applyKleisli {f=m} $ arrow id >>> arrow Left)
+                              (applyKleisli       $ f        >>> arrow Right)
+
+export
+implementation Choice Morphism where
+  left'  (Mor f) = Mor $ either (Left . f) Right
+  right' (Mor f) = Mor $ either Left (Right . f)
+
+export
+implementation Choice Tagged where
+  left'  = Tag . Left  . runTagged
+  right' = Tag . Right . runTagged
+
+export
+implementation Applicative f => Choice (UpStarred f) where
+  left'  (UpStar f) = UpStar $ either (map Left . f   ) (map Right . pure)
+  right' (UpStar f) = UpStar $ either (map Left . pure) (map Right . f   )
+
+export
+implementation Monoid r => Choice (Forgotten r) where
+  left'  (Forget k) = Forget .      either k $ const neutral
+  right' (Forget k) = Forget . flip either k $ const neutral
diff --git a/src/Data/Profunctor/Closed.idr b/src/Data/Profunctor/Closed.idr
index d910b92..32266f8 100644
--- a/src/Data/Profunctor/Closed.idr
+++ b/src/Data/Profunctor/Closed.idr
@@ -2,68 +2,85 @@ module Data.Profunctor.Closed
 
 import Control.Arrow
 import Control.Category
+import Data.Morphisms
 import Data.Profunctor
+import Data.Profunctor.Strong
 import Data.Profunctor.Unsafe
 
-%access public export
-
 ||| A Closed Profunctor that allows the closed structure to pass through
-interface Profunctor p => Closed (p : Type -> Type -> Type) where
+public export
+interface Profunctor p => Closed (0 p : Type -> Type -> Type) where
   ||| Pass the closed structure through the Profunctor
   |||
   ||| ````idris example
   ||| closed $ DownStar $ show
   ||| ````
   |||
-  closed : {x : _} -> p a b -> p (x -> a) (x -> b)
+  closed : {0 x : _} -> p a b -> p (x -> a) (x -> b)
 
-implementation Closed Arr where
-  closed = MkArr . (.) . runArr
+export
+implementation Closed Morphism where
+  closed = Mor . (.) . applyMor
 
+export
 implementation Functor f => Closed (DownStarred f) where
   closed (DownStar fab) = DownStar $ \fxa,x => fab $ map (\f => f x) fxa
 
+export
 implementation Monoid r => Closed (Forgotten r) where
   closed = const . Forget $ const neutral
 
+export
+implementation Closed Zipping where
+  closed (MkZipping f) = MkZipping $ \f1, f2, x => f (f1 x) (f2 x)
+
 ||| Closure adjoins a Closed structure to any Profunctor
+||| Adjoin a closed-structured Profunctor to a profunctor
+|||
+||| ````idris example
+||| Close $ closed $ DownStar $ show
+||| ````
+|||
+public export
 record Closure (p : Type -> Type -> Type) a b where
-  ||| Adjoin a closed-structured Profunctor to a profunctor
-  |||
-  ||| ````idris example
-  ||| Close $ closed $ DownStar $ show
-  ||| ````
-  |||
   constructor Close
   runClosure : p (x -> a) (x -> b)
 
+export
 hither : (s -> (a,b)) -> (s -> a, s -> b)
 hither h = (fst . h, snd . h)
 
+export
 yon : (s -> a, s -> b) -> s -> (a,b)
 yon h s = (fst h s, snd h s)
 
+export
 implementation Profunctor p => Profunctor (Closure p) where
   dimap f g (Close p) = Close $ dimap ((.) f) ((.) g) p
   lmap  f   (Close p) = Close $ lmap  ((.) f)         p
   rmap    g (Close p) = Close $ rmap          ((.) g) p
 
+export
 implementation UnsafeProfunctor p => UnsafeProfunctor (Closure p) where
   w         #. (Close p) = Close $ ((.) w) #. p
   (Close p) .# w         = Close $ p       .# ((.) w)
 
+export
 implementation Strong p => Strong (Closure p) where
   first'   (Close p) = Close $ dimap hither yon $ first' p
   second'  (Close p) = Close $ dimap hither yon $ second' p
 
+export
 implementation Profunctor p => Functor (Closure p a) where
   map = rmap
 
+export
 close : Closed p => {a,b : Type} -> ({a',b' : Type} -> p a' b' -> q a' b') ->
                                                        p a b -> (Closure q) a b
 close f p = Close {x=believe_me p} . f $ closed p
 
 ||| Environment is left adjoint to Closure
+public export
 data Environment : (Type -> Type -> Type) -> Type -> Type -> Type where
   ||| Convert a Profunctor to an Environment
   |||
@@ -71,8 +88,9 @@ data Environment : (Type -> Type -> Type) -> Type -> Type -> Type where
   ||| Environize $ Kleisli $ \x => Just $ reverse x
   ||| ````
   |||
-  Environize : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
+  Environize : ((c' -> b') -> b) -> p a' b' -> (a -> c' -> a') -> Environment p a b
 
+export
 implementation Profunctor p => Profunctor (Environment p) where
   dimap f g (Environize l m r) = Environize (g . l) m (r . f)
   lmap  f   (Environize l m r) = Environize l       m (r . f)
diff --git a/src/Data/Profunctor/Codensity.idr b/src/Data/Profunctor/Codensity.idr
index 096b204..30d4c5d 100644
--- a/src/Data/Profunctor/Codensity.idr
+++ b/src/Data/Profunctor/Codensity.idr
@@ -4,17 +4,18 @@ import Control.Category
 import Data.Profunctor
 import Data.Profunctor.Composition
 
-%access public export
-
 ||| The right Kan extenstion of a Profunctor
+public export
 record Codense (p : Type -> Type -> Type) a b where
   constructor Codensity
   runCodensity : p x a -> p x b
 
+export
 implementation Profunctor p => Profunctor (Codense p) where
   dimap ca bd f = Codensity $ rmap bd . runCodensity f . rmap ca
   lmap  ca    f = Codensity $           runCodensity f . rmap ca
   rmap     bd f = Codensity $ rmap bd . runCodensity f
 
+export
 implementation Profunctor p => Functor (Codense p a) where
   map bd f = Codensity $ rmap bd . runCodensity f
diff --git a/src/Data/Profunctor/Comonad.idr b/src/Data/Profunctor/Comonad.idr
index 461e431..24a8766 100644
--- a/src/Data/Profunctor/Comonad.idr
+++ b/src/Data/Profunctor/Comonad.idr
@@ -2,59 +2,32 @@ module Data.Profunctor.Comonad
 
 import Control.Arrow
 import Control.Category
+import Control.Comonad
 import Data.Profunctor
 
-%access public export
-
-interface Functor w => Comonad (w : Type -> Type) where
-  extract : w a -> a
-
-  duplicate : w a -> w (w a)
-  duplicate = extend id
-
-  extend : (w a -> b) -> w a -> w b
-  extend f = map f . duplicate
-
-implementation Comonad (Tagged a) where
-  duplicate = Tag
-  extract = runTagged
-
-infixr 1 =>>
-(=>>) : Comonad w => w a -> (w a -> b) -> w b
-(=>>) = flip extend
-
-infixl 1 <<=
-(<<=) : Comonad w => (w a -> b) -> w a -> w b
-(<<=) = extend
-
-wfix : Comonad w => w (w a -> a) -> a
-wfix w = extract w $ w =>> wfix
-
-infixr 1 =<=
-(=<=) : Comonad w => (w b -> c) -> (w a -> b) -> w a -> c
-f =<= g = f . extend g
-
-infixr 1 =>=
-(=>=) : Comonad w => (w a -> b) -> (w b -> c) -> w a -> c
-f =>= g = g . extend f
-
+public export
 record Cokleislimorphism (w : Type -> Type) a b where
   constructor Cokleisli
   runCokleisli : w a -> b
 
+export
 implementation Functor w => Profunctor (Cokleislimorphism w) where
   dimap f g (Cokleisli h) = Cokleisli $ g . h . map f
 
+export
 implementation Comonad w => Category (Cokleislimorphism w) where
   id = Cokleisli extract
   (Cokleisli f) . (Cokleisli g) = Cokleisli $ f =<= g
 
+export
 implementation Functor (Cokleislimorphism w a) where
   map f (Cokleisli g) = Cokleisli $ f . g
 
+export
 implementation Applicative (Cokleislimorphism w a) where
   pure = Cokleisli . const
   (Cokleisli f) <*> (Cokleisli a) = Cokleisli $ \w => f w $ a w
 
+export
 implementation Monad (Cokleislimorphism w a) where
   (Cokleisli k) >>= f = Cokleisli $ \w => runCokleisli (f $ k w) w
diff --git a/src/Data/Profunctor/Composition.idr b/src/Data/Profunctor/Composition.idr
index 227843a..d78a943 100644
--- a/src/Data/Profunctor/Composition.idr
+++ b/src/Data/Profunctor/Composition.idr
@@ -4,35 +4,70 @@ import Control.Arrow
 import Control.Category
 import Data.Profunctor
 import Data.Profunctor.Closed
-
-%access public export
+import Data.Profunctor.Choice
+import Data.Profunctor.Rep
+import Data.Profunctor.Sieve
+import Data.Profunctor.Strong
 
 ||| The composition of two Profunctors
+public export
 data Procomposed : (Type -> Type -> Type) -> (Type -> Type -> Type) ->
                    Type -> Type -> Type where
   ||| Compose two Profunctors
-  Procompose : {x,c,d : _} -> p x c -> q d x -> Procomposed p q d c
+  Procompose : {0 x,c,d : _} -> p x c -> q d x -> Procomposed p q d c
 
+export
 procomposed : Category p => Procomposed p p a b -> p a b
 procomposed (Procompose pxc pdx) = pxc . pdx
 
+export
 implementation (Profunctor p, Profunctor q) => Profunctor (Procomposed p q) where
   dimap l r (Procompose f g) = Procompose (rmap r f) (lmap l g)
   lmap  l   (Procompose f g) = Procompose         f  (lmap l g)
   rmap    r (Procompose f g) = Procompose (rmap r f)         g
 
+export
 implementation Profunctor p => Functor (Procomposed p q a) where
   map k (Procompose f g) = Procompose (rmap k f) g
 
+export
+implementation (Strong p, Strong q) => Strong (Procomposed p q) where
+  first' (Procompose x y) = Procompose (first' x) (first' y)
+  second' (Procompose x y) = Procompose (second' x) (second' y)
+
+export
+implementation (Choice p, Choice q) => Choice (Procomposed p q) where
+  left' (Procompose x y) = Procompose (left' x) (left' y)
+  right' (Procompose x y) = Procompose (right' x) (right' y)
+
+export
+implementation (Closed p, Closed q) => Closed (Procomposed p q) where
+  closed (Procompose x y) = Procompose (closed x) (closed y)
+
+export
+implementation (Sieve p f, Sieve q g) => Sieve (Procomposed p q) (g . f) using Functor.Compose where
+  sieve (Procompose g f) d = sieve g <$> sieve f d
+
+export
+implementation (Representable p f, Representable q g) => Representable (Procomposed p q) (g . f) using Functor.Compose where
+  tabulate f = Procompose (tabulate id) (tabulate f)
+
+export
+implementation (Cosieve p f, Cosieve q g) => Cosieve (Procomposed p q) (f . g) using Functor.Compose where
+  cosieve (Procompose g f) d = cosieve g $ cosieve f <$> d
+
 ||| The right Kan lift of one Profunctor along another
+public export
 record Rifted (p : Type -> Type -> Type) (q : Type -> Type -> Type) a b where
   constructor Rift
-  runRift : p b x -> q a x
+  runRift : p b y -> q a y
 
+export
 implementation (Profunctor p, Profunctor q) => Profunctor (Rifted p q) where
   dimap ca bd f = Rift $ lmap ca . runRift f . lmap bd
   lmap  ca    f = Rift $ lmap ca . runRift f
   rmap     bd f = Rift $           runRift f . lmap bd
 
+export
 implementation Profunctor p => Functor (Rifted p q a) where
   map bd f = Rift $ runRift f . lmap bd
diff --git a/src/Data/Profunctor/Fold.idr b/src/Data/Profunctor/Fold.idr
index 77b3028..2c71123 100644
--- a/src/Data/Profunctor/Fold.idr
+++ b/src/Data/Profunctor/Fold.idr
@@ -2,33 +2,71 @@ module Data.Profunctor.Fold
 
 import Control.Algebra
 import Data.Profunctor
+import Data.Profunctor.Choice
 import Data.Profunctor.Prism
 import Data.SortedSet
+import Data.Verified.Foldable
 
-%access public export
+liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
+liftA2 f x y = f <$> x <*> y
+
+public export
+interface Fold f where
+  run : Foldable t => f a b -> t a -> b
+
+  ||| Two folds are equal if they are point wise equal in their ``run`` function.
+  ||| We need this axiom because otherwise the Applicative instance would be unlawful.
+  ||| The requirement for a ``FoldableV`` instance stems from the necessity to destruct ``t``.
+  foldExtensionality : Fold f => (fa, fb : f a b) -> (forall t. FoldableV t => (l : t a) -> run fa l = run fb l) -> fa = fb
+
+namespace Fold
+  public export
+  finish : (r1 -> a -> b) -> (r2 -> a) -> (r1, r2) -> b
+  finish f g (x, y) = f x (g y)
+
+  namespace L
+    public export
+    step : (r1 -> a -> r1) -> (r2 -> a -> r2) -> (r1, r2) -> a -> (r1, r2)
+    step u v (x, y) b = (u x b, v y b)
+
+  namespace R
+    public export
+    step : (a -> r1 -> r1) -> (a -> r2 -> r2) -> a -> (r1, r2) -> (r1, r2)
+    step u v b (x, y) = (u b x, v b y)
 
 ||| A leftwards fold
+public export
 data L a b = MkL (r -> b) (r -> a -> r) r
 
 ||| Turn a finalization function, an accumulation function, and an initial value
 ||| into an `L`
+export
 unfoldL : (s -> (b, a -> s)) -> s -> L a b
 unfoldL f = MkL (fst . f) (snd . f)
 
 ||| Run an `L` on a `Foldable` container
+export
 runL : Foldable t => L a b -> t a -> b
 runL (MkL k h z) = k . foldl h z
 
 ||| Run an `L` on a `Foldable` container, accumulating results
+export
 scanL : L a b -> List a -> List b
 scanL (MkL k _ z) []      = pure $ k z
 scanL (MkL k h z) (x::xs) = k (h z x) :: scanL (MkL k h (h z x)) xs
 
+export
+implementation Fold L where
+  run = runL
+  foldExtensionality a b = believe_me
+
+export
 implementation Profunctor L where
   dimap f g (MkL k h z) = MkL (g . k) ((. f) . h) z
   rmap    g (MkL k h z) = MkL (g . k) h           z
   lmap  f   (MkL k h z) = MkL k       ((. f) . h) z
 
+export
 implementation Choice L where
   left' (MkL {r} k h z) = MkL (\e => case e of Left a  => Left $ k a
                                                Right b => Right b)
@@ -47,80 +85,207 @@ implementation Choice L where
     step (Left c)  _         = Left c
     step _         (Left c)  = Left c
 
+export
 implementation Prisming L where
   costrength = rmap (either id id) . right'
 
+export
 implementation Functor (L a) where
   map = rmap
 
+export
 implementation Applicative (L a) where
   pure b = MkL (const b) (const $ const ()) ()
-  (MkL f u y) <*> (MkL a v z) = MkL (uncurry $ (. a) . f)
-                                    (\(x, y), b => (u x b, v y b))
-                                    (y, z)
+  (MkL f u y) <*> (MkL a v z) = MkL (Fold.finish f a) (Fold.L.step u v) (y, z)
 
+export
 implementation Monad (L a) where
   m >>= f = MkL ((. f) . flip runL) ((. pure) . (++)) [] <*> m
 
+export
 implementation Semigroup m => Semigroup (L a m) where
   (<+>) = liftA2 (<+>)
 
+public export
+runLSemigroupDistributive : (FoldableV t, Semigroup m) => (ll, lr : L a m) -> (fo : t a) -> runL (ll <+> lr) fo = runL ll fo <+> runL lr fo
+runLSemigroupDistributive (MkL {r=r1} d g u) (MkL {r=r2} e h v) fo = let
+    prf : (xs : List a) -> (u : r1) -> (v : r2) -> foldl (L.step g h) (u, v) xs = (foldl g u xs, foldl h v xs)
+    prf []      = \_, _ => Refl
+    prf (x::xs) = \y, z => prf xs (g y x) (h z x)
+ in rewrite toListNeutralL g u fo
+ in rewrite toListNeutralL h v fo
+ in rewrite toListNeutralL (step g h) (u, v) fo
+ in cong (Fold.finish (\n, m => d n <+> m) e) (prf (toList fo) u v)
+
+export
+implementation (SemigroupV m) => SemigroupV (L a m) where
+  semigroupOpIsAssociative l@(MkL {r=r1} d g u) c@(MkL {r=r2} e h v) r@(MkL {r=r3} f j w)
+    = let
+      prf : forall t. FoldableV t => (fo : t a) -> runL (l <+> (c <+> r)) fo = runL ((l <+> c) <+> r) fo
+      prf fo = rewrite runLSemigroupDistributive l (c <+> r) fo
+            in rewrite runLSemigroupDistributive c r fo
+            in rewrite semigroupOpIsAssociative (d (foldl g u fo)) (e (foldl h v fo)) (f (foldl j w fo))
+            in rewrite sym (runLSemigroupDistributive l c fo)
+            in sym (runLSemigroupDistributive (l <+> c) r fo)
+    in foldExtensionality (l <+> (c <+> r)) ((l <+> c) <+> r) prf
+
+export
 implementation Monoid m => Monoid (L a m) where
   neutral = pure neutral
 
+export
+implementation MonoidV m => MonoidV (L a m) where
+  monoidNeutralIsNeutralL l@(MkL k h z) = let
+    neut : L a m
+    neut = neutral
+    prf : forall t. FoldableV t => (fo : t a) -> runL (l <+> neut) fo = runL l fo
+    prf fo = rewrite runLSemigroupDistributive l neut fo
+          in monoidNeutralIsNeutralL (k (foldl h z fo))
+
+    in foldExtensionality (l <+> neut) l prf
+  monoidNeutralIsNeutralR l@(MkL k h z) = let
+    neut : L a m
+    neut = neutral
+    prf : forall t. FoldableV t => (fo : t a) -> runL (neut <+> l) fo = runL l fo
+    prf fo = rewrite runLSemigroupDistributive neut l fo
+          in monoidNeutralIsNeutralR (k (foldl h z fo))
+    in foldExtensionality (neut <+> l) l prf
+
+export
 implementation Group m => Group (L a m) where
   inverse = map inverse
-
+  groupInverseIsInverseR l@(MkL k h z) = let
+       neut : L a m
+       neut = neutral
+       prf : forall t. FoldableV t => (fo : t a) -> runL (inverse l <+> l) fo = runL neut fo
+       prf fo = rewrite runLSemigroupDistributive (inverse l) l fo
+             in groupInverseIsInverseR (k (foldl h z fo))
+    in foldExtensionality (inverse l <+> l) neut prf
+
+export
 implementation AbelianGroup m => AbelianGroup (L a m) where
-
-implementation Ring m => Ring (L a m) where
-  (<.>) = liftA2 (<.>)
-
+  groupOpIsCommutative l@(MkL d g u) r@(MkL f j w) = let
+      prf : forall t. FoldableV t => (fo : t a) -> runL (l <+> r) fo = runL (r <+> l) fo
+      prf fo = rewrite runLSemigroupDistributive l r fo
+            in rewrite groupOpIsCommutative (d (foldl g u fo)) (f (foldl j w fo))
+            in sym (runLSemigroupDistributive r l fo)
+    in foldExtensionality (l <+> r) (r <+> l) prf
+
+mutual
+  export
+  implementation Ring m => Ring (L a m) where
+    (<.>) = liftA2 (<.>)
+    ringOpIsAssociative l@(MkL d g u) c@(MkL e h v) r@(MkL f j w) = let
+         prf : forall t. FoldableV t => (fo : t a) -> runL (l <.> (c <.> r)) fo = runL ((l <.> c) <.> r) fo
+         prf fo = rewrite runLRingDistributive l (c <.> r) fo
+               in rewrite runLRingDistributive c r fo
+               in rewrite ringOpIsAssociative (d (foldl g u fo)) (e (foldl h v fo)) (f (foldl j w fo))
+               in rewrite sym (runLRingDistributive l c fo)
+               in sym (runLRingDistributive (l <.> c) r fo)
+      in foldExtensionality (l <.> (c <.> r)) ((l <.> c) <.> r) prf
+    ringOpIsDistributiveL l@(MkL d g u) c@(MkL e h v) r@(MkL f j w) = let
+         prf : forall t. FoldableV t => (fo : t a) -> runL (l <.> (c <+> r)) fo = runL ((l <.> c) <+> (l <.> r)) fo
+         prf fo = rewrite runLRingDistributive l (c <+> r) fo
+               in rewrite runLSemigroupDistributive c r fo
+               in rewrite ringOpIsDistributiveL (d (foldl g u fo)) (e (foldl h v fo)) (f (foldl j w fo))
+               in rewrite sym (runLRingDistributive l c fo)
+               in rewrite sym (runLRingDistributive l r fo)
+               in sym (runLSemigroupDistributive (l <.> c) (l <.> r) fo)
+      in foldExtensionality (l <.> (c <+> r)) ((l <.> c) <+> (l <.> r)) prf
+    ringOpIsDistributiveR l@(MkL d g u) c@(MkL e h v) r@(MkL f j w) = let
+         prf : forall t. FoldableV t => (fo : t a) -> runL ((l <+> c) <.> r) fo = runL ((l <.> r) <+> (c <.> r)) fo
+         prf fo = rewrite runLRingDistributive (l <+> c) r fo
+               in rewrite runLSemigroupDistributive l c fo
+               in rewrite ringOpIsDistributiveR (d (foldl g u fo)) (e (foldl h v fo)) (f (foldl j w fo))
+               in rewrite sym (runLRingDistributive l r fo)
+               in rewrite sym (runLRingDistributive c r fo)
+               in sym (runLSemigroupDistributive (l <.> r) (c <.> r) fo)
+      in foldExtensionality ((l <+> c) <.> r) ((l <.> r) <+> (c <.> r)) prf
+
+  public export
+  runLRingDistributive : (FoldableV t, Ring m) => (ll, lr : L a m) -> (fo : t a) -> runL (ll <.> lr) fo = runL ll fo <.> runL lr fo
+  runLRingDistributive (MkL {r=r1} d g u) (MkL {r=r2} e h v) fo = let
+      prf : (xs : List a) -> (u : r1) -> (v : r2) -> foldl (L.step g h) (u, v) xs = (foldl g u xs, foldl h v xs)
+      prf [] = \_, _ => Refl
+      prf (x::xs) = \u, v => prf xs (g u x) (h v x)
+   in rewrite toListNeutralL (step g h) (u, v) fo
+   in rewrite toListNeutralL g u fo
+   in rewrite toListNeutralL h v fo
+   in cong (finish (\n, m => d n <.> m) e) (prf (toList fo) u v)
+
+export
 implementation RingWithUnity m => RingWithUnity (L a m) where
   unity = pure unity
+  unityIsRingIdL l@(MkL d g u) = let
+      uni : L a m
+      uni = unity
+      prf : forall t. FoldableV t => (fo : t a) -> runL (l <.> uni) fo = runL l fo
+      prf fo = rewrite runLRingDistributive l uni fo
+            in unityIsRingIdL (d (foldl g u fo))
+    in foldExtensionality (l <.> uni) l prf
+  unityIsRingIdR l@(MkL d g u) = let
+      uni : L a m
+      uni = unity
+      prf : forall t. FoldableV t => (fo : t a) -> runL (uni <.> l) fo = runL l fo
+      prf fo = rewrite runLRingDistributive uni l fo
+            in unityIsRingIdR (d (foldl g u fo))
+    in foldExtensionality (uni <.> l) l prf
 
 -- The `Field` implementation won't type check, but it should exist
 
+export
 implementation Num n => Num (L a n) where
   (+)         = liftA2 (+)
   (*)         = liftA2 (*)
   fromInteger = pure . fromInteger
 
+export
 implementation Neg n => Neg (L a n) where
   (-)         = liftA2 (-)
+  negate      = map negate
+
+export
+implementation Abs n => Abs (L a n) where
   abs         = map abs
-  negate = map negate
 
 ||| An `L` to calculate the size of a `Foldable` container
+export
 length : Num a => L _ a
 length = MkL id (const . (+ 1)) 0
 
 ||| An `L` which returns `True` if the container is empty, and `False` otherwise
+export
 null : L _ Bool
 null = MkL id (const $ const False) True
 
 ||| An `L` which returns either `Just` an element satisfying a given condition or
 ||| `Nothing`
+export
 find : (a -> Bool) -> L a (Maybe a)
 find p = MkL id step Nothing where
+  step : Maybe a -> a -> Maybe a
   step x a = case x of Nothing => if p a then Just a else Nothing
                        _       => x
 
 ||| An `L` which returns either `Just` the index of a given element or `Nothing`
+export
 index : Nat -> L a (Maybe a)
 index i = MkL done step (Left 0) where
+  step : Either Nat a -> a -> Either Nat a
   step x = case x of Left j => if i == j then Right else const . Left $ S j
                      _      => const x
   done : Either Nat a -> Maybe a
   done = either (const Nothing) Just
 
 ||| An `L` which returns a `List` containing each unique element in the input
+export
 nub : Eq a => L a (List a)
 nub = MkL (flip snd []) step ([], id) where
   step : (List a, List a -> List a) -> a -> (List a, List a -> List a)
   step (k, r) i = if elem i k then (k, r) else (i :: k, r . (i ::))
 
 ||| A faster `nub`
+export
 fastNub : {a : Type} -> Ord a => L a (List a)
 fastNub {a} = MkL (flip snd $ the (List a) [])
                   (\(s, r), a => if contains a s then (s, r)
@@ -128,68 +293,89 @@ fastNub {a} = MkL (flip snd $ the (List a) [])
                   (the (SortedSet a) empty, id)
 
 ||| An `L` which returns a sorted `List` of each element in the input
+export
 sort : Ord a => L a (List a)
 sort = MkL id (flip $ merge . pure) [] where
-  merge : Ord a => List a -> List a -> List a
+  merge : List a -> List a -> List a
   merge xs [] = xs
   merge [] ys = ys
   merge (x :: xs) (y :: ys) = if x < y then x :: merge xs (y :: ys)
                                        else y :: merge (x :: xs) ys
 
 ||| Turns a binary function into a lazy `L`
+export
 L1 : (a -> a -> a) -> L a (Lazy (Maybe a))
-L1 s = MkL Delay (\m => Just . case m of Just x => s x; _ => id) Nothing
+L1 s = MkL (\x => Delay x) (\m => Just . case m of Just x => s x; _ => id) Nothing
 
 ||| Returns the first element of its input, if it exists
-first : L a (Maybe a)
-first = map Force $ L1 const
+export
+first : L a (Lazy (Maybe a))
+first = map (\x => Force x) $ L1 const
 
 ||| Returns the last element of its input, if it exists
-last : L a (Maybe a)
-last = map Force . L1 $ flip const
+export
+last : L a (Lazy (Maybe a))
+last = map (\x => Force x) . L1 $ flip const
 
 ||| Returns the maximum element of its input, if it exists
-maximum : Ord a => L a (Maybe a)
-maximum = map Force $ L1 max
+export
+maximum : Ord a => L a (Lazy (Maybe a))
+maximum = map (\x => Force x) $ L1 max
 
 ||| Returns the minimum element of its input, if it exists
-minimum : Ord a => L a (Maybe a)
-minimum = map Force $ L1 min
+export
+minimum : Ord a => L a (Lazy (Maybe a))
+minimum = map (\x => Force x) $ L1 min
 
 ||| Sums the elements of its input
+export
 sum : Num a => L a a
 sum = MkL id (+) 0
 
 ||| Returns the product of the elements of its input
+export
 product : Num a => L a a
 product = MkL id (*) 0
 
 ||| Concats the elements of its input
+export
 concat : Monoid a => L a a
 concat = MkL id (<+>) neutral
 
 ||| Concats the elements of its input using binary operation given by the ring
+export
 concatR : RingWithUnity a => L a a
 concatR = MkL id (<.>) unity
 
 ||| A rightwards fold
+public export
 data R a b = MkR (r -> b) (a -> r -> r) r
 
 ||| Run an `R` on a `Foldable` container
+export
 runR : Foldable t => R a b -> t a -> b
 runR (MkR k h z) = k . foldr h z
 
 ||| Run an `R` on a `Foldable` container, accumulating results
-scanR : R a b -> List a -> List b
-scanR (MkR k h z) = map k . scan' where
-  scan' []      = pure z
+export
+scanR : {r : Type} -> R a b -> List a -> List b
+scanR (MkR {r} k h z) = map k . scan' where
+  scan' : List a -> List r
+  scan' []      = z :: []
   scan' (x::xs) = let l = scan' xs in h x (case l of [] => z; (q::_) => q) :: l
 
+export
+implementation Fold R where
+  run = runR
+  foldExtensionality a b = believe_me
+
+export
 implementation Profunctor R where
   dimap f g (MkR k h z) = MkR (g . k) (h . f) z
   rmap    g (MkR k h z) = MkR (g . k) h       z
   lmap  f   (MkR k h z) = MkR k       (h . f) z
 
+export
 implementation Choice R where
   left' (MkR {r} k h z) = MkR (\e => case e of Left a  => Left $ k a
                                                Right b => Right b)
@@ -208,52 +394,173 @@ implementation Choice R where
     step (Left c)  _         = Left c
     step _         (Left c)  = Left c
 
+export
 implementation Prisming R where
   costrength = rmap (either id id) . right'
 
+export
 implementation Functor (R a) where
   map = rmap
 
+export
 implementation Applicative (R a) where
   pure b = MkR (const b) (const $ const ()) ()
-  (MkR f u y) <*> (MkR a v z) = MkR (uncurry $ (. a) . f)
-                                    (\b, (x, y) => (u b x, v b y))
-                                    (y, z)
+  (MkR f u y) <*> (MkR a v z) = MkR (Fold.finish f a) (Fold.R.step u v) (y, z)
 
+export
 implementation Monad (R a) where
   m >>= f = MkR ((. f) . flip runR) (::) [] <*> m
 
+export
 implementation Semigroup m => Semigroup (R a m) where
   (<+>) = liftA2 (<+>)
 
+public export
+runRSemigroupDistributive : (FoldableV t, Semigroup m) => (rl, rr : R a m) -> (li : t a) -> runR (rl <+> rr) li = runR rl li <+> runR rr li
+runRSemigroupDistributive (MkR {r=r1} d g u) (MkR {r=r2} e h v) fo = let
+    prf : (xs : List a) -> foldr (R.step g h) (u, v) xs = (foldr g u xs, foldr h v xs)
+    prf [] = Refl
+    prf (x::xs) = cong (step g h x) (prf xs)
+ in rewrite toListNeutralR g u fo
+ in rewrite toListNeutralR h v fo
+ in rewrite toListNeutralR (step g h) (u, v) fo
+ in cong (Fold.finish (\n, m => d n <+> m) e) (prf (toList fo))
+
+export
+implementation SemigroupV m => SemigroupV (R a m) where
+  semigroupOpIsAssociative l@(MkR d g u) c@(MkR e h v) r@(MkR f j w) = let
+      prf : forall t. FoldableV t => (fo : t a) -> runR (l <+> (c <+> r)) fo = runR ((l <+> c) <+> r) fo
+      prf fo = rewrite runRSemigroupDistributive l (c <+> r) fo
+            in rewrite runRSemigroupDistributive c r fo
+            in rewrite semigroupOpIsAssociative (d (foldr g u fo)) (e (foldr h v fo)) (f (foldr j w fo))
+            in rewrite sym (runRSemigroupDistributive l c fo)
+            in sym (runRSemigroupDistributive (l <+> c) r fo)
+      in foldExtensionality (l <+> (c <+> r)) ((l <+> c) <+> r) prf
+
+export
 implementation Monoid m => Monoid (R a m) where
   neutral = pure neutral
 
+export
+implementation MonoidV m => MonoidV (R a m) where
+  monoidNeutralIsNeutralL r@(MkR k h z) = let
+    neut : R a m
+    neut = neutral
+    prf : forall t. FoldableV t => (fo : t a) -> runR (r <+> neut) fo = runR r fo
+    prf fo = rewrite runRSemigroupDistributive r neut fo
+            in monoidNeutralIsNeutralL (k (foldr h z fo))
+    in foldExtensionality (r <+> neut) r prf
+
+  monoidNeutralIsNeutralR r@(MkR k h z) = let
+    neut : R a m
+    neut = neutral
+    prf : forall t. FoldableV t => (fo : t a) -> runR (neut <+> r) fo = runR r fo
+    prf fo = rewrite runRSemigroupDistributive neut r fo
+            in monoidNeutralIsNeutralR (k (foldr h z fo))
+    in foldExtensionality (neut <+> r) r prf
+
+export
 implementation Num n => Num (R a n) where
   (+)         = liftA2 (+)
   (*)         = liftA2 (*)
   fromInteger = pure . fromInteger
 
+export
 implementation Neg n => Neg (R a n) where
   (-)         = liftA2 (-)
+  negate      = map negate
+
+export
+implementation Abs n => Abs (R a n) where
   abs         = map abs
-  negate = map negate
 
+export
 implementation Group m => Group (R a m) where
   inverse = map inverse
-
+  groupInverseIsInverseR r@(MkR k h z) = let
+       neut : R a m
+       neut = neutral
+       prf : forall t. FoldableV t => (fo : t a) -> runR (inverse r <+> r) fo = runR neut fo
+       prf fo = rewrite runRSemigroupDistributive (inverse r) r fo
+             in groupInverseIsInverseR (k (foldr h z fo))
+    in foldExtensionality (inverse r <+> r) neut prf
+
+export
 implementation AbelianGroup m => AbelianGroup (R a m) where
-
-implementation Ring m => Ring (R a m) where
-  (<.>) = liftA2 (<.>)
-
+  groupOpIsCommutative l@(MkR d g u) r@(MkR f j w) = let
+      prf : forall t. FoldableV t => (fo : t a) -> runR (l <+> r) fo = runR (r <+> l) fo
+      prf fo = rewrite runRSemigroupDistributive l r fo
+            in rewrite groupOpIsCommutative (d (foldr g u fo)) (f (foldr j w fo))
+            in sym (runRSemigroupDistributive r l fo)
+    in foldExtensionality (l <+> r) (r <+> l) prf
+
+mutual
+  export
+  implementation Ring m => Ring (R a m) where
+    (<.>) = liftA2 (<.>)
+    ringOpIsAssociative l@(MkR d g u) c@(MkR e h v) r@(MkR f j w) = let
+         prf : forall t. FoldableV t => (fo : t a) -> runR (l <.> (c <.> r)) fo = runR ((l <.> c) <.> r) fo
+         prf fo = rewrite runRRingDistributive l (c <.> r) fo
+               in rewrite runRRingDistributive c r fo
+               in rewrite ringOpIsAssociative (d (foldr g u fo)) (e (foldr h v fo)) (f (foldr j w fo))
+               in rewrite sym (runRRingDistributive l c fo)
+               in sym (runRRingDistributive (l <.> c) r fo)
+      in foldExtensionality (l <.> (c <.> r)) ((l <.> c) <.> r) prf
+    ringOpIsDistributiveL l@(MkR d g u) c@(MkR e h v) r@(MkR f j w) = let
+         prf : forall t. FoldableV t => (fo : t a) -> runR (l <.> (c <+> r)) fo = runR ((l <.> c) <+> (l <.> r)) fo
+         prf fo = rewrite runRRingDistributive l (c <+> r) fo
+               in rewrite runRSemigroupDistributive c r fo
+               in rewrite ringOpIsDistributiveL (d (foldr g u fo)) (e (foldr h v fo)) (f (foldr j w fo))
+               in rewrite sym (runRRingDistributive l c fo)
+               in rewrite sym (runRRingDistributive l r fo)
+               in sym (runRSemigroupDistributive (l <.> c) (l <.> r) fo)
+      in foldExtensionality (l <.> (c <+> r)) ((l <.> c) <+> (l <.> r)) prf
+
+    ringOpIsDistributiveR l@(MkR d g u) c@(MkR e h v) r@(MkR f j w) = let
+         prf : forall t. FoldableV t => (fo : t a) -> runR ((l <+> c) <.> r) fo = runR ((l <.> r) <+> (c <.> r)) fo
+         prf fo = rewrite runRRingDistributive (l <+> c) r fo
+               in rewrite runRSemigroupDistributive l c fo
+               in rewrite ringOpIsDistributiveR (d (foldr g u fo)) (e (foldr h v fo)) (f (foldr j w fo))
+               in rewrite sym (runRRingDistributive l r fo)
+               in rewrite sym (runRRingDistributive c r fo)
+               in sym (runRSemigroupDistributive (l <.> r) (c <.> r) fo)
+      in foldExtensionality ((l <+> c) <.> r) ((l <.> r) <+> (c <.> r)) prf
+
+  public export
+  runRRingDistributive : (FoldableV t, Ring m) => (rl, rr : R a m) -> (li : t a) -> runR (rl <.> rr) li = runR rl li <.> runR rr li
+  runRRingDistributive (MkR {r=r1} d g u) (MkR {r=r2} e h v) fo = let
+      prf : (xs : List a) -> foldr (R.step g h) (u, v) xs = (foldr g u xs, foldr h v xs)
+      prf [] = Refl
+      prf (x::xs) = cong (step g h x) (prf xs)
+   in rewrite toListNeutralR (step g h) (u, v) fo
+   in rewrite toListNeutralR g u fo
+   in rewrite toListNeutralR h v fo
+   in cong (Fold.finish (\n, m => d n <.> m) e) (prf (toList fo))
+
+export
 implementation RingWithUnity m => RingWithUnity (R a m) where
   unity = pure unity
+  unityIsRingIdL r@(MkR d g u) = let
+      uni : R a m
+      uni = unity
+      prf : forall t. FoldableV t => (fo : t a) -> runR (r <.> uni) fo = runR r fo
+      prf fo = rewrite runRRingDistributive r uni fo
+            in unityIsRingIdL (d (foldr g u fo))
+    in foldExtensionality (r <.> uni) r prf
+  unityIsRingIdR r@(MkR d g u) = let
+      uni : R a m
+      uni = unity
+      prf : forall t. FoldableV t => (fo : t a) -> runR (uni <.> r) fo = runR r fo
+      prf fo = rewrite runRRingDistributive uni r fo
+            in unityIsRingIdR (d (foldr g u fo))
+    in foldExtensionality (uni <.> r) r prf
 
 ||| Convert an `L` to an `R`
+export
 lr : L a b -> R a b
 lr (MkL k h z) = MkR k (flip h) z
 
 ||| Convert an `R` to an `L`
+export
 rl : R a b -> L a b
 rl (MkR k h z) = MkL k (flip h) z
diff --git a/src/Data/Profunctor/Grate.idr b/src/Data/Profunctor/Grate.idr
new file mode 100644
index 0000000..bed7e43
--- /dev/null
+++ b/src/Data/Profunctor/Grate.idr
@@ -0,0 +1,26 @@
+module Data.Profunctor.Grate
+
+import Data.Morphisms
+import Data.Profunctor
+import Data.Profunctor.Closed
+import Data.Profunctor.Iso
+
+public export
+Grate : {p : Type -> Type -> Type} -> Type -> Type -> Type -> Type -> Type
+Grate s t a b = Closed p => preIso {p} s t a b
+
+public export
+Grate' : {p : Type -> Type -> Type} -> Type -> Type -> Type
+Grate' s a = Simple (Grate {p}) s a
+
+export
+grate : (((s -> a) -> b) -> t) -> Grate {p=Morphism} s t a b
+grate f pab = dimap (flip apply) f (closed pab)
+
+export
+zipWithOf : Grate {p=Zipping} s t a b -> (a -> a -> b) -> s -> s -> t
+zipWithOf gr = runZipping . gr . MkZipping
+
+export
+zipFWithOf : Functor f => Grate {p=DownStarred f} s t a b -> (f a -> b) -> (f s -> t)
+zipFWithOf gr = runDownStar . gr . DownStar
diff --git a/src/Data/Profunctor/Iso.idr b/src/Data/Profunctor/Iso.idr
index ea8a93a..e46f07f 100644
--- a/src/Data/Profunctor/Iso.idr
+++ b/src/Data/Profunctor/Iso.idr
@@ -1,13 +1,13 @@
 module Data.Profunctor.Iso
 
+import Data.Either
 import Data.Profunctor
 
-%access public export
+infixl 1 .&
 
-infixl 1 &
-
-(&) : a -> (a -> b) -> b
-a & f = f a
+export
+(.&) : a -> (a -> b) -> b
+a .& f = f a
 
 ||| A type-level function to make it easier to talk about "simple" `Lens`,
 ||| `Prism`, and `Iso`s
@@ -17,85 +17,110 @@ a & f = f a
 ||| fstStrLens = _1
 ||| ````
 |||
+public export
 Simple : (Type -> Type -> Type -> Type -> Type) -> Type -> Type -> Type
 Simple t s a = t s s a a
 
+public export
 preIso : {p : Type -> Type -> Type} -> Type -> Type -> Type -> Type -> Type
-preIso {p} s t a b = p a b -> p s t
+preIso s t a b = p a b -> p s t
 
 ||| An isomorphism family.
-Iso : Profunctor p => Type -> Type -> Type -> Type -> Type
-Iso {p} = preIso {p}
+public export
+Iso : {p : Type -> Type -> Type} -> Type -> Type -> Type -> Type -> Type
+Iso s t a b = Profunctor p => preIso {p} s t a b
 
 ||| An isomorphism family that does not change types
-Iso' : Profunctor p => Type -> Type -> Type
-Iso' {p} = Simple $ Iso {p}
+public export
+Iso' : {p : Type -> Type -> Type} -> Type -> Type -> Type
+Iso' s a = Simple (Iso {p}) s a
 
 ||| Turns a coavariant and contravariant function into an `Iso`
-iso : Profunctor p => (s -> a) -> (b -> t) -> Iso {p} s t a b
-iso = dimap
+export
+iso : (s -> a) -> (b -> t) -> Iso s t a b
+iso f g = dimap f g
 
 ||| Builds an `Iso` useful for constructing a `Lens`
-lensIso : Profunctor p =>
-          (s -> a) -> (s -> b -> t) -> Iso {p} s t (a, s) (b, s)
+export
+lensIso : (s -> a) -> (s -> b -> t) -> Iso s t (a, s) (b, s)
 lensIso gt = iso (\s => (gt s, s)) . uncurry . flip
 
 ||| Builds an `Iso` useful for constructing a `Prism`
-prismIso : Profunctor p => (b -> t) -> (s -> Either t a) ->
-                           Iso {p} s t (Either t a) (Either t b)
-prismIso = flip iso . either id . Delay
+export
+prismIso : (b -> t) -> (s -> Either t a) -> Iso s t (Either t a) (Either t b)
+prismIso f = flip iso $ either id $ Delay f
 
 ||| Convert an element of the first half of an iso to the second
+export
 forwards : Profunctor p => Iso {p=Forgotten a} s t a b -> s -> a
 forwards i = runForget . i $ Forget id
 
 ||| Convert an element of the second half of an iso to the first
+export
 backwards : Profunctor p => Iso {p=Tagged} s t a b -> b -> t
 backwards i = runTagged . i . Tag
 
 ||| An `Iso` between a function and it's arguments-flipped version
-flipped : Profunctor p => Iso {p} (a -> b -> c) (d -> e -> f)
-                                  (b -> a -> c) (e -> d -> f)
+export
+flipped : Iso (a -> b -> c) (d -> e -> f)
+              (b -> a -> c) (e -> d -> f)
 flipped = iso flip flip
 
 ||| An `Iso` between a function and it's curried version
-curried : Profunctor p => Iso {p} ((a, b) -> c) ((d, e) -> f)
-                                  (a -> b -> c) (d -> e -> f)
+export
+curried : Iso ((a, b) -> c) ((d, e) -> f)
+              (a -> b -> c) (d -> e -> f)
 curried = iso curry uncurry
 
 ||| An `Iso` between a function and it's uncurried version
-uncurried : Profunctor p => Iso {p} (a -> b -> c) (d -> e -> f)
-                                    ((a, b) -> c) ((d, e) -> f)
+export
+uncurried : Iso (a -> b -> c) (d -> e -> f)
+                ((a, b) -> c) ((d, e) -> f)
 uncurried = iso uncurry curry
 
 ||| An `Iso` between a list and its reverse
-reversed : Profunctor p => Iso {p} (List a) (List b) (List a) (List b)
+export
+reversed : Iso (List a) (List b) (List a) (List b)
 reversed = iso reverse reverse
 
 ||| An `Iso` between a string and a list of its characters
-packed : Profunctor p => Iso' {p} String (List Char)
+export
+packed : Iso' String (List Char)
 packed = iso unpack pack
 
 ||| An `Iso` between a list of characters and its string
-unpacked : Profunctor p => Iso' {p} (List Char) String
+export
+unpacked : Iso' (List Char) String
 unpacked = iso pack unpack
 
+snooze : a -> Lazy a
+snooze x = Delay x
+ring : Lazy b -> b
+ring x = Force x
+
 ||| An `Iso` between a lazy variable and its strict form
-motivated : Profunctor p => Iso {p} a b (Lazy a) (Lazy b)
-motivated = iso Delay Force
+export
+motivated : Iso a b (Lazy a) (Lazy b)
+motivated = iso snooze ring
 
 ||| An `Iso` between a strict variable and its lazy form
-unmotivated : Profunctor p => Iso {p} (Lazy a) (Lazy b) a b
-unmotivated = iso Force Delay
-
-||| An `Iso` between an enumerable value and it's `Nat` representation
-enum : (Profunctor p, Enum a) => Iso' {p} Nat a
-enum = iso fromNat toNat
-
-||| An `Iso` between a `Nat` and its enumerable representation
-denum : (Profunctor p, Enum a) => Iso' {p} a Nat
-denum = iso toNat fromNat
-
-mirrored : Profunctor p => Iso {p} (Either a b) (Either c d)
-                                   (Either b a) (Either d c)
+export
+unmotivated : Iso (Lazy a) (Lazy b) a b
+unmotivated = iso ring snooze
+
+-- TODO: Enum is currently commented out of base
+--
+-- ||| An `Iso` between an enumerable value and it's `Nat` representation
+-- export
+-- enum : (Profunctor p, Enum a) => Iso' {p} Nat a
+-- enum = iso fromNat toNat
+--
+-- ||| An `Iso` between a `Nat` and its enumerable representation
+-- export
+-- denum : (Profunctor p, Enum a) => Iso' {p} a Nat
+-- denum = iso toNat fromNat
+
+export
+mirrored : Iso (Either a b) (Either c d)
+               (Either b a) (Either d c)
 mirrored = iso mirror mirror
diff --git a/src/Data/Profunctor/Lens.idr b/src/Data/Profunctor/Lens.idr
index bec9906..498183b 100644
--- a/src/Data/Profunctor/Lens.idr
+++ b/src/Data/Profunctor/Lens.idr
@@ -2,129 +2,201 @@ module Data.Profunctor.Lens
 
 import Data.Fin
 import Data.HVect
+import Data.Morphisms
 import Data.Profunctor
+import Data.Profunctor.Strong
 import Data.Profunctor.Iso
 import Data.Vect
 
-%access public export
 
 ||| A `Strong` `Profunctor` that can be used in a `Lens`
-interface Strong p => Lensing (p : Type -> Type -> Type) where
+public export
+interface Strong p => Lensing (0 p : Type -> Type -> Type) where
   strength : p a b -> p (b -> t, a) t
   strength = (rmap $ uncurry id) . second'
 
+export
 implementation Lensing (Forgotten r) where
   strength (Forget ar) = Forget $ ar . snd
 
+export
 implementation Functor f => Lensing (UpStarred f) where
   strength (UpStar f) = UpStar . uncurry $ (. f) . (<$>)
 
-implementation Lensing Arr where
-  strength = MkArr . uncurry . flip (.) . runArr
+export
+implementation Lensing Morphism where
+  strength = Mor . uncurry . flip (.) . applyMor
 
 ||| A Lens family, strictly speaking, or a polymorphic lens.
-Lens : Lensing p => Type -> Type -> Type -> Type -> Type
-Lens {p} = preIso {p}
+public export
+Lens : {p : Type -> Type -> Type} -> Type -> Type -> Type -> Type -> Type
+Lens s t a b = Lensing p => preIso {p} s t a b
 
 ||| A Lens family that does not change types
-Lens' : Lensing p => Type -> Type -> Type
-Lens' {p} = Simple $ Lens {p}
+public export
+Lens' : {p : Type -> Type -> Type} -> Type -> Type -> Type
+Lens' s a = Simple (Lens {p}) s a
 
 ||| Build a `Lens` out of a function. Note this takes one argument, not two
-lens : Lensing p => (s -> (b -> t, a)) -> Lens {p} s t a b
-lens f = lmap f . strength
+export
+lens' : (s -> (b -> t, a)) -> Lens {p} s t a b
+lens' f = lmap f . strength
+
+||| Build a `Lens` out of getter and setter
+export
+lens : (s -> a) -> (s -> b -> t) -> Lens {p} s t a b
+lens gt st = lens' $ \s => (\b => st s b, gt s)
+
+export
+foldMapOf : Lens {p=Forgotten r} s t a b -> (a -> r) -> s -> r
+foldMapOf l f = runForget $ l $ Forget f
+
+export
+foldrOf : Lens {p=Forgotten (Endomorphism r)} s t a b -> (a -> r -> r) -> r -> s -> r
+foldrOf p f = flip $ applyEndo . foldMapOf p (Endo . f)
+
+public export
+Getter : Type -> Type -> Type -> Type -> Type
+Getter s t a = Lens {p=Forgotten a} s t a
 
 ||| Build a function to look at stuff from a Lens
-view : Lens {p=Forgotten a} s _ a _ -> s -> a
-view = runForget . (\f => f $ Forget id)
+export
+view : Getter s t a b -> s -> a
+view = runForget . go
+  where go : (Lensing (Forgotten a) =>
+             Forgotten a a b -> Forgotten a s t) -> Forgotten a s t
+        go f = f $ Forget id
+
+||| Create a getter from arbitrary function `s -> a`.
+export
+getter : (s -> a) -> Getter s t a b
+getter k (Forget aa) = Forget $ aa . k
+
+||| Combine two getters.
+export
+takeBoth : Getter s t a b -> Getter s t c d -> Getter s t (a, c) (b, d)
+takeBoth l r = getter $ \s =>  (view l s, view r s)
 
 infixl 8 ^.
 ||| Infix synonym for `view`
-(^.) : Lens {p=Forgotten a} s _ a _ -> s -> a
-(^.) = view
+export
+(^.) : s -> Getter s t a b -> a
+(^.) = flip view
+
+infixl 8 ^?
+export
+(^?) : s -> Lens {p=Forgotten $ Maybe a} s t a b -> Maybe a
+s ^? l = foldMapOf l Just s
 
 ||| Build a function to `map` from a Lens
-over : Lens {p=Arr} s t a b -> (a -> b) -> s -> t
-over = (runArr .) . (. MkArr)
+export
+over : Lens {p=Morphism} s t a b -> (a -> b) -> s -> t
+over = (applyMor .) . go
+  where go : (Lensing Morphism => Morphism a b -> Morphism s t) -> (a -> b) -> Morphism s t
+        go = (. Mor)
 
 infixr 4 &~
 ||| Infix synonym for `over`
-(&~) : Lens {p=Arr} s t a b -> (a -> b) -> s -> t
+export
+(&~) : Lens {p=Morphism} s t a b -> (a -> b) -> s -> t
 (&~) = over
 
+export
+sets : ((a -> b) -> s -> t) -> Lens {p=Morphism} s t a b
+sets l (Mor f) = Mor $ l f
+
 ||| Set something to a specific value with a Lens
-set : Lens {p=Arr} s t _ b -> b -> s -> t
+export
+set : Lens {p=Morphism} s t a b -> b -> s -> t
 set = (. const) . over
 
 infixr 4 .~
 ||| Infix synonym for `set`
-(.~) : Lens {p=Arr} s t _ b -> b -> s -> t
+export
+(.~) : Lens {p=Morphism} s t a b -> b -> s -> t
 (.~) = set
 
+export
+mapped : Functor f => Lens {p=Morphism} (f a) (f b) a b
+mapped = sets map
+
 infixr 4 +~
 ||| Increment the target of a lens by a number
-(+~) : Num a => Lens {p=Arr} s t a a -> a -> s -> t
+export
+(+~) : Num a => Lens {p=Morphism} s t a a -> a -> s -> t
 (+~) = (. (+)) . over
 
 infixr 4 -~
 ||| Decrement the target of a lens by a number
-(-~) : Neg a => Lens {p=Arr} s t a a -> a -> s -> t
+export
+(-~) : Neg a => Lens {p=Morphism} s t a a -> a -> s -> t
 (-~) = (. (-)) . over
 
 infixr 4 *~
 ||| Multiply the target of a lens by a number
-(*~) : Num a => Lens {p=Arr} s t a a -> a -> s -> t
+export
+(*~) : Num a => Lens {p=Morphism} s t a a -> a -> s -> t
 (*~) = (. (*)) . over
 
 infixr 4 /~
 ||| Divide the target of a lens by a number
-(/~) : Lens {p=Arr} s t Double Double -> Double -> s -> t
+export
+(/~) : Fractional a => Lens {p=Morphism} s t a a -> a -> s -> t
 (/~) = (. (/)) . over
 
 infixr 4 <+>~
 ||| Associatively combine the target of a Lens with another value
-(<+>~) : Semigroup a => Lens {p=Arr} s t a a -> a -> s -> t
+export
+(<+>~) : Semigroup a => Lens {p=Morphism} s t a a -> a -> s -> t
 (<+>~) = (. (<+>)) . over
 
 infixr 4 $>~
 ||| Rightwards sequence the target of a lens with an applicative
-($>~) : Applicative f => Lens {p=Arr} s t (f a) (f a) -> f a -> s -> t
+export
+($>~) : Applicative f => Lens {p=Morphism} s t (f a) (f a) -> f a -> s -> t
 ($>~) l = over l . (*>)
 
 infixr 4 <$~
 ||| Rightwards sequence the target of a lens with an applicative
-(<$~) : Applicative f => Lens {p=Arr} s t (f a) (f a) -> f a -> s -> t
+export
+(<$~) : Applicative f => Lens {p=Morphism} s t (f a) (f a) -> f a -> s -> t
 (<$~) l = over l . (<*)
 
 ||| A Lens for the first element of a tuple
-_1 : Lensing p => Lens {p} (a, b) (x, b) a x
-_1 = lens $ \(a,b) => (flip MkPair b, a)
+export
+l_1 : Lens {p} (a, b) (x, b) a x
+l_1 = lens' $ \(a,b) => (flip MkPair b, a)
 
 ||| A Lens for the second element of a tuple
-_2 : Lensing p => Lens {p} (b, a) (b, x) a x
-_2 = lens $ \(b,a) => (MkPair b, a)
+export
+l_2 : Lens {p} (b, a) (b, x) a x
+l_2 = lens' $ \(b,a) => (MkPair b, a)
 
 ||| A Lens for the first element of a non-empty vector
-_vCons : Lensing p => Lens {p} (Vect (S n) a) (Vect (S n) b)
-                               (a, Vect n a) (b, Vect n b)
-_vCons = lens $ \(x::xs) => (uncurry (::), (x,xs))
+export
+l_vCons : Lens {p} (Vect (S n) a) (Vect (S n) b)
+                  (a, Vect n a)  (b, Vect n b)
+l_vCons = lens' $ \(x::xs) => (uncurry (::), (x,xs))
 
 ||| A Lens for the nth element of a big-enough vector
-_vNth : Lensing p => {m : Nat} -> (n : Fin (S m)) ->
+export
+l_vNth : {m : Nat} -> (n : Fin (S m)) ->
         Lens {p} (Vect (S m) a) (Vect (S m) b) (a, Vect m a) (b, Vect m b)
-_vNth n = lens $ \v => (uncurry $ insertAt n, (index n v, deleteAt n v))
+l_vNth n = lens' $ \v => (uncurry $ insertAt n, (index n v, deleteAt n v))
 
 ||| A Lens for the nth element of a big-enough heterogenous vector
-_hVNth : Lensing p => (i : Fin (S l)) -> Lens {p} (HVect us) (HVect vs)
-                                              (index i us, HVect (deleteAt i us))
-                                              (index i vs, HVect (deleteAt i vs))
-_hVNth n = lens $ \v =>
+export
+l_hVNth : (i : Fin (S l)) -> Lens {p} (HVect us) (HVect vs)
+                                 (index i us, HVect (deleteAt i us))
+                                 (index i vs, HVect (deleteAt i vs))
+l_hVNth n = lens' $ \v =>
            (believe_me . uncurry (insertAt' n), (index n v, deleteAt n v)) where
-  insertAt' : (i : Fin (S l)) -> a -> HVect us -> HVect (insertAt i a us)
+  insertAt' : (i : Fin (S k)) -> a -> HVect ws -> HVect (insertAt i a ws)
   insertAt' FZ     y xs      = y :: xs
   insertAt' (FS k) y (x::xs) = x :: insertAt' k y xs
   insertAt' (FS k) y []      = absurd k
 
 ||| Everything has a `()` in it
-devoid : Lensing p => Lens' {p} a ()
-devoid = lens $ flip MkPair () . const
+export
+devoid : Lens' {p} a ()
+devoid = lens' $ flip MkPair () . const
diff --git a/src/Data/Profunctor/Lens/At.idr b/src/Data/Profunctor/Lens/At.idr
new file mode 100644
index 0000000..3cbca20
--- /dev/null
+++ b/src/Data/Profunctor/Lens/At.idr
@@ -0,0 +1,39 @@
+module Data.Profunctor.Lens.At
+
+import Data.Morphisms
+import Data.SortedMap
+import Data.SortedSet
+import Data.Profunctor
+import Data.Profunctor.Iso
+import Data.Profunctor.Lens
+import Data.Profunctor.Traversal.Index
+import Data.Profunctor.Wander
+
+%default total
+
+||| Allows adding and deleting elements from "container-like" types
+public export
+interface Index p m a b => At (0 p : Type -> Type -> Type) (0 m : Type) (0 a : Type) (0 b : Type) | m where
+  at : a -> Lens' {p} m (Maybe b)
+
+export
+At p (Maybe a) () a where
+  at () = id
+
+export
+Ord k => At p (SortedMap k v) k v where
+  at k = lens (lookup k) (\m => maybe (delete k m) (\v => insert k v m))
+
+export
+Ord a => At p (SortedSet a) a () where
+  at x = lens get (flip update)
+    where
+      get : SortedSet a -> Maybe ()
+      get xs = if contains x xs then Just () else Nothing
+      update : Maybe () -> SortedSet a -> SortedSet a
+      update Nothing = delete x
+      update (Just _) = insert x
+
+export
+sans : At Morphism m a b => a -> m -> m
+sans {m} k = at {p=Morphism} {m} k .~ Nothing 
diff --git a/src/Data/Profunctor/Monad.idr b/src/Data/Profunctor/Monad.idr
new file mode 100644
index 0000000..6b18415
--- /dev/null
+++ b/src/Data/Profunctor/Monad.idr
@@ -0,0 +1,64 @@
+module Data.Profunctor.Monad
+
+import Control.Category
+import Control.Comonad
+
+import Data.Profunctor
+import Data.Profunctor.Cayley
+import Data.Profunctor.Closed
+import Data.Profunctor.Composition
+import Data.Profunctor.Ran
+
+public export
+interface ProfunctorFunctor (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
+  promap : (forall a, b. p a b -> q a b) -> t p a b -> t q a b
+
+export
+implementation ProfunctorFunctor (Ran p) where
+  promap f (Run g) = Run (f . g)
+
+export
+implementation ProfunctorFunctor (Rifted p) where
+  promap f (Rift g) = Rift (f . g)
+
+export
+implementation ProfunctorFunctor Closure where
+  promap f (Close p) = Close (f p)
+
+export
+implementation ProfunctorFunctor Environment where
+  promap f (Environize l m r) = Environize l (f m) r
+
+export
+implementation Functor f => ProfunctorFunctor (Cayleyed f) where
+  promap f (Cayley p) = Cayley (f <$> p)
+
+export
+implementation ProfunctorFunctor (Procomposed p) where
+  promap f (Procompose p q) = Procompose p (f q)
+
+public export
+interface ProfunctorFunctor t => ProfunctorMonad t where
+  propure : Profunctor p => p a b -> t p a b
+  projoin : Profunctor p => t (t p) a b -> t p a b
+
+export
+implementation Category p => ProfunctorMonad (Procomposed p) where
+  propure = Procompose id
+  projoin (Procompose p (Procompose q r)) = Procompose (p . q) r
+
+export
+implementation (Functor f, Monad f) => ProfunctorMonad (Cayleyed f) where
+  propure = Cayley . pure
+  projoin (Cayley m) = Cayley $ m >>= runCayley 
+
+public export
+interface ProfunctorFunctor t => ProfunctorComonad t where
+  proextract : Profunctor p => t p a b -> p a b
+  produplicate : Profunctor p => t p a b -> t (t p) a b
+
+export
+implementation Comonad f => ProfunctorComonad (Cayleyed f) where
+  proextract (Cayley f) = extract f
+  produplicate (Cayley p) = Cayley (Cayley <$> duplicate p)
+
diff --git a/src/Data/Profunctor/Prism.idr b/src/Data/Profunctor/Prism.idr
index 0f412c2..dc23240 100644
--- a/src/Data/Profunctor/Prism.idr
+++ b/src/Data/Profunctor/Prism.idr
@@ -1,97 +1,128 @@
 module Data.Profunctor.Prism
 
+import Data.Morphisms
+import Data.Maybe
 import Data.Profunctor
+import Data.Profunctor.Choice
 import Data.Profunctor.Iso
 
-%access public export
-
 ||| A `Choice` `Profunctor` that can be used in a `Prism`
-interface Choice p => Prisming (p : Type -> Type -> Type) where
+public export
+interface Choice p => Prisming (0 p : Type -> Type -> Type) where
   costrength : p a b -> p (Either b a) b
   costrength = rmap (either id id) . right'
 
-implementation Prisming Arr where
-  costrength = MkArr . either id . Delay . runArr
+export
+implementation Prisming Morphism where
+  costrength = Mor . either id . (\x => Delay x) . applyMor
 
+export
 implementation Monoid r => Prisming (Forgotten r) where
   costrength p = Forget . either (const neutral) $ runForget p
 
+export
 implementation Applicative f => Prisming (UpStarred f) where
   costrength p = UpStar . either pure $ runUpStar p
 
+export
 implementation Prisming Tagged where
   costrength = Tag . runTagged
 
 ||| A `Lens` for sum types instead of product types
-Prism : Prisming p => Type -> Type -> Type -> Type -> Type
-Prism {p} = preIso {p}
+public export
+Prism : {p : Type -> Type -> Type} -> Type -> Type -> Type -> Type -> Type
+Prism s t a b = Prisming p => preIso {p} s t a b
 
 ||| A Prism that does not change types
-Prism' : Prisming p => Type -> Type -> Type
-Prism' {p} = Simple $ Prism {p}
+public export
+Prism' : {p : Type -> Type -> Type} -> Type -> Type -> Type
+Prism' s a = Simple (Prism {p}) s a
 
 ||| Build a `Prism` from two functions
-prism : Prisming p => (b -> t) -> (s -> Either t a) -> Prism {p} s t a b
+export
+prism : (b -> t) -> (s -> Either t a) -> Prism {p} s t a b
 prism f g = lmap g . costrength . rmap f
 
-prism' : Prisming p => (b -> s) -> (s -> Maybe a) -> Prism {p} s s a b
+export
+prism' : (b -> s) -> (s -> Maybe a) -> Prism {p} s s a b
 prism' f g = prism f $ \s => maybe (Left s) Right $ g s
 
+public export
 record First a where
   constructor MkFirst
   runFirst : Maybe a
 
+export
 implementation Semigroup (First a) where
   (MkFirst Nothing) <+> r = r
   l                 <+> _ = l
 
+export
 implementation Monoid (First a) where
   neutral = MkFirst Nothing
 
 ||| Build a function from a `Prism` to look at stuff
+export
 preview : Prism {p=Forgotten (First a)} s _ a _ -> s -> Maybe a
 preview l = runFirst . runForget (l . Forget $ MkFirst . Just)
 
 ||| Build a function from a `Prism` to `map`
-review : Prism {p=Tagged} _ t _ b -> b -> t
-review = (runTagged .) . (. Tag)
+export
+review : Prism {p=Tagged} s t a b -> b -> t
+review = (runTagged .) . go
+  where go : (Prisming Tagged => Tagged a b -> Tagged s t) -> b -> Tagged s t
+        go = (. Tag)
 
 ||| A `Prism` for the left half of an `Either`
-_l : Prisming p => Prism {p} (Either a c) (Either b c) a b
-_l = prism Left $ either Right (Left . Right)
+export
+p_l : Prism {p} (Either a c) (Either b c) a b
+p_l = prism Left $ either Right (Left . Right)
 
 ||| A `Prism` for the right half of an `Either`
-_r : Prisming p => Prism {p} (Either c a) (Either c b) a b
-_r = prism Right $ either (Left . Left) Right
+export
+p_r : Prism {p} (Either c a) (Either c b) a b
+p_r = prism Right $ either (Left . Left) Right
 
 ||| A `Prism` for the just case of a `Maybe`
-_j : Prisming p => Prism {p} (Maybe a) (Maybe b) a b
-_j = prism Just $ maybe (Left Nothing) Right
+export
+p_j : Prism {p} (Maybe a) (Maybe b) a b
+p_j = prism Just $ maybe (Left Nothing) Right
 
 ||| A `Prism` for the nothing case of a `Maybe`
-_n : Prisming p => Prism' {p} (Maybe a) ()
-_n = prism' (const Nothing) . maybe (Just ()) $ const Nothing
+export
+p_n : Prism' {p} (Maybe a) ()
+p_n = prism' (const Nothing) . maybe (Just ()) $ const Nothing
 
 ||| A `Prism` for the left side of a `List`
-_lCons : Prisming p => Prism {p} (List a) (List b) (a, List a) (b, List b)
-_lCons = prism (uncurry (::)) $ \aas => case aas of
+export
+p_lCons : Prism {p} (List a) (List b) (a, List a) (b, List b)
+p_lCons = prism (uncurry (::)) $ \aas => case aas of
                                              (a::as) => Right (a, as)
                                              []      => Left  []
 
 ||| A `Prism` for the left side of a `String`
-_strCons : Prisming p => Prism' {p} String (Char, String)
-_strCons = prism (uncurry strCons) $ \aas => case unpack aas of
+export
+p_strCons : Prism' {p} String (Char, String)
+p_strCons = prism (uncurry strCons) $ \aas => case unpack aas of
                                                   (a::as) => Right (a, pack as)
                                                   []      => Left  ""
 
 ||| A prism for equality
-only : (Eq a, Prisming p) => a -> Prism' {p} a ()
+export
+only : Eq a => a -> Prism' {p} a ()
 only a = prism (const a) $ \x => if x == a then Left x else Right ()
 
 ||| A prism for near-equality, as determined by a given predicate
-nearly : Prisming p => a -> (a -> Bool) -> Prism' {p} a ()
+export
+nearly : a -> (a -> Bool) -> Prism' {p} a ()
 nearly a p = prism (const a) $ if p a then Left else const $ Right ()
 
+||| Checks whether an object would match a given `Prism`
+export
+is : Prism {p=Forgotten (First a)} s _ a _ -> s -> Bool
+is = (isJust .) . preview
+
 ||| Checks whether an object won't match a given `Prism`
+export
 isn't : Prism {p=Forgotten (First a)} s _ a _ -> s -> Bool
 isn't = (isNothing .) . preview
diff --git a/src/Data/Profunctor/Ran.idr b/src/Data/Profunctor/Ran.idr
index 02be56b..d274d60 100644
--- a/src/Data/Profunctor/Ran.idr
+++ b/src/Data/Profunctor/Ran.idr
@@ -2,23 +2,26 @@ module Data.Profunctor.Ran
 
 import Data.Profunctor
 import Data.Profunctor.Composition
-import Data.Profunctor.Monad
-
-%access public export
 
 ||| The right Kan extension of a profunctor
-record Ran : (Type -> Type -> Type) -> (Type -> Type -> Type) ->
-             Type -> Type -> Type where
-  Run : {x : _} -> (runRan : p x a -> q x b) -> Ran p q a b
+public export
+record Ran (p : Type -> Type -> Type) (q : Type -> Type -> Type)
+           (a : Type) (b : Type) where
+  -- Run : {x : _} -> (runRan : p x a -> q x b) -> Ran p q a b
+  constructor Run
+  runRan : p x a -> q x b
 
+export
 implementation (Profunctor p, Profunctor q) => Profunctor (Ran p q) where
   dimap ca bd f = Run $ rmap bd . runRan f . rmap ca
   lmap  ca    f = Run $           runRan f . rmap ca
   rmap     bd f = Run $ rmap bd . runRan f
 
+export
 implementation Profunctor q => Functor (Ran p q a) where
   map bd f = Run $ rmap bd . runRan f
 
 ||| Split up composed Profunctors by putting a Ran in the middle
-curryRan : (Procomposed p q -/-> r) -> p -/-> Ran q r
-curryRan f a b p = Run $ \q => f a b $ Procompose p q
+export
+curryRan : (Procomposed p q a b -> r a b) -> p a b -> Ran q r a b
+curryRan fpro pab = Run $ \qaa => fpro (Procompose pab qaa)
diff --git a/src/Data/Profunctor/Rep.idr b/src/Data/Profunctor/Rep.idr
new file mode 100644
index 0000000..7db14ec
--- /dev/null
+++ b/src/Data/Profunctor/Rep.idr
@@ -0,0 +1,47 @@
+module Data.Profunctor.Rep
+
+import Control.Applicative.Const
+import Control.Monad.Identity
+import Data.Morphisms
+
+import Data.Profunctor
+import Data.Profunctor.Iso
+import Data.Profunctor.Sieve
+import Data.Profunctor.Strong
+
+public export
+interface (Sieve p q, Strong p) => Representable p q where
+  tabulate : (d -> q c) -> p d c
+
+export
+implementation Representable Morphism Identity where
+  tabulate f = Mor $ runIdentity . f
+
+export
+implementation (Monad m, Functor m) => Representable (Kleislimorphism m) m where
+  tabulate = Kleisli
+
+export
+implementation Functor f => Representable (UpStarred f) f where
+  tabulate = UpStar
+
+export
+implementation Representable (Forgotten r) (Const r) where
+  tabulate = Forget . (runConst .)
+
+export
+tabulated : (Representable p f, Representable q g) => Iso (d -> f c) (d' -> g c') (p d c) (q d' c')
+tabulated = iso tabulate sieve
+
+export
+firstRep : Representable p (Pair a) => p a b -> p (a, c) (b, c)
+firstRep p = tabulate go
+  where go : (a, c) -> Pair a (Pair b c)
+        go (a, c) = (,c) <$> sieve p a
+
+export
+secondRep : Representable p (Pair c) => p a b -> p (c, a) (c, b)
+secondRep p = tabulate go
+  where go : (c, a) -> Pair c (Pair c b)
+        go (c, a) = (c,) <$> sieve p a
+
diff --git a/src/Data/Profunctor/Sieve.idr b/src/Data/Profunctor/Sieve.idr
new file mode 100644
index 0000000..f38f5a9
--- /dev/null
+++ b/src/Data/Profunctor/Sieve.idr
@@ -0,0 +1,50 @@
+module Data.Profunctor.Sieve
+
+import Control.Applicative.Const
+import Control.Monad.Identity
+import Data.Morphisms
+
+import Data.Profunctor
+import Data.Profunctor.Comonad
+import Data.Proxy
+
+public export
+interface (Profunctor p, Functor f) => Sieve p f where
+  sieve : p a b -> a -> f b
+
+export
+implementation Sieve Morphism Identity where
+  sieve f = Id . applyMor f
+
+export
+implementation (Monad m, Functor m) => Sieve (Kleislimorphism m) m where
+  sieve = applyKleisli
+
+export
+implementation Functor f => Sieve (UpStarred f) f where
+  sieve = runUpStar
+
+export
+implementation Sieve (Forgotten r) (Const r) where
+  sieve = (MkConst .) . runForget
+
+public export
+interface (Profunctor p, Functor f) => Cosieve p f where
+  cosieve : p a b -> f a -> b
+
+export
+implementation Cosieve Morphism Identity where
+  cosieve m (Id a) = applyMor m a
+
+export
+implementation Functor w => Cosieve (Cokleislimorphism w) w where
+  cosieve = runCokleisli
+
+export
+implementation Cosieve Tagged Proxy where
+  cosieve (Tag a) _ = a
+
+export
+implementation Functor f => Cosieve (DownStarred f) f where
+  cosieve = runDownStar
+
diff --git a/src/Data/Profunctor/Strong.idr b/src/Data/Profunctor/Strong.idr
new file mode 100644
index 0000000..2c7849c
--- /dev/null
+++ b/src/Data/Profunctor/Strong.idr
@@ -0,0 +1,57 @@
+module Data.Profunctor.Strong
+
+import Data.Profunctor
+import Data.Morphisms
+import Control.Arrow
+
+%default total
+
+-- }}}
+-- Strong
+-- {{{
+
+||| Generalized UpStar of a Strong Functor
+public export
+interface Profunctor p => Strong (0 p : Type -> Type -> Type) where
+  ||| Create a new Profunctor of tuples with first element from the original
+  |||
+  ||| ````idris example
+  ||| first' (Kleisli $ \x => Just $ reverse x)
+  ||| ````
+  |||
+  first'  : p a b -> p (a, c) (b, c)
+  first'  = dimap (\x => (snd x, fst x)) (\x => (snd x, fst x)) . second'
+
+  ||| Create a new Profunctor of tuples with second element from the original
+  |||
+  ||| ````idris example
+  ||| second' (Kleisli $ \x => Just $ reverse x)
+  ||| ````
+  |||
+  second' : p a b -> p (c, a) (c, b)
+  second' = dimap (\x => (snd x, fst x)) (\x => (snd x, fst x)) . first'
+
+export
+implementation Monad m => Strong (Kleislimorphism m) where
+  first'  (Kleisli f) = Kleisli $ \ac => f (fst ac) >>= \b => pure (b, snd ac)
+  second' (Kleisli f) = Kleisli $ \ca => f (snd ca) >>= pure . MkPair (fst ca)
+
+export
+implementation Strong Morphism where
+  first'  (Mor f) = Mor $ \(a,c) => (f a, c)
+  second' (Mor f) = Mor $ \(c,a) => (c, f a)
+
+export
+implementation Functor m => Strong (UpStarred m) where
+  first'  (UpStar f) = UpStar $ \ac => map (\b' => (b', snd ac)) . f $ fst ac
+  second' (UpStar f) = UpStar $ \ca => map (MkPair $    fst ca)  . f $ snd ca
+
+export
+implementation Arrow p => Strong (WrappedArrow p) where
+  first'  = WrapArrow . first  . unwrapArrow
+  second' = WrapArrow . second . unwrapArrow
+
+export
+implementation Strong (Forgotten r) where
+  first'  (Forget k) = Forget $ k . fst
+  second' (Forget k) = Forget $ k . snd
diff --git a/src/Data/Profunctor/Trace.idr b/src/Data/Profunctor/Trace.idr
index aa64e7a..45055f4 100644
--- a/src/Data/Profunctor/Trace.idr
+++ b/src/Data/Profunctor/Trace.idr
@@ -2,9 +2,8 @@ module Data.Profunctor.Trace
 
 import Data.Profunctor
 
-%access public export
-
 ||| Coend of Profunctor
+public export
 record Traced (f : Type -> Type -> Type) where
   constructor Trace
   runTrace : f a a
diff --git a/src/Data/Profunctor/Traversal.idr b/src/Data/Profunctor/Traversal.idr
new file mode 100644
index 0000000..c4bd82a
--- /dev/null
+++ b/src/Data/Profunctor/Traversal.idr
@@ -0,0 +1,26 @@
+module Data.Profunctor.Traversal
+
+import Data.Morphisms
+import Data.Profunctor
+import Data.Profunctor.Wander
+import Data.Profunctor.Iso
+import Control.Monad.Identity
+
+%default total
+
+public export
+Traversal : {p : Type -> Type -> Type} -> Type -> Type -> Type -> Type -> Type
+Traversal s t a b = Wander p => preIso {p} s t a b
+
+||| A Traversal that does not change types
+public export
+Traversal' : {p : Type -> Type -> Type} -> Type -> Type -> Type
+Traversal' s a = Simple (Traversal {p}) s a
+
+export
+traversed : Traversable t => Traversal {p} (t a) (t b) a b
+traversed = wander $ traverse
+
+export
+both : Bitraversable r => Traversal {p=Morphism} (r a a) (r b b) a b
+both (Mor f) = Mor $ runIdentity . bitraverse {f=Identity} (Id . f) (Id . f)
diff --git a/src/Data/Profunctor/Traversal/Index.idr b/src/Data/Profunctor/Traversal/Index.idr
new file mode 100644
index 0000000..6459af5
--- /dev/null
+++ b/src/Data/Profunctor/Traversal/Index.idr
@@ -0,0 +1,26 @@
+module Data.Profunctor.Traversal.Index
+
+import Data.SortedMap
+import Data.SortedSet
+import Data.Profunctor
+import Data.Profunctor.Iso
+import Data.Profunctor.Traversal
+import Data.Profunctor.Wander
+
+%default total
+
+public export
+interface Index (0 p : Type -> Type -> Type) (0 m : Type) (0 a : Type) (0 b : Type) | m where
+  ix : a -> Traversal' {p} m b
+
+export
+Index p (Maybe a) () a where
+  ix () = traversed
+
+export
+Ord k => Index p (SortedMap k v) k v where
+  ix k = wander $ \coalg, m => maybe (pure m) (map (\v => insert k v m) . coalg) (lookup k m)
+
+export
+Ord a => Index p (SortedSet a) a () where
+  ix x = wander $ \_ => pure . SortedSet.insert x
diff --git a/src/Data/Profunctor/Unsafe.idr b/src/Data/Profunctor/Unsafe.idr
index 612e5dc..d67d732 100644
--- a/src/Data/Profunctor/Unsafe.idr
+++ b/src/Data/Profunctor/Unsafe.idr
@@ -3,12 +3,11 @@ module Data.Profunctor.Unsafe
 import Data.Morphisms
 import Data.Profunctor
 
-%access public export
-
 infixr 9 #.
 infixl 8 .#
 
-interface Profunctor p => UnsafeProfunctor (p : Type -> Type -> Type) where
+public export
+interface Profunctor p => UnsafeProfunctor (0 p : Type -> Type -> Type) where
   ||| Map the second argument of a Profunctor covariantly with a function
   ||| which is assumed to be a cast
   (#.) : (b -> c) -> p a b -> p a c
@@ -19,13 +18,16 @@ interface Profunctor p => UnsafeProfunctor (p : Type -> Type -> Type) where
   (.#) : p b c -> (a -> b) -> p a c
   (.#) = flip lmap
 
-implementation UnsafeProfunctor Arr where
+export
+implementation UnsafeProfunctor Morphism where
   (#.) = const believe_me
   (.#) = const . believe_me
 
+export
 implementation Monad m => UnsafeProfunctor (Kleislimorphism m) where
   (.#) = const . believe_me
 
+export
 implementation UnsafeProfunctor Tagged where
   (#.) = const believe_me
   (.#) = const . Tag . runTagged
diff --git a/src/Data/Profunctor/Wander.idr b/src/Data/Profunctor/Wander.idr
new file mode 100644
index 0000000..af87fee
--- /dev/null
+++ b/src/Data/Profunctor/Wander.idr
@@ -0,0 +1,27 @@
+module Data.Profunctor.Wander
+
+import Control.Applicative.Const
+import Control.Monad.Identity
+import Data.Profunctor
+import Data.Profunctor.Strong
+import Data.Profunctor.Choice
+import Data.Morphisms
+
+%default total
+
+||| Profunctors that support polymorphic traversals
+public export
+interface (Strong p, Choice p) => Wander (0 p : Type -> Type -> Type) where
+  wander : ({0 f : Type -> Type} -> Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t
+
+export
+Wander Morphism where
+  wander t (Mor f) = Mor $ runIdentity . t (Id . f)
+
+export
+Applicative f => Wander (UpStarred f) where
+  wander t (UpStar u) = UpStar $ t u
+
+export
+Monoid r => Wander (Forgotten r) where
+  wander t (Forget f) = Forget $ runConst . t (MkConst . f)
diff --git a/src/Data/Proxy.idr b/src/Data/Proxy.idr
new file mode 100644
index 0000000..71fa181
--- /dev/null
+++ b/src/Data/Proxy.idr
@@ -0,0 +1,55 @@
+module Data.Proxy
+
+import Data.Contravariant
+
+public export
+record Proxy (a : Type) where
+  constructor MkProxy
+
+export
+implementation Eq (Proxy a) where
+  (==) _ _ = True
+
+export
+implementation Ord (Proxy a) where
+  compare _ _ = EQ
+
+export
+implementation Semigroup (Proxy a) where
+  (<+>) _ _ = MkProxy
+
+export
+implementation Monoid (Proxy a) where
+  neutral = MkProxy
+
+export
+implementation Functor Proxy where
+  map _ _ = MkProxy
+
+export
+implementation Applicative Proxy where
+  pure _ = MkProxy
+  (<*>) _ _ = MkProxy
+
+export
+implementation Monad Proxy where
+  (>>=) _ _ = MkProxy
+  join _ = MkProxy
+
+export
+implementation Foldable Proxy where
+  foldr _ z _ = z
+
+export
+implementation Traversable Proxy where
+  traverse _ _ = pure MkProxy
+
+export
+implementation Alternative Proxy where
+  empty = MkProxy
+  (<|>) _ _ = MkProxy
+
+export
+implementation Contravariant Proxy where
+  contramap _ _ = MkProxy
+
diff --git a/src/Data/Verified/Foldable.idr b/src/Data/Verified/Foldable.idr
new file mode 100644
index 0000000..8987cfc
--- /dev/null
+++ b/src/Data/Verified/Foldable.idr
@@ -0,0 +1,196 @@
+module Data.Verified.Foldable
+
+import Control.Applicative.Const
+import Control.Monad.Either
+import Control.Monad.Maybe
+import Data.List.Alternating
+import Data.List.Lazy
+import Data.List1
+import Data.SnocList
+import Data.SortedSet
+import Data.SortedMap
+import Data.Validated
+import Data.Vect
+import Data.Vect.Properties.Foldr
+import Text.Bounded
+
+%default total
+
+public export
+interface Foldable t => FoldableV t where
+  toListNeutralL : (f : r -> a -> r) -> (z : r) -> (fo : t a) -> foldl f z fo = foldl f z (Prelude.toList fo)
+  toListNeutralR : (f : a -> r -> r) -> (z : r) -> (fo : t a) -> foldr f z fo = foldr f z (Prelude.toList fo)
+
+export
+implementation FoldableV Maybe where
+  toListNeutralL f z Nothing  = Refl
+  toListNeutralL f z (Just x) = Refl
+  toListNeutralR f z Nothing  = Refl
+  toListNeutralR f z (Just x) = Refl
+
+export
+implementation FoldableV m => FoldableV (MaybeT m) where
+  toListNeutralL f z m@(MkMaybeT mm) = let
+                                      funEq : (x : c) -> (g : c -> d) -> (f : c -> d) -> g = f -> g x = f x
+                                      funEq x g f hyp = rewrite hyp in Refl
+                                    in rewrite funEq
+                                               z
+                                             ( foldr (\x, xs => maybe (Delay xs) (Delay (\arg, x => xs (f x arg))) x) id mm )
+                                             ( foldr (\x, xs => maybe (Delay xs) (Delay (\arg, x => xs (f x arg))) x) id (toList mm))
+                                             $ toListNeutralR (\x, xs => maybe (Delay xs) (Delay (\arg, x => xs (f x arg))) x) id mm
+                                    in rewrite toListNeutralR (\x, xs => maybe (Delay xs) (Delay (\arg => arg :: xs)) x) Prelude.Nil mm
+                                    in prf (toList mm) z
+                                    where prf : (l : List (Maybe a)) -> (zz : r)
+                                             -> foldr (\x, xs => maybe (Delay xs) (Delay (\arg, x => xs (f x arg))) x) Prelude.Basics.id l zz
+                                             = foldl f zz (foldr (\x,xs => maybe (Delay xs) (Delay (\arg => arg :: xs)) x) Prelude.Nil l)
+                                          prf [] = \_ => Refl
+                                          prf (Nothing::xs) = \zz => prf xs zz
+                                          prf (Just x ::xs) = \zz => prf xs (f zz x)
+  toListNeutralR f z (MkMaybeT mm) = rewrite toListNeutralR (\x, xs => maybe (Delay xs) (Delay (\arg => f arg xs)) x) z mm
+                                  in rewrite toListNeutralR (\x, xs => maybe (Delay xs) (Delay (\arg => arg :: xs)) x) Prelude.Nil mm
+                                  in prf (toList mm)
+                                  where prf : (l : List (Maybe a))
+                                           -> foldr (\x, xs => maybe (Delay xs) (Delay (\arg => f arg xs)) x) z l
+                                            = foldr f z (foldr (\x,xs => maybe (Delay xs) (Delay (\arg => arg :: xs)) x) Prelude.Nil l)
+                                        prf [] = Refl
+                                        prf (Nothing::xs) = prf xs
+                                        prf (Just x ::xs) = cong (f x) (prf xs)
+export
+implementation FoldableV (Either e) where
+  toListNeutralL f z (Left x)  = Refl
+  toListNeutralL f z (Right x) = Refl
+  toListNeutralR f z (Left x)  = Refl
+  toListNeutralR f z (Right x) = Refl
+
+export
+implementation FoldableV m => FoldableV (EitherT e m) where
+  toListNeutralL f z m@(MkEitherT mm) = let
+                                      funEq : (x : c) -> (g : c -> d) -> (f : c -> d) -> g = f -> g x = f x
+                                      funEq x g f hyp = rewrite hyp in Refl
+                                    in rewrite funEq
+                                               z
+                                             ( foldr (\x, xs => either (Delay (const xs)) (Delay (\arg, x => xs (f x arg))) x) id mm )
+                                             ( foldr (\x, xs => either (Delay (const xs)) (Delay (\arg, x => xs (f x arg))) x) id (toList mm))
+                                             $ toListNeutralR (\x, xs => either (Delay (const xs)) (Delay (\arg, x => xs (f x arg))) x) id mm
+                                    in rewrite toListNeutralR (\x, xs => either (Delay (const xs)) (Delay (\arg => arg :: xs)) x) Prelude.Nil mm
+                                    in prf (toList mm) z
+                                    where prf : (l : List (Either e a)) -> (zz : r)
+                                             -> foldr (\x, xs => either (Delay (const xs)) (Delay (\arg, x => xs (f x arg))) x) Prelude.Basics.id l zz
+                                             = foldl f zz (foldr (\x,xs => either (Delay (const xs)) (Delay (\arg => arg :: xs)) x) Prelude.Nil l)
+                                          prf [] = \_ => Refl
+                                          prf (Left e ::xs) = \zz => prf xs zz
+                                          prf (Right x::xs) = \zz => prf xs (f zz x)
+  toListNeutralR f z m@(MkEitherT mm) = rewrite toListNeutralR (\x, xs => either (Delay (const xs)) (Delay (\arg => f arg xs)) x) z mm
+                                     in rewrite toListNeutralR (\x, xs => either (Delay (const xs)) (Delay (\arg => arg :: xs)) x) Prelude.Nil mm
+                                     in prf (toList mm)
+                                     where prf : (l : List (Either e a))
+                                              -> foldr (\x, xs => either (Delay (const xs)) (Delay (\arg => f arg xs)) x) z l
+                                               = foldr f z (foldr (\x, xs => either (Delay (const xs)) (Delay (\arg => arg :: xs)) x) Prelude.Nil l)
+                                           prf [] = Refl
+                                           prf (Left e ::xs) = prf xs
+                                           prf (Right x::xs) = cong (f x) (prf xs)
+
+export
+implementation FoldableV List where
+  toListNeutralL f z fo = Refl
+  toListNeutralR f z fo = Refl
+
+export
+implementation FoldableV (Const a) where
+  toListNeutralL f z xs = Refl
+  toListNeutralR f z xs = Refl
+
+export
+implementation FoldableV List1 where
+  toListNeutralL f z (x ::: xs) = Refl
+  toListNeutralR f z (x ::: xs) = Refl
+
+export
+implementation FoldableV (Validated e) where
+  toListNeutralL f z (Valid x) = Refl
+  toListNeutralL f z (Invalid _) = Refl
+  toListNeutralR f z (Valid x) = Refl
+  toListNeutralR f z (Invalid _) = Refl
+
+export
+implementation FoldableV WithBounds where
+  toListNeutralL f z xs = Refl
+  toListNeutralR f z xs = Refl
+
+export
+implementation FoldableV (Vect n) where
+  toListNeutralL f z xs = let
+      foldlEmptyIndependent : (f : r -> a -> r) -> (xs : Vect m a) -> (z : r) -> foldl f z xs = foldl f z (toList xs)
+      foldlEmptyIndependent f Nil = \_ => Refl
+      foldlEmptyIndependent f (y :: ys) = let homomorphism = foldrVectHomomorphism.cons {A=a, F=(::), E=[]}
+                                       in \z => rewrite foldlEmptyIndependent f ys (f z y)
+                                             in cong (foldl f z) (sym (homomorphism y ys))
+    in foldlEmptyIndependent f xs z
+  toListNeutralR f z Nil = Refl
+  toListNeutralR f z (x :: xs) = let
+    vectHomomorphismCons = foldrVectHomomorphism.cons {A=a, F=(::), E=[]}
+    vectHomomorphismF = foldrVectHomomorphism.cons {A=a, F=f, E=z}
+    in rewrite vectHomomorphismCons x xs
+    in rewrite sym (toListNeutralR f z xs)
+    in vectHomomorphismF x xs
+
+namespace SortedSet
+  toListRedundant : (xs : List a) -> xs = foldr (::) [] xs
+  toListRedundant [] = Refl
+  toListRedundant (x::xs) = cong (x::) (toListRedundant xs)
+
+  export
+  implementation FoldableV SortedSet where
+    toListNeutralL f z xs = cong (foldl {t=List} f z) (toListRedundant (SortedSet.toList xs))
+    toListNeutralR f z xs = cong (foldr {t=List} f z) (toListRedundant (SortedSet.toList xs))
+
+  export
+  implementation FoldableV (SortedMap k) where
+    toListNeutralL f z xs = cong (foldl {t=List} f z) (toListRedundant (values xs))
+    toListNeutralR f z xs = cong (foldr {t=List} f z) (toListRedundant (values xs))
+
+export
+implementation FoldableV SnocList where
+  toListNeutralL f z sn = snocFoldlAsListFoldl f z sn
+  toListNeutralR f z sn = let
+    foldrListAppendDistributive : (f : a -> r -> r) -> (z : r) -> (l1, l2 : List a)
+                               -> foldr f (foldr f z l2) l1 = foldr f z (l1 ++ l2)
+    foldrListAppendDistributive f z [] = \_ => Refl
+    foldrListAppendDistributive f z (x::xs) = \li => cong (f x) (foldrListAppendDistributive f z xs li)
+
+    snocFoldrAsListFoldr : (f : a -> r -> r) -> (xs : SnocList a) -> (init : r) -> foldr f init xs = foldr f init (toList xs)
+    snocFoldrAsListFoldr f Lin = \_ => Refl
+    snocFoldrAsListFoldr f (xs :< x) = \init =>
+                                       rewrite snocFoldrAsListFoldr f xs (f x init)
+                                    in rewrite chipsAsListAppend xs [x]
+                                    in foldrListAppendDistributive f init (xs <>> []) [x]
+    in snocFoldrAsListFoldr f sn z
+
+export
+implementation FoldableV LazyList where
+  toListNeutralL f z xs = let
+      foldlEmptyIndependent : (f : r -> a -> r) -> (xs : LazyList a) -> (z : r) -> foldl f z xs = foldl f z (toList xs)
+      foldlEmptyIndependent f   []    = \_ => Refl
+      foldlEmptyIndependent f (y::ys) = \z => foldlEmptyIndependent f ys (f z y)
+    in foldlEmptyIndependent f xs z
+  toListNeutralR f z [] = Refl
+  toListNeutralR f z (x::xs) = cong (f x) (toListNeutralR f z xs)
+
+export
+implementation FoldableV (Odd b) where
+  toListNeutralL f z odd = let
+    foldlEmptyIndependent : (f : r -> a -> r) -> (xs : Odd b a) -> (z : r) -> foldl f z xs = foldl f z (toList xs)
+    foldlEmptyIndependent f (x :: xs) with (xs)
+      _ | Nil = \_ => Refl
+      _ | (y :: ys) with (ys)
+        _ | (n :: ns) with (ns)
+          _ | Nil = \_ => Refl
+          _ | (m :: ms) = \z => foldlEmptyIndependent f ms (f (f z y) m)
+    in foldlEmptyIndependent f odd z
+  toListNeutralR f z (x :: xs) with (xs)
+    _ | Nil = Refl
+    _ | (y :: ys) with (ys)
+      _ | (n :: ns) with (ns)
+        _ | Nil = Refl
+        _ | (m :: ms) = let rec = toListNeutralR f z ms in cong (f y) (cong (f m) (toListNeutralR f z ms))
+
diff --git a/src/Data/Verified/Profunctor.idr b/src/Data/Verified/Profunctor.idr
index f36ca2d..6733d53 100644
--- a/src/Data/Verified/Profunctor.idr
+++ b/src/Data/Verified/Profunctor.idr
@@ -2,10 +2,9 @@ module Data.Verified.Profunctor
 
 import Data.Profunctor
 
-%access public export
-
 ||| Verified Profunctors
 ||| A Profunctor for which identity and composition laws are verified
+public export
 interface Profunctor p => VerifiedProfunctor (p : Type -> Type -> Type) where
   profunctorIdentity : {a : Type} -> {b : Type} -> (x : p a b) -> dimap Basics.id Basics.id x = x
   profunctorComposition : {a : Type} -> {b : Type} -> {c : Type} ->