Idris2Doc : Data.Profunctor.Mapping

Data.Profunctor.Mapping

(source)
Definitions
interface Mapping : (Type -> Type -> Type) -> Type
  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 Id runIdentity . map' = id`

  Parameters: p
Constraints: Traversing p, Closed p
Methods:
  
map' : Functor f => p a b -> p (f a) (f b)
  
roam : ((a -> b) -> s -> t) -> p a b -> p s t

Implementations:
  
Mapping Morphism
  
Profunctor p => Mapping (CofreeMapping p)
  
Mapping (FreeMapping p)
map' : Mapping p => Functor f => p a b -> p (f a) (f b)
  Totality: total
  Visibility: public export
roam : Mapping p => ((a -> b) -> s -> t) -> p a b -> p s t
  Totality: total
  Visibility: public export
record CofreeMapping : (Type -> Type -> Type) -> Type -> Type -> Type
  The comonad generated by the reflective subcategory of profunctors that
  implement `Mapping`.

  Totality: total
  Visibility: public export
  Constructor: 
MkCFM : (Functor f => p (f a) (f b)) -> CofreeMapping p a b

  Projection: 
.runCFM : CofreeMapping p a b -> Functor f => p (f a) (f b)

  Hints:
  
Profunctor p => Closed (CofreeMapping p)
  
Profunctor p => Functor (CofreeMapping p a)
  
Symmetric ten => Profunctor p => GenStrong ten (CofreeMapping p)
  
Profunctor p => Mapping (CofreeMapping p)
  
Profunctor p => Profunctor (CofreeMapping p)
  
ProfunctorComonad CofreeMapping
  
ProfunctorFunctor CofreeMapping
  
Profunctor p => Traversing (CofreeMapping p)
.runCFM : CofreeMapping p a b -> Functor f => p (f a) (f b)
  Totality: total
  Visibility: public export
runCFM : CofreeMapping p a b -> Functor f => p (f a) (f b)
  Totality: total
  Visibility: public export
data FreeMapping : (Type -> Type -> Type) -> Type -> Type -> Type
  The monad generated by the reflective subcategory of profunctors that
  implement `Mapping`.

  Totality: total
  Visibility: public export
  Constructor: 
MkFM : Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b

  Hints:
  
Closed (FreeMapping p)
  
Functor (FreeMapping p a)
  
GenStrong Pair (FreeMapping p)
  
GenStrong Either (FreeMapping p)
  
Mapping (FreeMapping p)
  
Profunctor (FreeMapping p)
  
ProfunctorFunctor FreeMapping
  
ProfunctorMonad FreeMapping
  
Traversing (FreeMapping p)