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).

**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**

logic | category theory | type theory |
---|---|---|

true | terminal object/(-2)-truncated object | h-level 0-type/unit type |

proposition(-1)-truncated objecth-proposition, mere proposition

proofgeneralized elementprogram

cut rulecomposition of classifying morphisms / pullback of display mapssubstitution

cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction

introduction rule for implicationunit for hom-tensor adjunctioneta conversion

logical conjunctionproductproduct type

disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)

implicationinternal homfunction type

negationinternal hom into initial objectfunction type into empty type

universal quantificationdependent productdependent product type

existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalencepath space objectidentity type

equivalence classquotientquotient type

inductioncolimitinductive type, W-type, M-type

higher inductionhigher colimithigher inductive type

completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set

setinternal 0-groupoidBishop set/setoid

universeobject classifiertype of types

modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation

proof netstring diagramquantum circuit

(absence of) contraction rule(absence of) diagonalno-cloning theorem

synthetic mathematicsdomain specific embedded programming language

</table>

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.)

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

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.

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

Last revised on April 27, 2017 at 09:01:46. See the history of this page for a list of all contributions to it.