
  0 | module Data.Container.Additive.Properties.Definitions
  1 | 
  2 | import Data.Container.Base
  3 | import Data.Container.Additive.Object.Definition
  4 | 
  5 | import Data.ComMonoid
  6 | 
  7 | 
  8 | ||| Convenience datatype storing the property that
  9 | ||| an additive container `c` has an interface `i` on its positions
 10 | public export
 11 | data InterfaceOnPositions : (c : AddCont) -> (i : Type -> Type) -> Type where
 12 |   ||| For every shape s the set of positions c.Pos s has that interface
 13 |   MkI : (p : (s : c.Shp) -> i (c.Pos s)) =>
 14 |     InterfaceOnPositions c i
 15 | 
 16 | 
 17 | namespace Flat
 18 |   public export
 19 |   data IsFlat : AddCont -> Type where
 20 |     MkIsFlat : (p : Type) -> (mon : ComMonoid p) => IsFlat (MkAddCont (Const p))
 21 | 
 22 |   --flatEq : IsFlat c => c = MkAddCont (Const c.Shp)