Data.Container.Additive.Object.Definition

Definitions

record AddCont : Type

  Additive container: a container whose every set of positions is a
  commutative monoid.
  Not to be confused with `TensorMonoid` where the set of shapes is a monoid,
  and every set of positions is a comonoid
  We need additivity only because we want to copy/delete information: on the 
  backwards pass this sums up or creates a zero value
  TODO this in some sense dual to `TensorMonoid`, since by default we have a
  unique comonoid structure on shapes? I.e. every set is uniquely a comonoid

Totality: total
Visibility: public export
Constructor: 

MkAddCont : (UC : Cont) -> InterfaceOnPositions UC ComMonoid => AddCont

Projections:

.UC : AddCont -> Cont

.mon : ({rec:0} : AddCont) -> InterfaceOnPositions (UC {rec:0}) ComMonoid

.UC : AddCont -> Cont

Visibility: public export

UC : AddCont -> Cont

Visibility: public export

.mon : ({rec:0} : AddCont) -> InterfaceOnPositions (UC {rec:0}) ComMonoid

Visibility: public export

mon : ({rec:0} : AddCont) -> InterfaceOnPositions (UC {rec:0}) ComMonoid

Visibility: public export

.Shp : AddCont -> Type

Visibility: public export

.Pos : (c : AddCont) -> c .Shp -> Type

Visibility: public export

UMon : (c : AddCont) -> (s : c .Shp) -> ComMonoid (c .Pos s)

  Underlying monoid structure of positions

Visibility: public export

.Plus : (c : AddCont) -> (s : c .Shp) -> c .Pos s -> c .Pos s -> c .Pos s

Visibility: public export

.Zero : (c : AddCont) -> (s : c .Shp) -> c .Pos s

Visibility: public export

data InterfaceOnPositions : AddCont -> (Type -> Type) -> Type

  Convenience datatype storing the property that
  an additive container `c` has an interface `i` on its positions

Totality: total
Visibility: public export
Constructor: 

MkI : ((s : c .Shp) -> i (c .Pos s)) => InterfaceOnPositions c i

  For every shape s the set of positions c.Pos s has that interface

data IsFlat : AddCont -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsFlat : (p : Type) -> {auto mon : ComMonoid p} -> IsFlat (MkAddCont (Const p))