Data.Profunctor.Costrong

This module defines profunctor costrength with respect to a particular
monoidal structure.

Since the homset profunctor (`Morphism`) is not costrong, very few
profunctors implement this interface.

Unlike Haskell's profunctors library, `Costrong` and `Cochoice` are here
special cases of the interface `GenCostrong`, which defines costrength with
respect to an arbitrary tensor product. When writing implementations for
a profunctor, `GenCostrong Pair` and `GenCostrong Either` should be used instead
of `Costrong` and `Cochoice` respectively.

Definitions

interface GenCostrong : (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type

  Profunctor costrength with respect to a tensor product.
  
  These constraints are not required by the interface, but the tensor product
  `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`.
  
  Laws:
  * `costrongl = costrongr . dimap swap' swap'`
  * `costrongl . dimap unitr.rightToLeft unitr.leftToRight = id`
  * `costrongl . lmap (mapSnd f) = costrongl . rmap (mapSnd f)`
  * `costrongr . costrongr = costrongr . dimap assocl assocr`
  
  @ ten The tensor product of the monoidal structure

Parameters: ten, p
Constraints: Profunctor p
Methods:

costrongl : p (ten a c) (ten b c) -> p a b

  The left action of a costrong profunctor.

costrongr : p (ten c a) (ten c b) -> p a b

  The right action of a costrong profunctor.

Implementations:

GenCostrong Pair Tagged

GenCostrong Either (Forget r)

GenCostrong Pair (Coforget r)

GenCostrong ten (GenCotambara ten p)

GenCostrong ten (GenCopastro ten p)

costrongl : GenCostrong ten p => p (ten a c) (ten b c) -> p a b

  The left action of a costrong profunctor.

Totality: total
Visibility: public export

costrongr : GenCostrong ten p => p (ten c a) (ten c b) -> p a b

  The right action of a costrong profunctor.

Totality: total
Visibility: public export

Costrong : (Type -> Type -> Type) -> Type

  Profunctor costrength with respect to the product (`Pair`).

Totality: total
Visibility: public export

unfirst : Costrong p => p (a, c) (b, c) -> p a b

  A special case of `costrongl` with constraint `Costrong`.
  This is useful if the typechecker has trouble inferring the tensor product.

Totality: total
Visibility: public export

unsecond : Costrong p => p (c, a) (c, b) -> p a b

  A special case of `costrongr` with constraint `Costrong`.
  This is useful if the typechecker has trouble inferring the tensor product.

Totality: total
Visibility: public export

Cochoice : (Type -> Type -> Type) -> Type

  Profunctor costrength with respect to the coproduct (`Either`).

Totality: total
Visibility: public export

unleft : Cochoice p => p (Either a c) (Either b c) -> p a b

  A special case of `costrongl` with constraint `Cochoice`.
  This is useful if the typechecker has trouble inferring the tensor product.

Totality: total
Visibility: public export

unright : Cochoice p => p (Either c a) (Either c b) -> p a b

  A special case of `costrongr` with constraint `Cochoice`.
  This is useful if the typechecker has trouble inferring the tensor product.

Totality: total
Visibility: public export

data GenCotambara : (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type

  The comonad generated by the reflective subcategory of profunctors that
  implement `GenCostrong ten`.

Totality: total
Visibility: public export
Constructor: 

MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b

Hints:

Functor (GenCotambara ten p a)

GenCostrong ten (GenCotambara ten p)

Profunctor (GenCotambara ten p)

ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten)

ProfunctorComonad (GenCotambara ten)

ProfunctorFunctor (GenCotambara ten)

Cotambara : (Type -> Type -> Type) -> Type -> Type -> Type

  The comonad generated by the reflective subcategory of profunctors that
  implement `Costrong`.
  
  This is a special case of `GenCotambara`.

Totality: total
Visibility: public export

CotambaraSum : (Type -> Type -> Type) -> Type -> Type -> Type

  The comonad generated by the reflective subcategory of profunctors that
  implement `Cochoice`.
  
  This is a special case of `GenCotambara`.

Totality: total
Visibility: public export

cotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q

Totality: total
Visibility: public export

uncotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q

Totality: total
Visibility: public export

record GenCopastro : (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type

  The monad generated by the reflective subcategory of profunctors that
  implement `GenCostrong ten`.

Totality: total
Visibility: public export
Constructor: 

MkCopastro : (GenCostrong ten q => p :-> q -> q a b) -> GenCopastro ten p a b

Projection: 

.runCopastro : GenCopastro ten p a b -> GenCostrong ten q => p :-> q -> q a b

Hints:

GenCostrong ten (GenCopastro ten p)

Profunctor (GenCopastro ten p)

ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten)

ProfunctorFunctor (GenCopastro ten)

ProfunctorMonad (GenCopastro ten)

.runCopastro : GenCopastro ten p a b -> GenCostrong ten q => p :-> q -> q a b

Totality: total
Visibility: public export

runCopastro : GenCopastro ten p a b -> GenCostrong ten q => p :-> q -> q a b

Totality: total
Visibility: public export

Copastro : (Type -> Type -> Type) -> Type -> Type -> Type

  The monad generated by the reflective subcategory of profunctors that
  implement `Costrong`.
  
  This is a special case of `GenCopastro`.

Totality: total
Visibility: public export

CopastroSum : (Type -> Type -> Type) -> Type -> Type -> Type

  The monad generated by the reflective subcategory of profunctors that
  implement `Cochoice`.
  
  This is a special case of `GenCopastro`.

Totality: total
Visibility: public export

copastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q

Totality: total
Visibility: public export

uncopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q

Totality: total
Visibility: public export