Predicate

In type theory, this is anything of the form,

$$P:X_0\to \cdots \to X_{n-1}\to \mathrm{Prop}$$

For any type $X$.

In classical logic, it is represented semantically as,

$$P\subseteq X_0\text{texttimes}\cdots \text{texttimes}{X}_{n-1}$$

But the two notions are equivalent in Truncation (HoTT) systems.