nLab type

This entry is about the notion in type theory. For the unrelated notion of the same name in model theory see at type (in model theory).

---

Idea

In modern logic, we understand that every variable should have a type, or domain of discourse or be of some sort. For instance we say that if a variable $n$ is constrained to be an integer then “$n$ is of integer type” or “of type $\mathbb{Z}$”. The usual formal expression from set theory for this – $n \in \mathbb{Z}$ – is then often written $n \colon \mathbb{Z}$

We speak of typed logic if this typing of variables is enforced by the metalanguage. In formulations of a theory the types are often called sorts. More generally, type theory formalizes reasoning with such typed variables. See there for more

(Untyped logic may be seen as simply a special case, in which there is only a single unique type. Thus, untyped logic has one type, not no type.)

Definition

Reasoning with types is formalized in natural deduction (which in turn is formalized in a logical framework such as Elf).

Behaviour of types is specified by a 4-step set of rules

1. type formation

2. term introduction

3. term elimination

4. computation rules

Properties

Deep relations between type theory, category theory and computer science relate types to other notions, such as objects in a category. See at computational trinitarianism for more on this.

Related concepts

• category (philosophy)

• fibrant type

type, type theory

• propositions as types, propositions as some types

• inductive type, W-type

• empty type, unit type

• pointed type

dependent type, dependent type theory, Martin-Löf dependent type theory

• dependent sum type, dependent product type

homotopy type, homotopy type theory

• identity type, heterogeneous identity type

• homotopy n-type, connected type

• higher inductive type

• geometric homotopy type, cohesive homotopy type