Data.Profunctor.Functor

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.

Definitions

interface ProfunctorFunctor : ((Type -> Type -> Type) -> k -> k' -> Type) -> Type

  An endofunctor in the category of profunctors.
  
  Laws:
  * `promap id = id`
  * `promap g . promap f = promap (g . f)`

Parameters: t
Methods:

promap : Profunctor p => p :-> q -> t p :-> t q

  Lift a transformation between profunctors into the functor `t`.

Implementations:

ProfunctorFunctor (GenTambara ten)

ProfunctorFunctor (GenPastro ten)

ProfunctorFunctor Closure

ProfunctorFunctor Environment

promap : ProfunctorFunctor t => Profunctor p => p :-> q -> t p :-> t q

  Lift a transformation between profunctors into the functor `t`.

Totality: total
Visibility: public export

interface ProfunctorMonad : ((Type -> Type -> Type) -> Type -> Type -> Type) -> Type

  A monad in the category of profunctors.
  
  Laws:
  * `projoin . proreturn ≡ id`
  * `projoin . promap proreturn ≡ id`
  * `projoin . projoin ≡ projoin . promap projoin`

Parameters: t
Constraints: ProfunctorFunctor t
Methods:

propure : Profunctor p => p :-> t p

projoin : Profunctor p => t (t p) :-> t p

Implementations:

(Tensor ten i, Symmetric ten) => ProfunctorMonad (GenPastro ten)

ProfunctorMonad Environment

propure : ProfunctorMonad t => Profunctor p => p :-> t p

Totality: total
Visibility: public export

projoin : ProfunctorMonad t => Profunctor p => t (t p) :-> t p

Totality: total
Visibility: public export

interface ProfunctorComonad : ((Type -> Type -> Type) -> Type -> Type -> Type) -> Type

  A comonad in the category of profunctors.
  
  Laws:
  * `proextract . produplicate ≡ id`
  * `promap proextract . produplicate ≡ id`
  * `produplicate . produplicate ≡ promap produplicate . produplicate`

Parameters: t
Constraints: ProfunctorFunctor t
Methods:

proextract : Profunctor p => t p :-> p

produplicate : Profunctor p => t p :-> t (t p)

Implementations:

Tensor ten i => ProfunctorComonad (GenTambara ten)

ProfunctorComonad Closure

proextract : ProfunctorComonad t => Profunctor p => t p :-> p

Totality: total
Visibility: public export

produplicate : ProfunctorComonad t => Profunctor p => t p :-> t (t p)

Totality: total
Visibility: public export

interface ProfunctorAdjunction : ((Type -> Type -> Type) -> Type -> Type -> Type) -> ((Type -> Type -> Type) -> Type -> Type -> Type) -> Type

  An adjunction between endofunctors in the category of profunctors.
  
  Laws:
  * `counit . promap unit ≡ id`
  * `promap counit . unit ≡ id`

Parameters: l, r
Constraints: ProfunctorFunctor l, ProfunctorFunctor r
Methods:

prounit : Profunctor p => p :-> r (l p)

procounit : Profunctor p => l (r p) :-> p

Implementations:

ProfunctorAdjunction (GenPastro ten) (GenTambara ten)

ProfunctorAdjunction Environment Closure

prounit : ProfunctorAdjunction l r => Profunctor p => p :-> r (l p)

Totality: total
Visibility: public export

procounit : ProfunctorAdjunction l r => Profunctor p => l (r p) :-> p

Totality: total
Visibility: public export