Data.Profunctor.Yoneda

Definitions

record Yoneda : (Type -> Type -> Type) -> Type -> Type -> Type

  The cofree profunctor given a data constructor with two type parameters.

Totality: total
Visibility: public export
Constructor: 

MkYoneda : ((x -> a) -> (b -> y) -> p x y) -> Yoneda p a b

Projection: 

.runYoneda : Yoneda p a b -> (x -> a) -> (b -> y) -> p x y

Hints:

Closed p => Closed (Yoneda p)

Cosieve p f => Cosieve (Yoneda p) f

Functor (Yoneda p a)

GenCostrong ten p => GenCostrong ten (Yoneda p)

GenStrong ten p => GenStrong ten (Yoneda p)

Mapping p => Mapping (Yoneda p)

Profunctor (Yoneda p)

ProfunctorComonad Yoneda

ProfunctorFunctor Yoneda

ProfunctorMonad Yoneda

Sieve p f => Sieve (Yoneda p) f

Traversing p => Traversing (Yoneda p)

.runYoneda : Yoneda p a b -> (x -> a) -> (b -> y) -> p x y

Totality: total
Visibility: public export

runYoneda : Yoneda p a b -> (x -> a) -> (b -> y) -> p x y

Totality: total
Visibility: public export

yonedaEqv : Profunctor p => p a b <=> Yoneda p a b

  A witness that `Yoneda p` and `p` are equivalent when `p` is a profunctor.

Totality: total
Visibility: public export

yonedaIso : (Profunctor q, Profunctor r) => Profunctor p => p (q a b) (r a' b') -> p (Yoneda q a b) (Yoneda r a' b')

Totality: total
Visibility: public export

data Coyoneda : (Type -> Type -> Type) -> Type -> Type -> Type

  The free profunctor given a data constructor with two type parameters.

Totality: total
Visibility: public export
Constructor: 

MkCoyoneda : (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b

Hints:

Closed p => Closed (Coyoneda p)

Cosieve p f => Cosieve (Coyoneda p) f

Functor (Coyoneda p a)

GenCostrong ten p => GenCostrong ten (Coyoneda p)

GenStrong ten p => GenStrong ten (Coyoneda p)

Mapping p => Mapping (Coyoneda p)

Profunctor (Coyoneda p)

ProfunctorComonad Coyoneda

ProfunctorFunctor Coyoneda

ProfunctorMonad Coyoneda

Sieve p f => Sieve (Coyoneda p) f

Traversing p => Traversing (Coyoneda p)

coyonedaEqv : Profunctor p => p a b <=> Coyoneda p a b

  A witness that `Coyoneda p` and `p` are equivalent when `p` is a profunctor.

Totality: total
Visibility: public export

coyonedaIso : (Profunctor q, Profunctor r) => Profunctor p => p (q a b) (r a' b') -> p (Coyoneda q a b) (Coyoneda r a' b')

Totality: total
Visibility: public export