It's not a bogus! We are FP enthusiasts and the word "category" has really strong connections to our type system. However, the name might be a little misleading so we've already changed it. Anyway, we treat our types as categories. For example 1 belongs to a singleton category 1 (thus you can write 1 :: 1) but it also belongs to category of positive numbers or all numbers in general, thus again you can write (1 :: 1 :: Nat :: Int :: Num :: *). I hope you see now connections to category theory. However the name itself, as I noted above, could be misleading so we need to change it.

That's just plain-old dependent typing, isn't it? What's in this and not in, say, Idris, such that you can say that it's a whole new paradigm?

1 also belongs to 'all integers from 1 through 10'. Is this also a category? (I assume yes). How is this category expressed in Luna?

Yes it is, `1 :: 1 | .. | 10`. The pipe combines categories, so you can as well write `1 :: 1|2|3|4|5|6|7|8|9|10`. Both of the forms are however not yet supported in the main branch of official compiler and will not be supported during the first release yet.

I wouldn’t say it’s bogus, and there definitely wasn’t any malicious intention behind it, it’s just that finding a name for such a property is super difficult. As I’ve written above, it’s about having fine-grained control over the data (object) constructors. It turns out most words synonymous to “type”, “kind”, “category” etc. (as understood in the wide sense) are already taken by mathematical / programming concepts. We will, however, change the name, as it causes way too much confusion :).

And you know that because?