\import Algebra.Module
\import Algebra.Module.ModuleCategory
\import Algebra.Module.LinearMap
\import Algebra.Ring
\import Category.Functor
\import Paths.Meta
\import Set.SetCategory

\instance PowerLModule {R : Ring} (J : \Set) (M : LModule R) : LModule R (J -> M)
  | zro _ => M.zro
  | + f g j => f j M.+ g j
  | zro-left => ext (\lam j => M.zro-left)
  | zro-right => ext (\lam j => M.zro-right)
  | +-assoc => ext (\lam j => M.+-assoc)
  | negative f j => M.negative (f j)
  | negative-left => ext (\lam j => M.negative-left)
  | +-comm => ext (\lam j => M.+-comm)
  | *c r f j => r *c f j
  | *c-assoc => ext (\lam j => *c-assoc)
  | *c-ldistr => ext (\lam j => *c-ldistr)
  | *c-rdistr => ext (\lam j => *c-rdistr)
  | ide_*c => ext (\lam j => ide_*c)

\func FunctorPowerLMod {R : Ring} : Functor SetCat.op (LModuleCat R) \cowith
  | F I => PowerLModule I (RingLModule R)
  | Func f => \new LinearMap {
    | func r j => r (f j)
    | func-+ => idp
    | func-*c => idp
  }
  | Func-id => idp
  | Func-o => idp