Well, there's an easy way: For any property Q you can create a type of all objects satisfying Q. If we want we can happily capture that too in Fitch-style, after adding an inbuilt type of all types called "type":
Q : bool ⊢ { x : Q(x) } : type
Oh actually we don't need to add "type" and the first rule if we have the last two rules. (I added it because I also like to be able to reason about types, but that's unrelated to our conversation now.)
