External feature (type theory)

In type theory, a concept is colloquially referred to as external if it exists in the metatheory and not as a construction within the type theory.

For example, one might contrast $a\in A$ and $a:A$ by saying that $a\in A$ is a proposition (an internal statement), while $a:A$ is a judgement (an external statement). Within a type theory, one can reason about $a\in A$: "if $a\in A$, then $b\in B$ and not $c\in C$;" the same cannot be done with $a:A$, since it is a judgement. As far as the type theory itself is concerned, it is completely meaningless to speak of $a$ the relation to $A$ — $a:A$ is a simple fact of the type theory.[cite:@1lab]