∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {H : Type u_3} [inst_2 : Group H] (X : Action V H) [inst_3 : CategoryTheory.RightRigidCategory V] (h : H),
  Xᘁ.ρ h = X.ρ h⁻¹ᘁ