Type theory

is used by Twelf, often to define other type theories;

LF

many type theories which fall under are used by the HOL family of provers and PVS;

higher-order logic

computational type theory is used by ;

NuPRL

and its derivatives are used by Coq, Matita, and Lean;

calculus of constructions

UTT (Luo's Unified Theory of dependent Types) is used by which is both a programming language and proof assistant

Agda

"${\displaystyle T}$ "

is a type

"${\displaystyle t}$ of type ${\displaystyle T}$"

is a term

"Type ${\displaystyle T_{1}}$ type ${\displaystyle T_{2}}$"

is equal to

"Terms ${\displaystyle t_{1}}$ and ${\displaystyle t_{2}}$ both of type ${\displaystyle T}$ "

are equal

correspond to the typed λ-calculus (Lambek, 1970);

cartesian closed categories

(categories with products and exponentials and one non-terminal object) correspond to the untyped λ-calculus (observed independently by Lambek and Dana Scott around 1980);

C-monoids

correspond to Martin-Löf type theories (Seely, 1984).

locally cartesian closed categories

${\displaystyle 42:{\mathsf {nat}}}$

${\displaystyle \mathrm {true} :{\mathsf {bool}}}$

${\displaystyle x:{\mathsf {nat}}}$

${\displaystyle y:{\mathsf {bool}}}$

Set theory has both and axioms, while type theories only have rules. Type theories, in general, do not have axioms and are defined by their rules of inference.^[14]

rules

Classical set theory and logic have the . When a type theory encodes the concepts of "and" and "or" as types, it leads to intuitionistic logic, and does not necessarily have the law of excluded middle.^[17]

law of excluded middle

In set theory, an element is not restricted to one set. The element can appear in subsets and unions with other sets. In type theory, terms (generally) belong to only one type. Where a subset would be used, type theory can use a or use a dependently-typed product type, where each element ${\displaystyle x}$ is paired with a proof that the subset's property holds for ${\displaystyle x}$. Where a union would be used, type theory uses the sum type, which contains new canonical terms.

predicate function

Type theory has a built-in notion of computation. Thus, "1+1" and "2" are different terms in type theory, but they compute to the same value. Moreover, functions are defined computationally as lambda terms. In set theory, "1+1=2" means that "1+1" is just another way to refer the value "2". Type theory's computation does require a complicated concept of equality.

Set theory . Type theory can encode numbers as functions using Church encoding, or more naturally as inductive types, and the construction closely resembles Peano's axioms.

encodes numbers as sets

In type theory, proofs are types whereas in set theory, proofs are part of the underlying first-order logic.

[14]

which is a higher-order logic

Simply typed lambda calculus

intuitionistic type theory

system F

is often used to define other type theories

LF

and its derivatives

calculus of constructions

Foundations of mathematics

Logic

which has articles on many topics.

Type Theory at nLab

article at the Stanford Encyclopedia of Philosophy

Intuitionistic Type Theory

book by Henk Barendregt

Lambda Calculi with Types

textbook style paper by Helmut Brandl

Calculus of Constructions / Typed Lambda Calculus

notes by Per Martin-Löf

Intuitionistic Type Theory

book

Programming in Martin-Löf's Type Theory

book, which proposed homotopy type theory as a mathematical foundation.

Homotopy Type Theory