Quest 1 - Dependent Types

In a “place to do maths” we would like to be able to express and “prove” the statement

The statement

There exists a natural that is even.

The goal of this quest is to define what it means for a natural to be even.

Part 0 - Predicates / Dependent Constructions / Bundles

This requires the notion of a predicate. In general a predicate on a type A : Type is a term of type A Type. For example,

isEven :   Type
isEven n = ?
  • Do C-c C-l to load the file.

  • Navigate to the hole.

  • Input n in the hole and do C-c C-c. You should now see

    isEven :   Type
    isEven zero = {!!}
    isEven (suc n) = {!!}

    It says “to define a function on , it suffices to define the function on the cases, zero and suc n, since these are the only constructors given in the definition of ”. This has the following interpretations :

    • propositionally, this is the principle of mathematical induction.

    • categorically, this is the universal property of a natural numbers object.

  • Navigate to the first hole and check the goal. You should see

    Goal: Type

    Fill the hole with , since we want zero to be even.

  • Navigate to the second hole.

  • Input n and do C-c C-c again. You should now see

    isEven :   Type
    isEven zero = ⊤
    isEven (suc zero) = {!!}
    isEven (suc (suc n)) = {!!}

    We have just used induction again.

  • Navigate to the first hole and check the goal. agda should be asking for a term of type Type, so fill the hole with , since we don”t want suc zero to be even.

  • Navigate to the next hole and check the goal. You should see in the *Agda information* window,

    Goal: Type
    n : ℕ

    We are in the “inductive step”, so we have access to the previous natural number.

  • Fill the hole with isEven n, since we want suc (suc n) to be even precisely when n is even. The reason we have access to the term isEven n is again because we are in the “inductive step”.

  • There should now be nothing in the *Agda information* window. This means everything is working. (Compare your isEven with our solutions in Quest2Solutions.agda.)

Part 1 - Interpretations of Bundles

The interpretations of isEven : Type are

  • Propositionally : Already mentioned, isEven is a predicate on .

  • As a construction : isEven is a dependent construction. Specifically, isEven n is either or depending on n : .

  • Geometrically : seen as a map from the space to the space of spaces Type, isEven assigns for every point n in a space isEven n. Pictorially, it looks like


    We say isEven is a bundle of spaces over , or simply a bundle over for short. The space isEven n lying above each n is called the fiber over n. In this particular example the fibers are either empty or singleton.


    In the above picture, we have implicitly drawn as a bunch of “disconnected” points, i.e. a discrete space. See a later arc where this is justified.

  • Categorically : isEven is an object in the over-category Type↓ℕ.

In general given a type A : Type, a dependent type F over A is a term F : A Type. This should be drawn as a collection of space parameterised by the space A.


You can check if 2 is even by asking agda to “reduce” the term isEven 2 (do C-c C-n, “n” for normalize) and type in isEven 2. (You can write in numerals since we are now secretly using from the cubical agda library.)

Part 2 - Using the Trinitarianism

We introduced new ideas through each perspectives, as each has their own advantage

  • Types as propositions is often the most familiar perspective, and hence can offer guidance for the other two perspectives. However the current mathematical paradigm uses “proof irrelevance” (two proofs of the same proposition are always “the same”), which is not compatible with HoTT. We will expand on this later.

  • Types as constructions conveys the way in which “data” is important, and should be preserved.

  • Types as objects/spaces allows us to draw pictures, thus guiding us through the syntax with geometric intuition.

For each new idea introduced, make sure to justify it proof theoretically, type theoretically and categorically/geometrically.