∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] [inst_2 : SizeOf V]
  [inst_3 : SizeOf G] (V_1 : V) (ρ : G →* CategoryTheory.End V_1),
  sizeOf { V := V_1, ρ := ρ } = 1 + sizeOf V_1 + sizeOf ρ