Contradiction

Predicate from which any predicate (in the same context) can be derrived.

For example,

• $\vec{C}⊢a:\perp$ in type theory, and
• $\vec{x}:\vec{X}⊢P\vec{x}\vee \neg P\vec{x}$, for some predicate $P:\vec{X}\to \mathrm{Prop}$, are both examples of a contradiction.