
  0 | module Data.Container.Additive.Extension.Definition
  1 | 
  2 | import Data.Container.Base
  3 | import Data.Container.Additive.Object.Definition
  4 | import Data.ComMonoid
  5 | 
  6 | ||| A functor `AddCont -> [ComMon, Type]`
  7 | public export
  8 | record Ext (0 c : AddCont) (y : ComMonoid) where
  9 |   constructor (<|)
 10 |   shapeExt : c.Shp
 11 |   index : ComMonoidHomo (UMon c shapeExt) y
 12 |