Predicate

Definition (Type Theory)

In type theory, this is anything of the form,

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

For type $X_i$.

Definition (Classical)

In classical logic, it is represented semantically as,

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