
  0 | module Data.Container.Additive.Extension.Definition
  1 | 
  2 | import Data.Container.Base
  3 | import Data.Container.Additive.Object.Definition
  4 | 
  5 | public export
  6 | Ext : AddCont -> Type -> Type
  7 | Ext c x = Ext (UC c) x
  8 | 
  9 | ||| Can be represented as a derivative
 10 | public export
 11 | Path : AddCont -> Type
 12 | Path c = (x : c.Shp ** c.Pos x)