Data.Tensor

(source)

This module defines tensor products, which are later used to define
the concept of profunctor strength. The two primary tensor products
in `Idr` are the product (`Pair`) and the coproduct (`Either`).

Definitions

interface Associative : (Type -> Type -> Type) -> Type

  A bifunctor that admits an *associator*, i.e. a bifunctor that is
  associative up to isomorphism.
  
  Laws:
  * `mapFst assocl . assocl . assocl = assocl . mapSnd assocl`

Parameters: ten
Constraints: Bifunctor ten
Methods:

assocl : ten a (ten b c) -> ten (ten a b) c
assocr : ten (ten a b) c -> ten a (ten b c)
assoc : ten a (ten b c) <=> ten (ten a b) c

Implementations:

Associative Pair
Associative Either

assocl : Associative ten => ten a (ten b c) -> ten (ten a b) c

Totality: total
Visibility: public export

assocr : Associative ten => ten (ten a b) c -> ten a (ten b c)

Totality: total
Visibility: public export

assoc : Associative ten => ten a (ten b c) <=> ten (ten a b) c

Totality: total
Visibility: public export

interface Symmetric : (Type -> Type -> Type) -> Type

  A bifunctor that admits a swap map, i.e. a bifunctor that is
  symmetric up to isomorphism.
  
  The bifunctor `ten` is generally also associative.

Parameters: ten
Constraints: Bifunctor ten
Methods:

swap' : ten a b -> ten b a
symmetric : ten a b <=> ten b a

Implementations:

Symmetric Pair
Symmetric Either

swap' : Symmetric ten => ten a b -> ten b a

Totality: total
Visibility: public export

symmetric : Symmetric ten => ten a b <=> ten b a

Totality: total
Visibility: public export

interface Tensor : (Type -> Type -> Type) -> Type -> Type

  A tensor product is an associative bifunctor that has an identity element
  up to isomorphism. Tensor products constitute the monoidal structure of a
  monoidal category.
  
  Laws:
  * `mapSnd unitl.leftToRight = mapFst unitr.leftToRight . assocl`

Parameters: ten, i
Constraints: Associative ten
Methods:

unitl : ten i a <=> a
unitr : ten a i <=> a

Implementations:

Tensor Pair ()
Tensor Either Void

unitl : Tensor ten i => ten i a <=> a

Totality: total
Visibility: public export

unitr : Tensor ten i => ten a i <=> a

Totality: total
Visibility: public export