Data.Container.Base.Product.Definitions

Definitions

(>*<) : Cont -> Cont -> Cont

  Binary version of product

Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3

AllAny : List Cont -> Cont

  N-ary version of product

Visibility: public export

AllAny : Vect n Cont -> Cont

  N-ary version of product

Visibility: public export

DPairCart : (s : Cont) -> (s .Shp -> Cont) -> Cont

  "Dependent categorical product": 
  Dependent pair type for the categorical product of containers
  Given a container `s` and a family `p : s.Shp -> Cont`,
  form the container whose shapes are dependent pairs of shapes
  and a position is either a position of s or a position of p.

Visibility: public export

(><) : Cont -> Cont -> Cont

Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3

AllAny : List Cont -> Cont

  N-ary version of tensor product

Visibility: public export

AllAll : Vect n Cont -> Cont

  N-ary version of tensor product

Visibility: public export

(><) : c1 =%> d1 -> c2 =%> d2 -> (c1 >< c2) =%> (d1 >< d2)

  Action on morphisms

Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3

DPairTensor : (s : Cont) -> (s .Shp -> Cont) -> Cont

  "Dependent tensor product": 
  Dependent pair type for the tensor product of containers
  Given a container `s` and a family `p : s.Shp -> Cont`,
  form the container whose shapes are dependent pairs of shapes
  and positions are pairs of positions.

Visibility: public export

(>+<) : Cont -> Cont -> Cont

  Binary version of coproduct

Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3

Any : List Cont -> Cont

  N-ary version of coproduct

Visibility: public export

Any : Vect n Cont -> Cont

  N-ary version of coproduct

Visibility: public export

(>@) : Cont -> Cont -> Cont

  Composition of containers making Ext (c >@ d) = (Ext c) . (Ext d)
  Non-symmetric in general, and not in diagrammatic order
  Monoid with Scalar

Visibility: public export
Fixity Declaration: infixr operator, level 3

(@>) : Cont -> Cont -> Cont

  Diagrammatic composition of containers, i.e. swapped order of composition

Visibility: public export
Fixity Declaration: infixr operator, level 3

(>@) : c1 =%> d1 -> c2 =%> d2 -> (c1 >@ c2) =%> (d1 >@ d2)

  Action on morphisms

Visibility: public export
Fixity Declaration: infixr operator, level 3

(@>) : c1 =%> c2 -> d1 =%> d2 -> (c1 @> d1) =%> (c2 @> d2)

  Action on morphisms for diagrammatic composition

Visibility: public export
Fixity Declaration: infixr operator, level 3

InternalLens : Cont -> Cont -> Cont

  Every lens gives rise to a container
  The set of shapes is the lens itself
  The set of positions is the inputs to the lens

Visibility: public export

curry : (c >< d) =%> e -> c =%> InternalLens d e

Visibility: public export

uncurry : c =%> InternalLens d e -> (c >< d) =%> e

Visibility: public export

(<!>) : (Type -> Type) -> Cont -> Cont

  If `f` is a monad, then `f <!> -` is a comonad, and vice versa

Visibility: public export
Fixity Declarations:
infixr operator, level 9
infixr operator, level 9

(<!>) : (f : (Type -> Type)) -> Functor f => c =%> d -> (f <!> c) =%> (f <!> d)

Visibility: public export
Fixity Declarations:
infixr operator, level 9
infixr operator, level 9

CartesianClosure : Cont -> Cont -> Cont

  From https://www.cs.ox.ac.uk/people/samuel.staton/papers/cie10.pdf

Visibility: public export

curry : (c >*< d) =%> e -> c =%> CartesianClosure d e

Visibility: public export

uncurry : c =%> CartesianClosure d e -> (c >*< d) =%> e

Visibility: public export

apply : (CartesianClosure x y >*< x) =%> y

Visibility: public export

List : Cont -> Cont

Visibility: public export

bww : (f : c =%> d) -> (cs : List (c .Shp)) -> All (d .Pos) (f .fwd <$> cs) -> All (c .Pos) cs

Visibility: public export

List : c =%> d -> List c =%> List d

Visibility: public export

(!!) : Cont -> Cont

  BANG. List on positions, always has a monoid structure

Visibility: public export
Fixity Declaration: prefix operator, level 9

PreparedChoice : Vect n Cont -> Cont

  TODO Might be able to delete this and leave just the definition in Additive?

Visibility: public export

Simplex : Nat -> Cont

Visibility: public export

ConvexComb : Vect n Cont -> Cont

  Probabilistic product of containers
  Convex combination of shapes, and a product of positions
  This is equivalent to the n-ary Hancock tensor product of containers, 
  together with a choice of a point inside an n-simplex

Visibility: public export

Deriv : (c : Cont) -> InterfaceOnPositions c DecEq => Cont

  Derivative of a container
  Given c=(Shp !> pos) the derivative can be thought of as
  a shape s : Shp, a distinguished position p : pos s, and the set of *all other positions*

Visibility: public export