[wdanilo]

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.

[tentaTherapist]

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?

[shalabhc]

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?

[wdanilo]

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.