
  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 | ||| Convenience datatype storing the property that
  8 | ||| an additive container `c` has an interface `i` on its positions
  9 | public export
 10 | data InterfaceOnPositions : (c : AddCont) -> (i : Type -> Type) -> Type where
 11 |   ||| For every shape s the set of positions c.Pos s has that interface
 12 |   MkI : ((s : c.Shp) -> i (c.Pos s)) -> InterfaceOnPositions c i
 13 | 
 14 | 
 15 | 
 16 | namespace Flat
 17 |   public export
 18 |   data IsFlat : AddCont -> Type where
 19 |     MkIsFlat : (p : Type) -> (mon : ComMonoid p) => IsFlat (MkAddCont (Const p))
 20 | 
 21 |   --flatEq : IsFlat c => c = MkAddCont (Const c.Shp)