Mehran Baghi

HoTT for Cools

PDF | EPUB | MOBI | EDIT

Previous | Table of contents | Next

4. Type theory

4.1. Type theory versus set theory

Proposition: A statement susceptible to proof.

Theorem: A proposition that has been proven.

Deductive system: A collection of rules for deriving judgments.

Judgment (first order logic): For the proposition , “ 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:

EnglishType 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:

  1. Formation rules: How to form new types of this kind.

  2. Introduction rules (type’s constructors): How to construct elements of that type by:
    • Direct definition
    • -abstraction: When we don’t want to introduce a name for the function.
  3. Elimination rules (type’s eliminators): How to use elements of that type.

  4. Computation rule ( -reduction): How an eliminator acts on a constructor.

  5. Uniqueness principle ( -expansion) (optional): Expresses the uniqueness of maps into or out of that type.

  6. 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.

4.2. Function types

  1. Formation rules: Given types and , we can construct the type of functions with domain and codomain .

  2. Introduction rules:

    • Direct definition: Defining by where is a variable and is an expression which may use .

    • -abstraction:

  3. 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 .

  4. Computation rule: where is the expression in which all occurrences of have been replaced by .

  5. Uniqueness principle: . It shows that is uniquely determined by its values.

4.3. Universes and families

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 .

4.4. Dependent function types

  1. Formation rules: Given a type and a family , we may construct the type of dependent functions .

  2. 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:

  3. Elimination rules: Applying to an argument to obtain an element .

  4. Computation rule: Given we have and , where is obtained by replacing all occurrences of in by .

  5. 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.

4.5. Product types

  1. Formation rules: Given types we introduce the type , which we call their cartesian product.

  2. Introduction rules:

    • Direct definition: Given and , we may form .

    • -abstraction:

  3. Elimination rules: For any , we can define a function by

  4. Computation rule:

  5. 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.