\import Algebra.Group.Aut
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Category
\import Category.Functor
\import Equiv (Equiv)
\import Paths.Meta

-- TODO: when limits in presheaves are added, write that category of actions is bicomplete whenever the underlying category is bicomplete

\class MonoidCatAction {C : Precat} (M : Monoid) (\classifying  c : C){
  | act : MonoidHom M (End c)

  \func functor : Functor (DeloopM M) C \cowith
    | F => \lam _ => c
    | Func (f : M) => act f
    | Func-id => act.func-ide
    | Func-o => act.func-*
}

\instance DeloopM (M : Monoid) : Precat
  | Ob => \Sigma
  | Hom _ _ => M
  | id _ => M.ide
  | o => *
  | id-left => ide-left
  | id-right => ide-right
  | o-assoc => *-assoc

\func functor->action {C : Precat} {M : Monoid} (f : Functor (DeloopM M) C) : MonoidCatAction M \cowith
  | c => f ()
  | act => \new MonoidHom {
    | func => Func
    | func-ide => Func-id
    | func-* => Func-o
  }

\func Action<->Functor {C : Precat} {M : Monoid} : Equiv {MonoidCatAction M} {Functor (DeloopM M) C} \cowith
  | f (c : MonoidCatAction) => c.functor
  | ret => functor->action
  | ret_f c => ext (idp, idp)
  | sec => functor->action
  | f_sec f => idp