(motive : Lean.Name → Sort u_1) →
  (catName : Lean.Name) →
    (Unit → motive `term) →
      (Unit → motive `command) →
        (Unit → motive `tactic) → (Unit → motive `conv) → ((x : Lean.Name) → motive x) → motive catName