Inductive CategoryT :=
  Category : forall (s : string),
    matches s (regex "[A-Z][A-Za-z0-9_-]{0,128}")
      -> CategoryT.
