1 Abstract
We introduce to Martin Löf Type Theory. The material follows from [1].
Type theory is a foundational language for mathematics (i.e. an alternative to set theory). However, it behaves differently from set theory. A set-theoretic foundation has two layers: (1) a deduction system (e.g. first order logic), and (2) some axioms formulated inside this system (e.g. axioms of ZFC). Therefore, set theory is not only about sets, but rather about the interplay between sets (objects of the second layer) and propositions (objects of the first layer).
In constrast, type theory has its own deductive system. Instead of working with propositions and sets in set theory, type theory uses the notion of types and terms. Propositions are identified with particular types; and thus proving a theorem corresponds to the mathematical activity of constructing an term (called an inhabitant) of a type that represents the proposition.
A deductive system consists of a collection of judgments with rules to derive them. This is analogous to positions with rules in game theory, and elements with operations in an algebraic theory.
In type theory, the most basic judgment is " ", read as "the term has type ". When is a type representing a proposition, the term may be regarded as an evidence to the truth of (or even a proof of ).
We sometimes can treat the type as a set; the judgment " " can then be interpreted as analogous to the set-theoretic statement " ". However, an essential difference is that " " is a judgment (in type theory) whereas " " is a proposition (in set theory). In particular, we cannot "disprove" the judgment " " or make statements such as "if then it is not the case that " when working internally in a type theory.
One way to think about it is that the set-theoretic "membership" is a predicate that may or may not hold between two pre-existing sets and , but in type theory, we cannot talk abount an element is isolation. This is because every element is by nature an element of some type. For instance, when we say informally "let be a natural number", the set-theoretic interpretation is "let be a set and assume ", but in type theory "let " is an atomic statement: we cannot introduce a variable without specifying its type.
2.2 Equality, Equality, Equality
The last difference between type theory and set theory is the treatment of equality. In mathematics, the familiar notion of equality is a proposition: e.g. we can disprove an equality or assume it as a hypothesis. In type theory, this correspond to the equality type " " given . When is inhabited, we say that and are propositionally equal.
However, we also need a notion of equality as a judgment, denoted , or simply . For instance, if we define a function by , then is equal to by definition. A judgmental equality (or definitional equality) is then useful when we have derived the judgment for some , and would like to use it to derive an inhabitant for the type , since is by definition. Ultimately, we want a rule saying that given the judgments and , we can derive the judgment .
A third kind of equality are used to define new constants in a type theory. If our type theory has depenedent function types, we can define the type for ordinary functions by . This notation is essentially a shorthand for extending the type theory with the judgments " is a type" and " is judgmentally equal to ".
There are four kinds of judgments in MLTT.
" is a (well-formed) type under context ", expressed as
" and are judgmentally equal types under context ", expressed as
" is an element of type under context ", expressed as
" are are judgmentally equal elements of type under context ", expressed as
All judgments have the form " ", consisting of a context and a judgment thesis . The role of a context is to declare what hypothetical elements are assumed (along with their types).
A context is a finite list of variable declarations
where for each we can derive the judgment
A context is a finite list of variable declarations
where is a type under context ; in other words, we can derive the judgment .
When we write " ", it implies that the variables in may occur free in the type . If so, is a dependent type, and we often write " " to denote this fact. For instance, is a context iff and . For convenience, we write to refer in the empty context.
A feature of type theory is that all judgments are context dependent. This gives rise to the notion of type families and sections, which are types and elements in a dependent setting.
Given a type under context , a type family over under context is a type under context . In other words, is a type family when
Alternatively, we say that is a type indexed by under context .
Given a type family over under context , a section of over under context is an element of type under context . In other words, is a section when
Alternatively, we say that is an element of indexed by under context .
Note that in the above definitions, , , and may also depend on the variables declared under context . It is common practice to not explicitly mention them.
There are the six structual rules of MLTT. These establish its basic mathematical framework.
When saying " is a element of " we are preassuming that is a type. This alludes to the presuppositions about contexts, types, and elements.
4.2 Equivalence Relation of Judgmental Equality
We postulate that judgmental equality is an equivalence relation.
This is where judgmental equality comes in handy.
The variable conversion rules postulate that we can convert/replace the type of a variable in a context to a judgmentally equal type.
Consider a type family under . If there is an element under , we prostulate that, under , we can obtain a type by substituting every free occurrence of in by , denoted .
We generalise this idea by prostulating the substitution rule over an arbirtary judgment thesis :
In addition to the substitution rule itself, we also prostulate that substituting judgmentally equal elements results in judgmentally equal types and elements:
Consider a type family over under context . For , the type is called the fiber of at and is denoted . Similarly, if is a section of , we use to denote , called the value of at .
A context can be weakened to provided that is a fresh variable, and is a type under . One can think of weakening as the inverse of refinement.
The weakening rule postulate that any judgment thesis derivable from a context is also derivable from a weaker context.
Last prostulate about judgments asserts the reflexivity of the turnstile . This rule is also called generic element or variable rule.
The generic element rule postulate that a variable/generic element under the context is indeed an element of type .
Notice that this rule provides the identity function on the type under context .
5 Typing Rules: Dependent Functions
When adding new types to a type theory, we need to specify four principal rules.
The first three rules also come with congruence rules, postulating that all constructors respect judgmental equality. The computation rules are often referred as the β-rule and the η-rule.
In this sectionm, we use dependent function types ( -types) as an example.
The formation rule for -types postulates that is a type for any type family over type
The term is called a λ-abstraction.
This rule is also called the evaluation rule.
The computation consists of two parts. First, the β-rule postulate that
The second rule is the η-rule
which postulate that all elements of a -type are -terms.
Together, the two rules postulate that the introduction and elimination rules are inverese of each other.
Sometimes, we simply write and for simplicity.
We can extend our type theory with internal definitions. An internal definition can be seen as a shorthand (i.e. a new constant) that is judgmentally equivalent to an existing type. In this section, we build the nondepedent function type .
Consider the derivation
Define
This means that we our type theory with a new constant and the rules
In general, we can define new terms as well.
Given a derivation
the notation
means that is a new constant in the type theory, and the rules
are admissible.