
  0 | module Data.Container.Additive.Extension.Definition
  1 | 
  2 | import Data.Container.Base
  3 | import Data.Container.Additive.Object.Definition
  4 | 
  5 | ||| If extension of a container is a functor Type -> Type, what is an extension
  6 | ||| of an additive container?
  7 | public export
  8 | Ext : AddCont -> Type -> Type
  9 | Ext c x = Ext (UC c) x