Idris2Doc : Data.Profunctor.Closed

Data.Profunctor.Closed

(source)
Definitions
interface Closed : (Type -> Type -> Type) -> Type
  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`

  Parameters: p
Constraints: Profunctor p
Methods:
  
closed : p a b -> p (x -> a) (x -> b)
  The action of a closed profunctor.

Implementations:
  
Closed Morphism
  
Functor f => Closed (Costar f)
  
Profunctor p => Closed (Closure p)
  
Closed (Environment p)
closed : Closed p => p a b -> p (x -> a) (x -> b)
  The action of a closed profunctor.

  Totality: total
  Visibility: public export
curry' : Closed p => p (a, b) c -> p a (b -> c)
  Totality: total
  Visibility: public export
record Closure : (Type -> Type -> Type) -> Type -> Type -> Type
  The comonad generated by the reflective subcategory of profunctors that
  implement `Closed`.

  Totality: total
  Visibility: public export
  Constructor: 
MkClosure : p (x -> a) (x -> b) -> Closure p a b

  Projection: 
.runClosure : Closure p a b -> p (x -> a) (x -> b)

  Hints:
  
Profunctor p => Closed (Closure p)
  
Profunctor p => Functor (Closure p a)
  
Strong p => GenStrong Pair (Closure p)
  
Profunctor p => Profunctor (Closure p)
  
ProfunctorAdjunction Environment Closure
  
ProfunctorComonad Closure
  
ProfunctorFunctor Closure
.runClosure : Closure p a b -> p (x -> a) (x -> b)
  Totality: total
  Visibility: public export
runClosure : Closure p a b -> p (x -> a) (x -> b)
  Totality: total
  Visibility: public export
close : Closed p => p :-> q -> p :-> Closure q
  Totality: total
  Visibility: public export
unclose : Profunctor q => p :-> Closure q -> p :-> q
  Totality: total
  Visibility: public export
data Environment : (Type -> Type -> Type) -> Type -> Type -> Type
  The monad generated by the reflective subcategory of profunctors that
  implement `Closed`.

  Totality: total
  Visibility: public export
  Constructor: 
MkEnv : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b

  Hints:
  
Closed (Environment p)
  
Profunctor p => Functor (Environment p a)
  
Profunctor (Environment p)
  
ProfunctorAdjunction Environment Closure
  
ProfunctorFunctor Environment
  
ProfunctorMonad Environment
environment : Closed q => p :-> q -> Environment p :-> q
  Totality: total
  Visibility: public export
unenvironment : Environment p :-> q -> p :-> q
  Totality: total
  Visibility: public export