{V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        CategoryTheory.Functor.id (Action V G) ≅
          Action.FunctorCategoryEquivalence.functor.comp Action.FunctorCategoryEquivalence.inverse