, “ has a proof” is a judgment.
Judgment (type theory): is the basic judgment and pronounced as “the term has type ”.
Propositions are types: Finding an element of a type is proving that proposition. Thus we call an element of a type a witness or an evidence of the truth of a proposition.
Propositional equality: When is inhabited, we say that and are propositionally equal.
Judgmental (or definitional) equality: When two expressions are equal by definition. You expand and compute the definitions and conclude that they are equal. We write it as or simply . Use to introduce definitional equality.
Assumption: , where is a variable and is a type.
Context: The collection of all such assumptions.
Type former: A way to construct types, together with rules for the construction and behavior of elements of that type.
For the rest of this chapter we will introduce these type formers:
English | Type Theory |
---|---|
True | |
False | |
and | |
or | |
If then | |
if and only if | |
Not | |
For all , holds | |
There exists such that |
How to introduce a new kind of type:
Formation rules: How to form new types of this kind.
Elimination rules (type’s eliminators): How to use elements of that type.
Computation rule ( -reduction): How an eliminator acts on a constructor.
Uniqueness principle ( -expansion) (optional): Expresses the uniqueness of maps into or out of that type.
Propositional uniqueness principle (optional): When the uniqueness principle is not taken as a rule of judgmental equality, we can prove it as a propositional equality from the other rules for the type.
Formation rules: Given types and , we can construct the type of functions with domain and codomain .
Introduction rules:
Direct definition: Defining by where is a variable and is an expression which may use .
-abstraction:
Elimination rules: Given a function and an element of the domain , we can apply the function to obtain an element of the codomain , denoted and called the value of at .
Computation rule: where is the expression in which all occurrences of have been replaced by .
Uniqueness principle: . It shows that is uniquely determined by its values.
Universe: a type whose elements are types.
Hierarchy of universes: where every universe is an element of the next universe. We assume that they are cumulative: All the elements of the universe are also elements of the universe.
Typical ambiguity: Omitting the level for convenience.
Families of types: Using functions whose codomain is a universe to model a collection of types varying over a given type .
Formation rules: Given a type and a family , we may construct the type of dependent functions .
Introduction rules:
Direct definition: To define , where is the name of a dependent function to be defined, we need an expression possibly involving the variable , and we write
-abstraction:
Elimination rules: Applying to an argument to obtain an element .
Computation rule: Given we have and , where is obtained by replacing all occurrences of in by .
Uniqueness principle: for any .
Polymorphic function: A class of dependent function types which takes a type as one of its arguments and acts on elements of that type.
Formation rules: Given types we introduce the type , which we call their cartesian product.
Introduction rules:
Direct definition: Given and , we may form .
-abstraction:
Elimination rules: For any , we can define a function by
Computation rule:
Propositional uniqueness principle: Every element of is a pair.
Unit type: We call the nullary product type the unit type . The only element of is some particular object .
Except As Otherwise Noted, The Content Of This Page Is Licensed Under The CC-BY-SA 4.0 License And Code Samples Are Licensed Under The GPL 3.0 License. For Details, See License.