|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
In other words a pure type system is
a system of natural deduction;
for dependent types;
A pure type system is defined by
In fact all such triples appearing in the following have . So we can just as well regard them as binary relations (rather than ternary ones).
From the above input data we derive the following
The terms of a pure type system are the following (recursive definition):
Here is a variable and , are terms. The operators and bind the variable .
The typing of terms is inductively defined by the following rules.
A typing is of the form
meaning that the types of the variables declared on the left induces the term has type . Note that types are also terms.
The order of variable declarations is significant: the declaration may depend on declarations to its left.
The natural deduction rules are defined to be the following, for all and where ranges over the set of variables.
|(axioms)||if is an axiom;|
The lambda cube consists of eight systems arranged in a cube. The most expressive is given by the following choice of sorts, axioms and relations:
(Here denotes the 2-element set.)
The other systems omit some of the last three relations. Some specific systems are the following:
|simply typed lambda calculus||yes|
|calculus of constructions||yes||yes||yes||yes|
For instance for the calculus of constructions we have
The relations express the usual rule for dependent product type:
a dependent product over a generic dependent type is itself some type;
The most permissive pure type system:
But there is an example with even non-circular system of axioms:
A quick survey is in