Document everything

Data/Profunctor/Cayley.idr

@@ -11,6 +11,7 @@ import Data.Profunctor.Sieve
 
 -- NOTE: This may be better as a type synonym instead of a new type?
 
+||| A profunctor lifted into a functor.
 public export
 record Cayley {0 k1,k2,k3 : Type} f (p : k1 -> k2 -> k3) a b where
   constructor MkCayley

Data/Profunctor/Closed.idr

@@ -8,15 +8,34 @@ import Data.Profunctor.Strong
 %default total
 
 
+------------------------------------------------------------------------------
+-- Closed interface
+------------------------------------------------------------------------------
+
+
+||| Closed profunctors preserve the closed structure of a category.
+|||
+||| Laws:
+||| * `lmap (. f) . closed = rmap (. f) . closed`
+||| * `closed . closed = dimap uncurry curry . closed`
+||| * `dimap const ($ ()) . closed = id`
 public export
 interface Profunctor p => Closed p where
+  ||| The action of a closed profunctor.
   closed : p a b -> p (x -> a) (x -> b)
 
 
+------------------------------------------------------------------------------
+-- Implementations for existing types
+------------------------------------------------------------------------------
+
+
 export
 Closed Morphism where
   closed (Mor f) = Mor (f .)
 
+||| A named implementation of `Closed` for function types.
+||| Use this to avoid having to use a type wrapper like `Morphism`.
 export
 [Function] Closed (\a,b => a -> b) using Profunctor.Function where
   closed = (.)
@@ -30,6 +49,12 @@ export
 curry' : Closed p => p (a, b) c -> p a (b -> c)
 curry' = lmap (,) . closed
 
+
+------------------------------------------------------------------------------
+-- Closure
+------------------------------------------------------------------------------
+
+
 -- Helper functions for working with function types
 hither : (s -> (a, b)) -> (s -> a, s -> b)
 hither h = (fst . h, snd . h)
@@ -38,8 +63,8 @@ yon : (s -> a, s -> b) -> s -> (a,b)
 yon h s = (fst h s, snd h s)
 
 
--- Closure
+||| The comonad generated by the reflective subcategory of profunctors that
-
+||| implement `Closed`.
 public export
 record Closure p a b where
   constructor MkClosure
@@ -84,8 +109,13 @@ unclose : Profunctor q => p :-> Closure q -> p :-> q
 unclose f p = dimap const ($ ()) $ runClosure $ f p
 
 
+------------------------------------------------------------------------------
 -- Environment
+------------------------------------------------------------------------------
 
