\import Algebra.Group.Aut
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Category
\import Category.Functor
\import 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} : QEquiv {MonoidCatAction M} {Functor (DeloopM M) C} \cowith
  | f c => c.functor
  | ret => functor->action
  | ret_f c => ext (idp, idp)
  | f_sec f => idp