Idris2Doc : Data.Profunctor.Cayley

Data.Profunctor.Cayley

(source)

Definitions

record Cayley : (k3 -> Type) -> (k1 -> k2 -> k3) -> k1 -> k2 -> Type
  A profunctor lifted into a functor.

Totality: total
Visibility: public export
Constructor: 
MkCayley : f (p a b) -> Cayley f p a b

Projection: 
.runCayley : Cayley f p a b -> f (p a b)

Hints:
Functor f => Closed p => Closed (Cayley f p)
Functor f => GenCostrong ten p => GenCostrong ten (Cayley f p)
Functor f => GenStrong ten p => GenStrong ten (Cayley f p)
Functor f => Mapping p => Mapping (Cayley f p)
Functor f => Profunctor p => Profunctor (Cayley f p)
Functor f => ProfunctorFunctor (Cayley f)
Monad m => ProfunctorMonad (Cayley m)
Functor g => Sieve p f => Sieve (Cayley g p) (g . f)
Functor f => Traversing p => Traversing (Cayley f p)
.runCayley : Cayley f p a b -> f (p a b)
Totality: total
Visibility: public export
runCayley : Cayley f p a b -> f (p a b)
Totality: total
Visibility: public export
mapCayley : (f x -> g x) -> Cayley f p :-> Cayley g p
Totality: total
Visibility: public export