Given a container `c`, i.e. a`c.Shp`-indexed family of sets, it is
straightforward to compute the coproduct of this family/its Sigma type:
It is simply the type of dependent pairs `(s : c.Shp ** c.Pos s)`.
But given an additive container, i.e. a `c.Shp`-indexed family of
*commutative monoids*, its coproduct / Sigma type is a bit tricky:
Despite the fact that we have a monoid structure on every `c.Pos s`, we
cannot naively use the type of dependent pairs `(s : c.Shp ** c.Pos s)` as
the base set. This is because it doesn't form a monoid: we cannot add
`(s1 ** p1)` and `(s2 ** p2)` when `s1 ≠ s2` as `p1` and `p2` have
different types.
Instead, we add them *formally*. We can use the free monoid construction on
this dependent pair, and quotient it out by certain relations. Specifically,
we use the base set `List (x : c.Shp ** c.Pos x)` quotiented out by:
1) Permutation (the list order should not matter)
2) `(s, 0) : xs = xs` (pairs where output is zero can be dropped)
3) `(s, p1) : (s, p2) : xs` = (s, p1 + p2) : xs` (same-shape entires add)
We don't enforce these properties here, but instead need to check that all
maps consuming this type preserve them.
Abstractly, we can state the following:
* the Pi type of additive containers is inherited from ordinary containers
* When `c.Shp` is finite, Pi and Sigma type of additive containers coincide
(i.e. in the finitary case, product and coproduct coincide)
* When `c.Shp` is not finite, Sigma type is the subtype of Pi type, with finite support
Totality: total
Visibility: public export