+
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `Closed`.
 public export
 data Environment : (p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkEnv : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b

Data/Profunctor/Costrong.idr

@@ -1,3 +1,14 @@
+||| This module defines profunctor costrength with respect to a particular
+||| monoidal structure.
+|||
+||| Since the homset profunctor (`Morphism`) is not costrong, very few
+||| profunctors implement this interface.
+|||
+||| Unlike Haskell's profunctors library, `Costrong` and `Cochoice` are here
+||| special cases of the interface `GenCostrong`, which defines costrength with
+||| respect to an arbitrary tensor product. When writing implementations for
+||| a profunctor, `GenCostrong Pair` and `GenCostrong Either` should be used instead
+||| of `Costrong` and `Cochoice` respectively.
 module Data.Profunctor.Costrong
 
 import Data.Morphisms
@@ -7,37 +18,71 @@ import Data.Profunctor.Types
 
 %default total
 
+
+------------------------------------------------------------------------------
+-- Costrength interface
+------------------------------------------------------------------------------
+
+
+||| Profunctor costrength with respect to a tensor product.
+|||
+||| These constraints are not required by the interface, but the tensor product
+||| `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`.
+|||
+||| Laws:
+||| * `costrongl = costrongr . dimap swap swap`
+||| * `costrongl . dimap unitr.rightToLeft unitr.leftToRight = id`
+||| * `costrongl . lmap (mapSnd f) = costrongl . rmap (mapSnd f)`
+||| * `costrongr . costrongr = costrongr . dimap assoc.leftToRight assoc.rightToLeft`
+|||
+||| @ ten The tensor product of the monoidal structure
 public export
 interface Profunctor p => GenCostrong (0 ten : Type -> Type -> Type) p where
+  ||| The left action of a costrong profunctor.
   costrongl : p (a `ten` c) (b `ten` c) -> p a b
+  ||| The right action of a costrong profunctor.
   costrongr : p (c `ten` a) (c `ten` b) -> p a b
 
 
+||| Profunctor costrength with respect to the product (`Pair`).
 public export
 Costrong : (p : Type -> Type -> Type) -> Type
 Costrong = GenCostrong Pair
 
+||| A special case of `costrongl` with constraint `Costrong`.
+||| This is useful if the typechecker has trouble inferring the tensor product.
 public export
 unfirst : Costrong p => p (a, c) (b, c) -> p a b
 unfirst = costrongl {ten=Pair}
 
+||| A special case of `costrongr` with constraint `Costrong`.
+||| This is useful if the typechecker has trouble inferring the tensor product.
 public export
 unsecond : Costrong p => p (c, a) (c, b) -> p a b
 unsecond = costrongr {ten=Pair}
 
+||| Profunctor costrength with respect to the coproduct (`Either`).
 public export
 Cochoice : (p : Type -> Type -> Type) -> Type
 Cochoice = GenCostrong Either
 
+||| A special case of `costrongl` with constraint `Cochoice`.
+||| This is useful if the typechecker has trouble inferring the tensor product.
 public export
 unleft : Cochoice p => p (Either a c) (Either b c) -> p a b
 unleft = costrongl {ten=Either}
 
+||| A special case of `costrongr` with constraint `Cochoice`.
+||| This is useful if the typechecker has trouble inferring the tensor product.
 public export
 unright : Cochoice p => p (Either c a) (Either c b) -> p a b
 unright = costrongr {ten=Either}
 
--- Implementations
+
+------------------------------------------------------------------------------
+-- Implementations for existing types
+------------------------------------------------------------------------------
+
 
 export
 GenCostrong Pair Tagged where
@@ -45,8 +90,13 @@ GenCostrong Pair Tagged where
   costrongr (Tag (_,x)) = Tag x
 
 
--- Tambara
+------------------------------------------------------------------------------
+-- Cotambara
+------------------------------------------------------------------------------
 
+
+||| The comonad generated by the reflective subcategory of profunctors that
+||| implement `GenCostrong ten`.
 public export
 data GenCotambara : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b
@@ -76,43 +126,39 @@ Functor (GenCotambara ten p a) where
   map = rmap
 
 
-export
+||| The comonad generated by the reflective subcategory of profunctors that
-gencotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q
+||| implement `Costrong`.
-gencotambara f = MkCotambara f
+|||
-
+||| This is a special case of `GenCotambara`.
-export
-ungencotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q
-ungencotambara f p = proextract (f p)
-
-
 public export
 Cotambara : (p : Type -> Type -> Type) -> Type -> Type -> Type
 Cotambara = GenCotambara Pair
 
-export
+||| The comonad generated by the reflective subcategory of profunctors that
-cotambara : Costrong p => p :-> q -> p :-> Cotambara q
+||| implement `Cochoice`.
-cotambara = gencotambara
+|||
-
+||| This is a special case of `GenCotambara`.
-export
-uncotambara : Profunctor q => p :-> Cotambara q -> p :-> q
-uncotambara = ungencotambara
-
-
 public export
 CotambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
 CotambaraSum = GenCotambara Either
 
-export
-cotambaraSum : Cochoice p => p :-> q -> p :-> CotambaraSum q
-cotambaraSum = gencotambara
 
 export
-uncotambaraSum : Profunctor q => p :-> CotambaraSum q -> p :-> q
+cotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q
-uncotambaraSum = ungencotambara
+cotambara f = MkCotambara f
+
+export
+uncotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q
+uncotambara f p = proextract (f p)
 
 
+------------------------------------------------------------------------------
 -- Copastro
+------------------------------------------------------------------------------
 
+
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `GenCostrong ten`.
 public export
 record GenCopastro (ten, p : Type -> Type -> Type) a b where
   constructor MkCopastro
@@ -144,10 +190,18 @@ ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where
   procounit (MkCopastro h) = proextract (h id)
 
 
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `Costrong`.
+|||
+||| This is a special case of `GenCopastro`.
 public export
 Copastro : (p : Type -> Type -> Type) -> Type -> Type -> Type
 Copastro = GenCopastro Pair
 
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `Cochoice`.
+|||
+||| This is a special case of `GenCopastro`.
 public export
 CopastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
 CopastroSum = GenCopastro Either

Data/Profunctor/Functor.idr

@@ -1,3 +1,6 @@
+||| This module defines endofunctors in the category of profunctors `[Idrᵒᵖ * Idr, Idr]`,
+||| along with adjunctions of those functors.
+||| Examples of these functors include `Yoneda`, `Pastro`, `Closure`, etc.
 module Data.Profunctor.Functor
 
 import Data.Profunctor.Types
@@ -5,24 +8,48 @@ import Data.Profunctor.Types
 %default total
 
 
+||| An endofunctor in the category of profunctors.
+|||
+||| Laws:
+||| * `promap id = id`
+||| * `promap g . promap f = promap (g . f)`
 public export
 interface ProfunctorFunctor (0 t : (Type -> Type -> Type) -> k -> k' -> Type) where
+  ||| Lift a transformation between profunctors into the functor `t`.
   promap : Profunctor p => p :-> q -> t p :-> t q
 
+
+||| A monad in the category of profunctors.
+||| 
+||| Laws:
+||| * `projoin . proreturn ≡ id`
+||| * `projoin . promap proreturn ≡ id`
+||| * `projoin . projoin ≡ projoin . promap projoin`
 public export
 interface ProfunctorFunctor t =>
     ProfunctorMonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
   propure : Profunctor p => p :-> t p
   projoin : Profunctor p => t (t p) :-> t p
 
+||| A comonad in the category of profunctors.
+|||
+||| Laws:
+||| * `proextract . produplicate ≡ id`
+||| * `promap proextract . produplicate ≡ id`
+||| * `produplicate . produplicate ≡ promap produplicate . produplicate`
 public export
 interface ProfunctorFunctor t =>
     ProfunctorComonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
   proextract : Profunctor p => t p :-> p
   produplicate : Profunctor p => t p :-> t (t p)
 
+||| An adjunction between endofunctors in the category of profunctors.
+|||
+||| Laws:
+||| * `counit . promap unit ≡ id`
+||| * `promap counit . unit ≡ id`
 public export
-interface (ProfunctorFunctor f, ProfunctorFunctor u) =>
+interface (ProfunctorFunctor l, ProfunctorFunctor r) =>
-    ProfunctorAdjunction (0 f, u : (Type -> Type -> Type) -> Type -> Type -> Type) | f, u where
+    ProfunctorAdjunction (0 l, r : (Type -> Type -> Type) -> Type -> Type -> Type) | l, r where
-  prounit   : Profunctor p => p :-> u (f p)
+  prounit   : Profunctor p => p :-> r (l p)
-  procounit : Profunctor p => f (u p) :-> p
+  procounit : Profunctor p => l (r p) :-> p

Data/Profunctor/Mapping.idr

@@ -9,6 +9,18 @@ import Data.Profunctor.Traversing
 %default total
 
 
+------------------------------------------------------------------------------
+-- Mapping interface
+------------------------------------------------------------------------------
+
+
+||| The interface of profunctors that implement `roam`.
+|||
+||| Laws:
+||| * `map' . lmap f = lmap (map f) . map'`
+||| * `map' . rmap f = rmap (map f) . map'`
+||| * `map' . map' = map' @{Compose}`
+||| * `dimap Identity runIdentity . map' = id`
 public export
 interface (Traversing p, Closed p) => Mapping p where
   map' : Functor f => p a b -> p (f a) (f b)
@@ -21,11 +33,18 @@ interface (Traversing p, Closed p) => Mapping p where
       functor = MkFunctor (\f => (. (. f)))
 
 
+------------------------------------------------------------------------------
+-- Implementations for existing types
+------------------------------------------------------------------------------
+
+
 export
 Mapping Morphism where
   map' (Mor f) = Mor (map f)
   roam f (Mor x) = Mor (f x)
 
+||| A named implementation of `Mapping` for function types.
+||| Use this to avoid having to use a type wrapper like `Morphism`.
 export
 [Function] Mapping (\a,b => a -> b)
     using Traversing.Function Closed.Function where
@@ -33,6 +52,13 @@ export
   roam = id
 
 
+------------------------------------------------------------------------------
+-- Implementations for existing types
+------------------------------------------------------------------------------
+
+
+||| The comonad generated by the reflective subcategory of profunctors that
+||| implement `Mapping`.
 public export
 record CofreeMapping p a b where
   constructor MkCFM
@@ -83,8 +109,12 @@ Profunctor p => Mapping (CofreeMapping p) where
   map' (MkCFM p) = MkCFM (p @{Compose})
   roam = roamCofree
 
+------------------------------------------------------------------------------
+-- FreeMapping
+------------------------------------------------------------------------------
 
-
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `Mapping`.
 public export
 data FreeMapping : (p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkFM : Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b

Data/Profunctor/Representable.idr

@@ -9,15 +9,45 @@ import Data.Profunctor.Sieve
 %default total
 
 
+------------------------------------------------------------------------------
+-- Interfaces
+------------------------------------------------------------------------------
+
+
+||| A profunctor `p` is representable if it is isomorphic to `Star f` for some `f`.
 public export
 interface (Sieve p f, Strong p) => Representable p f | p where
   tabulate : (a -> f b) -> p a b
 
 
+||| A profunctor `p` is representable if it is isomorphic to `Costar f` for some `f`.
+public export
+interface Cosieve p f => Corepresentable p f | p where
+  cotabulate : (f a -> b) -> p a b
+
+
+export
+tabulated : (Representable q f, Representable r g) => forall p. Profunctor p =>
+              p (q a b) (r a' b') -> p (a -> f b) (a' -> g b')
+tabulated = dimap tabulate sieve
+
+export
+cotabulated : (Corepresentable q f, Corepresentable r g) => forall p. Profunctor p =>
+              p (q a b) (r a' b') -> p (f a -> b) (g a' -> b')
+cotabulated = dimap cotabulate cosieve
+
+
+------------------------------------------------------------------------------
+-- Implementations
+------------------------------------------------------------------------------
+
+
 export
 Representable Morphism Identity where
   tabulate f = Mor (runIdentity . f)
 
+||| A named implementation of `Representable` for function types.
+||| Use this to avoid having to use a type wrapper like `Morphism`.
 export
 [Function] Representable (\a,b => a -> b) Identity
     using Sieve.Function Strong.Function where
@@ -33,17 +63,7 @@ Functor f => Representable (Star f) f where
 
 
 export
-tabulated : (Representable q f, Representable r g) => forall p. Profunctor p =>
+Functor f => Corepresentable (Costar f) f where
-              p (q a b) (r a' b') -> p (a -> f b) (a' -> g b')
+  cotabulate = MkCostar
-tabulated = dimap tabulate sieve
 
 
-public export
-interface (Cosieve p f, Costrong p) => Corepresentable p f | p where
-  cotabulate : (f a -> b) -> p a b
-
-
-export
-cotabulated : (Corepresentable q f, Corepresentable r g) => forall p. Profunctor p =>
-              p (q a b) (r a' b') -> p (f a -> b) (g a' -> b')
-cotabulated = dimap cotabulate cosieve

Data/Profunctor/Sieve.idr

@@ -7,15 +7,34 @@ import Data.Profunctor
 %default total
 
 
+------------------------------------------------------------------------------
+-- Interfaces
+------------------------------------------------------------------------------
+
+
+||| A profunctor `p` is a sieve on `f` if it is a subprofunctor of `Star f`.
 public export
 interface (Profunctor p, Functor f) => Sieve p f | p where
   sieve : p a b -> a -> f b
 
 
+||| A profunctor `p` is a cosieve on `f` if it is a subprofunctor of `Costar f`.
+public export
+interface (Profunctor p, Functor f) => Cosieve p f | p where
+  cosieve : p a b -> f a -> b
+
+
+------------------------------------------------------------------------------
+-- Implementations
+------------------------------------------------------------------------------
+
+
 export
 Sieve Morphism Identity where
   sieve (Mor f) = Id . f
 
+||| A named implementation of `Sieve` for function types.
+||| Use this to avoid having to use a type wrapper like `Morphism`.
 export
 [Function] Sieve (\a,b => a -> b) Identity using Profunctor.Function where
   sieve = (Id .)
@@ -29,15 +48,14 @@ Functor f => Sieve (Star f) f where
   sieve = applyStar
 
 
-public export
-interface (Profunctor p, Functor f) => Cosieve p f | p where
-  cosieve : p a b -> f a -> b
 
 export
 Cosieve Morphism Identity where
   cosieve (Mor f) = f . runIdentity
 
 namespace Cosieve
+  ||| A named implementation of `Cosieve` for function types.
+  ||| Use this to avoid having to use a type wrapper like `Morphism`.
   export
   [Function] Cosieve (\a,b => a -> b) Identity using Profunctor.Function where
     cosieve = (. runIdentity)

Data/Profunctor/Strong.idr

@@ -1,3 +1,11 @@
+||| This module defines profunctor strength with respect to a particular
+||| monoidal structure.
+|||
+||| Unlike Haskell's profunctors library, `Strong` and `Choice` are here
+||| special cases of the interface `GenStrong`, which defines strength with
+||| respect to an arbitrary tensor product. When writing implementations for
+||| a profunctor, `GenStrong Pair` and `GenStrong Either` should be used instead
+||| of `Strong` and `Choice` respectively.
 module Data.Profunctor.Strong
 
 import Data.Morphisms
@@ -7,50 +15,92 @@ import Data.Profunctor.Types
 
 %default total
 
+
+------------------------------------------------------------------------------
+-- Strength interface
+------------------------------------------------------------------------------
+
+||| Profunctor strength with respect to a tensor product.
+||| A strong profunctor preserves the monoidal structure of a category.
+|||
+||| These constraints are not required by the interface, but the tensor product
+||| `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`.
+|||
+||| Laws:
+||| * `strongl = dimap swap swap . strongr`
+||| * `dimap unitr.rightToLeft unitr.leftToRight . strongl = id`
+||| * `lmap (mapSnd f) . strongl = rmap (mapSnd f) . strongl`
+||| * `strongr . strongr = dimap assoc.rightToLeft assoc.leftToRight . strongr`
+|||
+||| @ ten The tensor product of the monoidal structure
 public export
 interface Profunctor p => GenStrong (0 ten : Type -> Type -> Type) p where
+  ||| The left action of a strong profunctor.
   strongl : p a b -> p (a `ten` c) (b `ten` c)
+  ||| The right action of a strong profunctor.
   strongr : p a b -> p (c `ten` a) (c `ten` b)
 
 
+||| Profunctor strength with respect to the product (`Pair`).
 public export
 Strong : (p : Type -> Type -> Type) -> Type
 Strong = GenStrong Pair
 
+||| A special case of `strongl` with constraint `Strong`.
+||| This is useful if the typechecker has trouble inferring the tensor product.
+%inline
 public export
 first : Strong p => p a b -> p (a, c) (b, c)
 first = strongl {ten=Pair}
 
+||| A special case of `strongr` with constraint `Strong`.
+||| This is useful if the typechecker has trouble inferring the tensor product.
+%inline
 public export
 second : Strong p => p a b -> p (c, a) (c, b)
 second = strongr {ten=Pair}
 
+||| Profunctor strength with respect to the coproduct (`Either`).
 public export
 Choice : (p : Type -> Type -> Type) -> Type
 Choice = GenStrong Either
 
+||| A special case of `strongl` with constraint `Choice`.
+||| This is useful if the typechecker has trouble inferring the tensor product to use.
+%inline
 public export
 left : Choice p => p a b -> p (Either a c) (Either b c)
 left = strongl {ten=Either}
 
+||| A special case of `strongr` with constraint `Choice`.
+||| This is useful if the typechecker has trouble inferring the tensor product to use.
+%inline
 public export
 right : Choice p => p a b -> p (Either c a) (Either c b)
 right = strongr {ten=Either}
 
 
-
 export
 uncurry' : Strong p => p a (b -> c) -> p (a, b) c
 uncurry' = rmap (uncurry id) . first
 
+export
+strong : Strong p => (a -> b -> c) -> p a b -> p a c
+strong f = dimap dup (uncurry $ flip f) . first
+
+
+------------------------------------------------------------------------------
+-- Implementations for existing types
+------------------------------------------------------------------------------
 
--- Implementations
 
 export
 Bifunctor ten => GenStrong ten Morphism where
   strongl (Mor f) = Mor (mapFst f)
   strongr (Mor f) = Mor (mapSnd f)
 
+||| A named implementation of `GenStrong` for function types.
+||| Use this to avoid having to use a type wrapper like `Morphism`.
 export
 [Function] Bifunctor ten => GenStrong ten (\a,b => a -> b)
     using Profunctor.Function where
@@ -83,8 +133,13 @@ GenStrong Either Tagged where
   strongr (Tag x) = Tag (Right x)
 
 
+------------------------------------------------------------------------------
 -- Tambara
+------------------------------------------------------------------------------
 
+
+||| The comonad generated by the reflective subcategory of profunctors that
+||| implement `GenStrong ten`.
 public export
 record GenTambara (ten, p : Type -> Type -> Type) a b where
   constructor MkTambara
@@ -114,10 +169,18 @@ Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where
   map = rmap
 
 
+||| The comonad generated by the reflective subcategory of profunctors that
+||| implement `Strong`.
+|||
+||| This is a special case of `GenTambara`.
 public export
 Tambara : (p : Type -> Type -> Type) -> Type -> Type -> Type
 Tambara = GenTambara Pair
 
+||| The comonad generated by the reflective subcategory of profunctors that
+||| implement `Choice`.
+|||
+||| This is a special case of `GenTambara`.
 public export
 TambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
 TambaraSum = GenTambara Either
@@ -132,8 +195,13 @@ untambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q
 untambara f x = dimap unitr.rightToLeft unitr.leftToRight $ runTambara $ f x
 
 
+------------------------------------------------------------------------------
 -- Pastro
+------------------------------------------------------------------------------
 
+
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `GenStrong ten`.
 public export
 data GenPastro : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkPastro : (y `ten` z -> b) -> p x y -> (a -> x `ten` z) -> GenPastro ten p a b
@@ -181,10 +249,18 @@ export
       r' = mapSnd swap . assoc.rightToLeft . mapFst r . swap
 
 
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `Strong`.
+|||
+||| This is a special case of `GenPastro`.
 public export
 Pastro : (p : Type -> Type -> Type) -> Type -> Type -> Type
 Pastro = GenPastro Pair
 
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `Choice`.
+|||
+||| This is a special case of `GenPastro`.
 public export
 PastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
 PastroSum = GenPastro Either

Data/Profunctor/Traversing.idr

@@ -61,6 +61,20 @@ Traversable (Baz t b) where
   traverse f bz = map (\m => MkBaz (runBazaar m)) $ runBaz bz @{Compose} $ \x => sell <$> f x
 
 
+------------------------------------------------------------------------------
+-- Traversing interface
+------------------------------------------------------------------------------
+
+
+||| The interface of profunctors that implement `wander`.
+||| NOTE: Definitions in terms of `wander` are much more efficient!
+|||
+||| Laws:
+||| * `traverse' = wander traverse`
+||| * `traverse' . lmap f = lmap (map f) . traverse'`
+||| * `traverse' . rmap f = rmap (map f) . traverse'`
+||| * `traverse' . traverse' = traverse' @{Compose}`
+||| * `dimap Id runIdentity . traverse' = id`
 public export
 interface (Strong p, Choice p) => Traversing p where
   traverse' : Traversable f => p a b -> p (f a) (f b)
@@ -75,6 +89,8 @@ Traversing Morphism where
   traverse' (Mor f) = Mor (map f)
   wander f (Mor p) = Mor (runIdentity . (f $ Id . p))
 
+||| A named implementation of `Traversing` for function types.
+||| Use this to avoid having to use a type wrapper like `Morphism`.
 export
 [Function] Traversing (\a,b => a -> b) using Strong.Function where
   traverse' = map
@@ -91,9 +107,13 @@ Applicative f => Traversing (Star f) where
   wander f (MkStar p) = MkStar (f p)
 
 
-
+------------------------------------------------------------------------------
 -- CofreeTraversing
+------------------------------------------------------------------------------
 
+
+||| The comonad generated by the reflective subcategory of profunctors that
+||| implement `Traversing`.
 public export
 record CofreeTraversing p a b where
   constructor MkCFT
@@ -142,8 +162,13 @@ uncofreeTraversing : Profunctor q => p :-> CofreeTraversing q -> p :-> q
 uncofreeTraversing f p = proextract $ f p
 
 
+------------------------------------------------------------------------------
 -- FreeTraversing
+------------------------------------------------------------------------------
 
+
+||| The monad generated by the reflective subcategory of profunctors that
+||| implement `Traversing`.
 public export
 data FreeTraversing : (p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkFT : Traversable f => (f y -> b) -> p x y -> (a -> f x) -> FreeTraversing p a b

Data/Profunctor/Types.idr

@@ -1,3 +1,5 @@
+||| This module contains the Profunctor interface itself, along with a few
+||| examples of profunctors.
 module Data.Profunctor.Types
 
 import Data.Contravariant
@@ -6,26 +8,56 @@ import Data.Morphisms
 %default total
 
 
+------------------------------------------------------------------------------
+-- Profunctor interface
+------------------------------------------------------------------------------
+
+
+||| An interface for (self-enriched) profunctors `Idr -/-> Idr`.
+|||
+||| Formally, a profunctor is a binary functor that is contravariant in its
+||| first argument and covariant in its second. A common example of a profunctor
+||| is the (non-dependent) function type.
+|||
+||| Implementations can be defined by specifying either `dimap` or both `lmap`
+||| and `rmap`.
+|||
+||| Laws:
+||| * `dimap id id = id`
+||| * `dimap (f . g) (h . i) = dimap g h . dimap f i`
 public export
 interface Profunctor p where
 
+  ||| Map over both parameters of a profunctor at the same time, with the
+  ||| left function argument mapping contravariantly.
   dimap : (a -> b) -> (c -> d) -> p b c -> p a d
   dimap f g = lmap f . rmap g
 
+  ||| Map contravariantly over the first parameter of a profunctor.
   lmap : (a -> b) -> p b c -> p a c
   lmap f = dimap f id
 
+  ||| Map covariantly over the second parameter of a profunctor.
   rmap : (b -> c) -> p a b -> p a c
   rmap = dimap id
 
 
 infix 0 :->
+||| A transformation between profunctors that preserves their type parameters.
+|||
+||| Formally, this is a natural transformation of functors `Idrᵒᵖ * Idr => Idr`.
+|||
+||| If the transformation is `tr`, then we have the following law:
+||| * `tr . dimap f g = dimap f g . tr`
 public export
 0 (:->) : (p, q : k -> k' -> Type) -> Type
 p :-> q = forall a, b. p a b -> q a b
 
 
--- Instances for existing types
+------------------------------------------------------------------------------
+-- Implementations for existing types
+------------------------------------------------------------------------------
+
 
 export
 Profunctor Morphism where
@@ -34,6 +66,8 @@ Profunctor Morphism where
   rmap = map
 
 namespace Profunctor
+  ||| A named implementation of `Profunctor` for function types.
+  ||| Use this to avoid having to use a type wrapper like `Morphism`.
   export
   [Function] Profunctor (\a,b => a -> b) where
     dimap f g h = g . h . f
@@ -47,8 +81,15 @@ Functor f => Profunctor (Kleislimorphism f) where
   rmap = map
 
 
--- Examples of profunctors
+------------------------------------------------------------------------------
+-- Implementations for existing types
+------------------------------------------------------------------------------
 
+
+||| Lift a functor into a profunctor in the return type.
+|||
+||| This type is equivalent to `Kleislimorphism` except for the polymorphic type
+||| of `b`.
 public export
 record Star {0 k : Type} (f : k -> Type) a (b : k) where
   constructor MkStar
@@ -81,6 +122,7 @@ Functor f => Profunctor (Star f) where
   rmap f (MkStar g) = MkStar (map f . g)
 
 
+||| Lift a functor into a profunctor in the argument type.
 public export
 record Costar {0 k : Type} (f : k -> Type) (a : k) b where
   constructor MkCostar
@@ -106,11 +148,14 @@ Functor f => Profunctor (Costar f) where
   rmap f (MkCostar g) = MkCostar (f . g)
 
 
+||| The profunctor that ignores its argument type.
+||| Equivalent to `const id` up to isomorphism.
 public export
 record Tagged {0 k : Type} (a : k) b where
   constructor Tag
   runTagged : b
 
+||| Retag the value with a different type-level parameter.
 public export
 retag : Tagged a c -> Tagged b c
 retag (Tag x) = Tag x

Data/Profunctor/Yoneda.idr

@@ -9,6 +9,12 @@ import Data.Profunctor.Sieve
 %default total
 
 
+------------------------------------------------------------------------------
+-- Yoneda
+------------------------------------------------------------------------------
+
+
+||| The cofree profunctor given a data constructor with two type parameters.
 public export
 record Yoneda p a b where
   constructor MkYoneda
@@ -34,6 +40,7 @@ ProfunctorComonad Yoneda where
   proextract (MkYoneda p) = p id id
   produplicate p = MkYoneda $ \l,r => dimap l r p
 
+||| A witness that `Yoneda p` and `p` are equivalent when `p` is a profunctor.
 export
 yonedaEqv : Profunctor p => p a b <=> Yoneda p a b
 yonedaEqv = MkEquivalence propure proextract
@@ -75,6 +82,12 @@ Cosieve p f => Cosieve (Yoneda p) f where
   cosieve = cosieve . proextract
 
 
+------------------------------------------------------------------------------
+-- Coyoneda
+------------------------------------------------------------------------------
+
+
+||| The free profunctor given a data constructor with two type parameters.
 public export
 data Coyoneda : (p : Type -> Type -> Type) -> Type -> Type -> Type where
   MkCoyoneda : (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b
@@ -100,6 +113,7 @@ ProfunctorComonad Coyoneda where
   proextract (MkCoyoneda l r p) = dimap l r p
   produplicate = MkCoyoneda id id
 
+||| A witness that `Coyoneda p` and `p` are equivalent when `p` is a profunctor.
 export
 coyonedaEqv : Profunctor p => p a b <=> Coyoneda p a b
 coyonedaEqv = MkEquivalence propure proextract

Data/Tensor.idr

@@ -1,12 +1,29 @@
+||| This module defines tensor products, which are later used to define
+||| the concept of profunctor strength. The two primary tensor products
+||| in `Idr` are the product (`Pair`) and the coproduct (`Either`).
 module Data.Tensor
 
 %default total
 
 
+------------------------------------------------------------------------------
+-- Tensor products
+------------------------------------------------------------------------------
+
+
+||| A bifunctor that admits an *associator*, i.e. a bifunctor that is
+||| associative up to isomorphism.
+|||
+||| Laws:
+||| * `mapFst assoc.rightToLeft . assoc.leftToRight . assoc.leftToRight = assoc.leftToRight . mapSnd assoc.leftToRight`
 public export
 interface Bifunctor ten => Associative ten where
   assoc : a `ten` (b `ten` c) <=> (a `ten` b) `ten` c
 
+||| A bifunctor that admits a swap map, i.e. a bifunctor that is
+||| symmetric up to isomorphism.
+|||
+||| The bifunctor `ten` is generally also associative.
 public export
 interface Bifunctor ten => Symmetric ten where
   swap : a `ten` b -> b `ten` a
@@ -16,13 +33,23 @@ interface Bifunctor ten => Symmetric ten where
   symmetric = MkEquivalence swap swap
 
 
-
+||| A tensor product is an associative bifunctor that has an identity element
+||| up to isomorphism. Tensor products constitute the monoidal structure of a
+||| monoidal category.
+|||
+||| Laws:
+||| * `mapSnd unitl.leftToRight = mapFst unitr.leftToRight . assoc.leftToRight`
 public export
 interface Associative ten => Tensor ten i | ten where
   unitl : i `ten` a <=> a
   unitr : a `ten` i <=> a
 
 
+------------------------------------------------------------------------------
+-- Cartesian monoidal structure
+------------------------------------------------------------------------------
+
+
 export
 Associative Pair where
   assoc = MkEquivalence (\(x,(y,z)) => ((x,y),z)) (\((x,y),z) => (x,(y,z)))
@@ -37,6 +64,11 @@ Tensor Pair () where
   unitr = MkEquivalence fst (,())
 
 
+------------------------------------------------------------------------------
+-- Cocartesian monoidal structure
+------------------------------------------------------------------------------
+
+
 export
 Associative Either where
   assoc = MkEquivalence f b