Data.Container.Additive.Object.Instances

Definitions

Const2 : Type -> ComMonoid -> AddCont

  Constant (non-dependent) add. container, positions not dependent on shapes
  As a polynomial functor: F(Y) = aY^b

Totality: total
Visibility: public export

Const : (a : Type) -> ComMonoid a => AddCont

  Constant additive container whose shapes and positions coincide
  Also arises from Num instance

Totality: total
Visibility: public export

Nap : ComMonoid -> AddCont

  Naperian additive container: a constant container with a single shape
  As a polynomial functor: F(Y) = Y^b

Totality: total
Visibility: public export

Flat : Type -> AddCont

  Flat additive container: a constant container with a single position
  As a polynomial functor: F(Y) = aY
  Notably, unlike with `Data.Container.Base`, there is no `Sharp`

Totality: total
Visibility: public export

Empty : AddCont

  Empty additive container
  As a polynomial functor: F(Y) = 0
  Initial additive container

Totality: total
Visibility: public export

Scalar : AddCont

  Container of a single thing
  As a polynomial functor: F(Y) = U(Y) where U is forgetful functor
  Unit of the tensor product

Totality: total
Visibility: public export

UnitCont : AddCont

  Additive container with a single shape and position
  As a polynomial functor F(Y) = 1
  Terminal additive container

Totality: total
Visibility: public export