builtins.toJSON (builtins.substring 0 1 "𝒫")