natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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
Generally here also the type $Z$ itself may depend on the variable $x$ (hence the term $z$ may be of different type dependending on its free variables) in which case one says that $z$ is a term of $X$-dependent type.
In the metalanguage of type theory called natural deduction, terms are what the term introduction rules produce.
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
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
dependent term?
Last revised on September 26, 2012 at 17:06:01. See the history of this page for a list of all contributions to it.