∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (F : CategoryTheory.Functor C FintypeCat) {G : Type u_4}
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).carrier] (g : G) (X : C) (x : (F.obj X).carrier),
  g • g⁻¹ • x = x