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