# Contents

## 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 dependending 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 \,.$
• dependent term?

Revised on September 26, 2012 17:06:01 by Urs Schreiber (131.174.191.22)