While set theory is axiomatised in the formal system of first order logic, a type theory is its own formal system. We present a type theory called Martin Löf Type Theory (MLTT for short). By Curry-Howard, MLTT corresponds to first-order logic. The material is essentially from Chapter 1 of [1].
In MLTT, there are four kinds of judgments, each is expressed as follows:
is a (well-formed) type in context ,
and are judgmentally equal as types in context ,
is an element of type in context ,
and are judgmentally equal as elements of type in context ,
In general, all judgments are in the form
where is a context (defined later) and is a judgment thesis that asserts either (1) is a type, (2) and are equal types, (3) is an element of type , or (4) and are equal elements of type . Note that all the metavariables may depend on variables in .
A context is a finite sequence in the form
such that for each , we can derive the judgment
To phrase it differently, we say that the empty context is a context. If has type (in the empty context) and has type in the context , then is a context. Longer contexts are defined similarly.
is a type family over in context if the judgment
is admissible. Similar to indexed family of sets, we also say that the type is indexed by in context .
The element version of a type family is called a section.
is a section of type family over in context if the judgment
is admissible. The element is said to be indexed by in context .
In the above definitions, may all depend on despite we have not explicitly mentioned them.
We first present the system of structural rules of MLTT. These rules establish the basic mathematical framework for type dependency. See for a more detailed introduction to substructural rules.
In MLTT, there are six sets of structural rules:
Judgmental presumptions
Equivalence on judgmental equality
Variable conversion
Substitution
Weakening
Generic elements
todohere 2.2.1 Presumptions
Consider the judgment . For to be a type from the context , we need to presume that is a (well-formed) context, and is indeed a type. In MLTT, we have these presuppositions
2.2.2 Equivalence on Judgmental Equality
these inference rules postulate that judgmental equality on types and on elements is an equivalence relation. That is, they are reflexive, symmetric, and transitive
The variable conversion rule
postulates that we can swap judgmentally equal types in a context, where the generic judgment thesis refers to an arbitrary judgment (one of the four defined in Definition A).
It is convenient to be able to covert the type of an element to a judgmentally equal type. This rule is called the element conversion rule
which is derivable from the existing rules. See todolater
We add two more congruence rules for substitution. They postulate that substituting judgmentally equal elemets results in judgmentally equal types and elements
When is a type family over and , we say that is the fiber of at . We use to denote .
Similary, when is a section of the family over , we call the element the value of at . Again, we use to denote it.
Given a type in context , any judgment in a longer context can also be made in a weaker context for a fresh variable . This is the weaking rule
With the weakening rule, we can derive where does not depend on .
The type in context is called the constant family .
prove
also known as the variable rule
to keep proof trees short and manageable, we use the convention that any derived rules can be used in future derivations
variables can always be changed to fresh variables
we prove
is deriable, where is a variable not in the context .
notice that in we impose that is not in .
If we have types and in context , and we can make some judgments in , then we can make the same judgment in .
todohere