nLab term

Idea

In formal logic such as type theory a term $z$ is an entity/expression of the formal language which is of some type $Z$. One writes $z : Z$ to express this (a typing judgement). The semantics of terms in Set is: elements of a set, where one writes $z \in Z$. One also says $z$ is an inhabitant of the type $Z$ and that $Z$ is an inhabited type if it has a term.

A term $z : Z$ may depend on free variables $x$ that are themselves terms $x : X$ of some other type $X$. For instance $z \coloneqq x + 3$ may be a term of type $Z \coloneqq \mathbb{Z}$ (the integers) which depends on a variable term $x$ also of type $X \coloneqq \mathbb{Z}$ the integers. The notation for this in the metalanguage is

$$x : X \vdash z : Z \,.$$

Generally here also the type $Z$ itself may depend on the variable $x$ (hence the term $z$ may be of different type depending on its free variables) in which case one says that $z$ is a term of $X$-dependent type.

Definition

In the metalanguage of type theory called natural deduction, terms are what the term introduction rules produce.

Categorical semantics

Here are comments on the interpretation of types in the categorical semantics of dependent type theory.

In the internal language of any category $C$, a morphism

$$f : B \to A$$

is a term $f(x)$ of type $A$ where $x$ is a free variable of type $B$, which in type-theoretic symbols is given by

$$x\colon B \vdash f(x)\colon A \,.$$

Related concepts

• element, generalized element

• dependent term?

• term introduction rule, term elimination rule

• telescope