0 | module Data.Container.Additive.Object.Instances
 1 |
 2 | import Data.List.Quantifiers
 3 | import Data.Vect.Quantifiers
 4 |
 5 | import Data.Container.Base
 6 | import Data.ComMonoid
 7 | import Data.Container.Additive.Object.Definition
 8 | import Data.Container.Additive.Extension.Definition
 9 | import Data.Container.Additive.Product.Definitions
10 |
11 | ||| Scalar additive container
12 | ||| This is equivalent to `!! UnitCont`
13 | ||| Unit of the categorical product
14 | public export
15 | Scalar : AddCont
16 | Scalar = MkAddCont Scalar
17 |
18 | ||| Empty additive container
19 | ||| Unit of the coproduct
20 | ||| Initial container
21 | public export
22 | Empty : AddCont
23 | Empty = MkAddCont Empty @{MkI absurd}
24 |
25 | ||| Constant additive container, positions not dependent on shapes
26 | ||| Allows the backward part to be different than forward one
27 | public export
28 | Const : Type -> ComMonoid -> AddCont
29 | Const a (t ** m) = MkAddCont (Const2 a t) @{MkI $ \_ => m}
30 |
31 | public export
32 | TrivialPos : Type -> AddCont
33 | TrivialPos a = Const a (Unit ** %search)
34 |
35 | namespace NumConst
36 |   ||| Like above, but where backward part is same as forward one
37 |   ||| Also arises from Num instance
38 |   public export
39 |   Const : (a : Type) -> (mon : ComMonoid a) => AddCont
40 |   Const a = Const a (a ** mon)