|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-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|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, (idemponent) 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|
|synthetic mathematics||domain specific embedded programming language|
Per Martin-Löf’s meaning explanations of type theory provide a way to justify the correctness of the rules of type theory. The meaning of the judgements of type theory are defined by computation of closed terms to canonical form in some untyped notion of computation, such as a lambda calculus extended with constants for the constructors and eliminators of type theory.
From a technical/mathematical point of view, the meaning explanations give rise to a realizability model of type theory, where realizers are terms in some untyped notion of computation, such as an extended lambda calculus. That is, it can be regarded as a description of how types are assigned to untyped computations. However, the term “meaning explanations” also refer to the “philosophical” or “pre-mathematical” component, which regards this as an “explanation” of the “constructive validity” of the judgements of the type theory.
The standard meaning explanations validate not just the rules of intensional type theory but also the stronger rules of extensional type theory. Thus, if one regards it as the “intended semantics” then one may believe in the extensional theory. However, like any particular semantics for a formal theory, the meaning explanation also validates many other “rules” as well which are not usually added to type theories, so it is not so clear that meaning explanations in their own right argue for extensionality. They can also be modified so as to no longer satisfy extensionality.
Martin-Löf has been quoted as saying
Some people feel that when I have presented my meaning explanations I have said nothing. And this is how it should be. The standard semantics should be just that: standard. It should come as no surprise.
Suppose we have given some collection of computational objects which we call “terms”, with an untyped notion of “reduction” or “computation”. These could be terms in a lambda calculus, or elements of a partial combinatory algebra, or even programs in a real-world programming language such as C, Java, or Python. We write to mean that computes or reduces to (in some number of steps). We then define simultaneously the following predicates, where are terms:
The definition is by induction-recursion. We define the property “ is a type” inductively, and simultaneously we define recursively two functions assigning to each type the collection of terms of type and the collection of pairs of equal terms of type , respectively. Moreover, each such collection may itself be defined inductively.
The clauses which we include in each case depend on what types we want to put into our type theory; in each case the base notion of untyped computation must include a corresponding structure. Here are three paradigmatic examples.
Suppose that we have terms , , and , along with a recursor such that
The term is intended to denote the value at of a recursively defined function specified to be at zero and at successors. Here and are variables which may occur free in but are bound in , representing the current index and the result of the last recursive call, respectively.
The corresponding clause for elements is
And for equality:
Suppose that we have a term constructor yielding “” for terms and , and similarly and , such that
Then to explain the function type, we include a clause in the inductive definition of “ is a type” which says
The clause for elements is:
This is not an inductive definition as we had for the natural numbers; it is merely a simple definition. On the other hand, we are now using the fact that the function mapping types to their collections of elements is recursively defined, since in order to make this definition, we must invoke it at and .
For equality, of course we have:
Suppose we have a term constructor yielding for terms , and similarly some term . Then to explain the identity type, we add to the inductive definition of “ is a type” the clause
Here we are finally using the fact that typehood and elements are defined by induction-recursion: this clause in the inductive definition of typehood must refer to the value of the recursive elementhood function at some smaller type.
The clause for elements is:
Here we use not only the fact that elementhood is recursively defined, but that it is defined by mutual recursion with equality. The clause for equality is:
Because we have deliberately only put (and terms reducing to it) into the identity type, this definition of identity types will validate the “equality reflection” rule of extensional type theory.
There are simple ways to modify the meaning explanation so as to no longer validate the extensional rules. For instance, if we add to the semantics additional “free variables”, so that there are “neutral terms” which do not compute to any canonical form, and modify the rules of the interpretation so as to say that any normalizable neutral term inhabits every type, then extensionality will no longer hold, since the identity type (like any type) will contain all the variables. This is maybe not a particular compelling model of intensionality, but there are proposals for better ways to expand the meaning explanation to deal with intensional type theory.
The claim is that by inspecting these definitions, one can arrive at the formal rules of type theory for manipulating judgments such as “ is a type”, “”, and “”, which no longer refer to any given notion of computation. However, Martin-Löf famously wrote
…there are … certain limits to what verbal explanations can do when it comes to justifying axioms and rules of inference. In the end, everybody must understand for himself.
Moreover, as mentioned above, the meaning explanation (like any particular semantics) validates many other “rules” which are not usually added to type theories, such as
(However in Nuprl rules such as these are, in fact, included.) Thus, some discrimination is required, as well as some choices (e.g. whether to add the extensionality rule for identity types).
Jon Sterling, Type theory and its Meaning Explanations , 2015 (video recording)
Proposal for homotopy type theory: