Quest 0 - Terms and Types

There are three ways of looking at A : Type.

  • proof theoretically, “A is a proposition”

  • type theoretically, “A is a construction”

  • geometrically / categorically, “A is a space and Type is the category of spaces”.

A first example of a type construction is the function type. Given types A : Type and B : Type, we have another type A → B : Type which can be seen as

  • the proposition “A implies B”

  • the construction ways to convert A recipes to B recipes”

  • the space of maps from A to B, i.e. maps from A to B correspond to points of A → B.

  • internal hom of the category Type

To give examples of this, lets make some types first.

Part 0 - True / Unit / Terminal object

data ⊤ : Type where
  tt : ⊤

It reads “⊤ is an inductive type with a constructor tt”, with interpretations

  • ⊤ is a proposition “true” and there is a proof of it, called tt.

  • ⊤ is a construction “top” with a recipe called tt

  • ⊤ is the singleton space

  • ⊤ is a terminal object: every object has a morphism into ⊤ given by · ↦ tt

In general, the expression a : A is read “a is a term of type A”, and has interpretations interpretations,

  • a is a proof of the proposition A

  • a is a recipe for the construction A

  • a is a point in the space A

  • a is a generalised element of the object A in the category Type.

The above tells you how we make a term of type ⊤. Lets see an example of using a term of type ⊤:

TrueToTrue : ⊤ → ⊤
TrueToTrue = {!!}

  • enter C-c C-l (this means Ctrl-c Ctrl-l). Whenever you do this, agda will check the document is written correctly. This will open the *Agda Information* window looking like

    ?0 : ⊤ → ⊤
?1 : ⊤
?2 : ⊤

    This says you have three unfilled holes.

  • Now you can fill the first hole.

  • Navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward)

  • Enter C-c C-r. The r stands for refine. Whenever you do this whilst having your cursor in a hole, agda will try to help you.

  • You should see λ x → { }. This is agda notation for x ↦ { } and is called λ abstraction, think “λ for let”.

  • Navigate to the new hole

  • Enter C-c C-, (this means Ctrl-c Ctrl-comma). Whenever you make this command whilst having your cursor in a hole, agda will check the goal.

  • The goal (*Agda information* window) should look like

    Goal: ⊤
—————————————————————————
x : ⊤

    you have a proof/recipe/generalized element x : ⊤ and you need to give a proof/recipe/generalized element of ⊤

  • Write the proof/recipe/generalized element x of ⊤ in the hole

  • Press C-c C-SPC to fill the hole with x. In general when you have some term (and your cursor) in a hole, doing C-c C-SPC will tell agda to replace the hole with that term. agda will give you an error if it cant make sense of your term.

  • The *Agda Information* window should now only have two unfilled holes left, this means agda has accepted your proof.

    ?1 : ⊤
?2 : ⊤

There is more than one proof (see Quest0Solutions.agda). Here is an important one:

TrueToTrue' : ⊤ → ⊤
TrueToTrue' x = { }

  • Navigate to the hole and check the goal.

  • Note x is already taken out for you.

  • You can try type x in the hole and C-c C-c

  • c stands for cases”. Doing C-c C-c with x in the hole tells agda to do cases on x”. The only case is tt.

One proof says for any term x : ⊤ give x again. The other says it suffices to do the case of tt, for which we just give tt.

The same”

Are these proofs “the same”? What is “the same”?

(This question is deep and should be unsettling. The short answer is that they are internally but not externally the same.)

Built into the definition of ⊤ is the way agda can make a map out of ⊤ into another type A, which we have just used. It says to map out of ⊤ it suffices to do the case when x is tt”, or

  • the only proof of ⊤ is tt

  • the only recipe for ⊤ is tt

  • the only point in ⊤ is tt

  • the only one generalized element tt in ⊤

Lets define another type.

Part 1 - False / Empty / Initial object

data ⊥ : Type where

This reads “⊥ is an inductive type with no constructors”, with interpretations

  • ⊥ is a proposition “false” with no proofs

  • ⊥ is a construction “bot” with no recipes

  • ⊥ is the empty space

  • There are no generalized elements of ⊥ (it is a strict initial object)

We can make a map from ⊥ to any other type, in particular into ⊤.

explosion : ⊥ → ⊤
explosion x = {!!}

  • Navigate to the hole and do cases on x.

agda knows that there are no cases so there is nothing to do! (See Quest0Solutions.agda) Our interpretations:

  • “false” implies “true”. In fact the same proof gives “false” implies anything (principle of explosion)

  • One can convert recipes of ⊥ to recipes of ⊤. In fact the same construction gives a recipe of any other construction since there are no recipes of ⊥.

  • There is a map from the empty space to the singleton space. In fact given any space A , there is a map from the empty space to A.

  • ⊥ is has a map into ⊤. This is due to ⊥ being initial in the category Type.

Part 2 - The natural numbers

We can also encode “natural numbers” as a type.

data ℕ : Type where
  zero : ℕ
  suc : ℕ → ℕ

Our interpretations are:

  • ℕ has no interpretation as a proposition since there are “too many proofs” - mathematicians classically don’t distinguish between proofs of a single proposition. (ZFC doesn’t even mention logic internally, but type theory does.) In this sense constructions are proof relevant types.

  • As a construction :

    • ℕ is a type of construction

    • zero is a recipe for ℕ

    • suc takes an existing recipe for ℕ and gives another recipe for ℕ.

  • Categorically : ℕ is a natural numbers object in the category Type. This means it is equipped with morphisms zero : ⊤ → ℕ and suc : ℕ → ℕ such that given any ⊤ → A → A there exist a unique morphism ℕ → A such that the diagram commutes:

nno

  • Geometrically : ℕ is a space with a point zero and for every point n in ℕ, there is another point suc n in ℕ.

To see how to use terms of type ℕ, i.e. to induct on ℕ, go to Quest 1 - Dependent Types.

Part 3 - Universes

You may have noticed the notational similarities between zero : ℕ and ℕ : Type. The type Type has the following interpretations :

  • As a construction : any type of construction is a recipe for Type.

  • Geometrically : Type is a space of spaces. Each individual point in Type is a space.

This may have lead you to the question, Type : ?. In type theory, we simply assert Type : Type₁. But then we are chasing our tail, asking Type₁ : Type₂. Type theorists make sure that every type (i.e. anything the right side of :) itself is a term (i.e. anything on the left of :), and every term has a type. So what we really need is

Type : Type₁, Type₁ : Type₂, Type₂ : Type₃, ⋯

These are called universes. The numberings of universes are called levels. It will be crucial that types can be treated as terms. This will allows us to

  • talk about predicates i.e. “propositions depending on a variable”. E.g. the proposition “n is even” depends on a natural number n. See the next quest where we elaborate on this example.

  • reason about “structures” such as “the structure of a group”, to express “for all groups, …”

  • do category theory without stepping out of the theory. (For experts, we have Grothendieck universes.)

  • reason about when two types are “the same”, for example when are two definitions of the natural numbers “the same”? What is “the same”?