I didn’t notice before, but I want to point out that this is the wrong unicode symbol. The n-ary times operator \u{2a09} indicates a repeated operation, similar to ∑ for sums and ∏ for products.
The correct symbol here is the multiplication sign \u{d7}, which looks like “×” in text and “×” in code, thus[5 × Int] for the example.