Usually it's not possible to form such a predicate. If we have impredicative base universe, then it's possible to form a predicate over all types in the base universe (which may or may not be all types in the language), including the predicate itself. However, this feature is rarely used in type theory, because it is incompatible with classical logic.

In programming, this is more commonly available, because we don't necessarily care about propositions, let alone classical logical proofs. The polymorphic identity function type `forall a. a -> a` in System F quantifies over all types including itself.