
  0 | module Data.Container.Additive.Extension.Definition
  1 | 
  2 | import Data.Container.Base
  3 | import Data.Container.Additive.Object.Definition
  4 | import Data.Container.Additive.Morphism.Definition
  5 | import Data.ComMonoid
  6 | 
  7 | ||| A functor `AddCont -> [ComMon, Type]`
  8 | public export
  9 | record Ext (0 c : AddCont) (y : ComMonoid) where
 10 |   constructor (<|)
 11 |   shapeExt : c.Shp
 12 |   index : ComMonoidHomo (UMon c shapeExt) y
 13 | 
 14 | 
 15 | ||| Analogous to one in `Base.Extension.Definition`
 16 | public export
 17 | extMap : {0 y : ComMonoid} -> {0 c, d : AddCont} ->
 18 |   c =%+> d -> Ext c y -> Ext d y
 19 | extMap f (sh <| index) = let (y ** ky) = (%!+) f sh
 20 |                          in y <| (index . ky)