At the core of homotopy type theory (and its predecessors) is the idea of propostions as types. Namely, we interpret logical propositions - statements that are either true or false, as types, with a proposition being true if and only if the corresponding type has an element (i.e., there is an object with that type). The Curry-Howard correspondence lets us embed all of logic into type theory in the manner.

True and False

We begin by representing the two simplest propositions: true - always true, and false.

1
2
3
4
5

data True : Set where
  qed : True


data False : Set where

The $True$ type has just one constructor, giving an object with type $True$. On the other hand, the $False$ type has no constructors, so there are no objects of type $False$.

There are various ways of building propositions from other propositions. We see how these translate to constructions of types.

Logical implies

If $P$ and $Q$ are propositions, which we identify with their corresponding types. We interpret the proposition $P \implies Q$ as the function type $P \to Q$.

Some deductions

Modus Poens is the rule of deduction (due to Aristotle) that says that if the proposition $P$ is true, and $P$ implies $Q$, then $Q$ is true. We can prove this in the types interpretation. Namely, Modus Poens transaltes to the statement that if we have an objects of type $P$ and $P \to Q$, then we have an object of type $Q$. We get an object of type $Q$ by function application.

1
2

moduspoens : {P : Set} → {Q : Set} → P → (P → Q) → Q
moduspoens p imp = imp p

Next, we see my favourite method of proof - vacuous implication. This says that a false statement implies everything, i.e., for any proposition $P$, we have $False \implies P$, which in type theory says $False\to P$ has objects.

As the $False$ type has no cases at all, a function is defined on $False$ by using an absurd pattern, which just says that there are no cases, so no definition is needed.

1
2

vacuous : {A : Set} → False → A
vacuous ()

Even and Odd numbers

Next, we define a type family Even n which is non-empty if and only if n is even. To do this, we see that a number is even if and only if it is even as a consequence of the rules

• $0$ is even.
• If $n$ is even, so is $n + 2$.
• Thus, we can define the inductive type family:

1
2
3

data Even : ℕ → Set where
  zeroeven : Even zero
  +2even : {n : ℕ} → Even n → Even (succ (succ n))

We can prove that $2$ is even by applying the second rule, with $n=0$, to the first rule (telling us that $0$ is even).

1
2

2even : Even 2
2even = +2even zeroeven

We next show that $1$ is odd. This means that we have to show that the type $Even 1$ is empty. While rules let us construct objects, and verify their types, there is no rule that tells us directly that a type is empty.

However, there is a nice way of capturing that a type $A$ is empty - if there is a function from $A$ to the empty type $False$, then $A$ must be empty - there is nowhere for an object of type $A$ to be mapped.

Indeed, what we prove is that there is a function from $Even\ 1$ to $False$ ; we define this using an absurd pattern.

1
2

1odd : Even 1 → False
1odd ()

The identity type

One of the most fundamental concepts in homotopy type theory is the identity type family, representing equality between objects with a given type. This is an inductive type family, generated by the reflexivity constructor giving an equality between an object and itself.

1
2

data _==_ {A : Set} : A → A → Set where
  refl : (a : A) → a == a

Note that while this is an inductive type family, for a fixed object a the type $a==a$ is not an inductive type defined by $refl(a)$, i.e., we cannot define (dependent) functions on this type but just defining them on the reflexivity constructor. This is a subtle point, which will become clearer as we look at the topological interpretation. We shall study the identity type extensively.

For now, let us show some basic properties of the identity type. All these are proved by constructing objects by pattern matching (recall that these are dependent functions, so we are formally constructing them by induction, not recursion).

Firstly, if $f$ is a function and $a==b$ (i.e., there is an object of type $a==b$), then $f(a)==f(b)$ (again, we mean there is an object of this type).

1
2

transfer : {A : Set} → {B : Set} → {x y : A} → (f : A → B) → x == y → f(x) == f(y)
transfer f (refl a) = refl (f a)

Further, we see that equality (given by the identity type) is symmetric and transitive.

1
2

symm : {A : Set} → {x y : A} → x == y → y == x
symm (refl a) = refl a

1
2

_transEq_ : {A : Set} → {x y z : A} → x == y → y == z → x == z
(refl a) transEq (refl .a) = refl a

There is a new Agda feature we have used in the proof of transitivity: the dot notation. Notice that we have a term .a - this says that we can deduce, from the types, that $a$ is the only possibility at its position in the pattern.

For all

Suppose we have a type $A$ and a family of types $P(a)$ (which we regard as propositions), with a type associated to each object $a$ of type $A$. Then all the types $P(a)$ have objects (i.e., all corresponding propositions are true) if and only if there is a dependent function mapping each object $a$ of type $A$ to an object of type $P(a)$. Thus, the logical statement

translates to the product type

In Agda, we represent the product type as $(a : A) \to P(a)$

A proof by induction

We can now prove a more substantial result. Namely, suppose we have a function $f : \Bbb{N}\to \Bbb{N}$ , and suppose for all $n\in \Bbb{N}$ we have $f(n) = f(n+1)$, then we show that, for all $n$, $f(n)=f(0)$.

Such a statement is normally proved by induction (indeed any proof must reduce to induction). We see that our pattern matching rules for constructing dependent functions suffice to prove this - this is why the dependent function that gives them is called the induction function.

1
2
3

constthm : (f : ℕ → ℕ) → ((m : ℕ) → (f (succ m)) == (f m)) → (n : ℕ) → (f n) == (f 0)
constthm f _ 0 = refl (f 0)
constthm f adjEq (succ n) = (adjEq n) transEq (constthm f adjEq n)

Let us look at the statement and proof more carefully. Firstly, note that the statement is of the form

As we have seen, the first term is a translation of $\forall f : \Bbb{N} \to \Bbb{N}$, so the statement says that for all functions $f : \Bbb{N} \to \Bbb{N}$ (or any other codomain with obvious modifications), we have $P(f) \to Q(f)$.

This in turn is a translation of $P(f) \implies Q(f)$. So we can regard $P(f)$ as the hypothesis, for a fixed function $f$, and $Q(f)$ as the desired conclusion.

The hypothesis P(f) is the statement

which is just the statement that for all $m$, $f(m+1)=f(m)$. Finally, the conclusion $Q(f)$ just says that $f(n)=f(o)$ for all $n$.

We now look at the proof. The two constructors correspond to the base case and the induction step. Here the base case is just $f(0)=f(0)$, which follows from reflexivity of equality.

The induction step is more complicated. We prove the result for $n+1$ assuming the result for $n$. The main hypothesis $\forall m, f(m+1) = f(m)$, is, by pattern matching, $adjEq$. The right hand side, which is the proof in the case of $n+1$, is obtained from:

• The hypothesis for $n$, giving $f(n+1) = f(n).$
• The induction hypothesis, which is the theorem we are proving applied to $n$, giving $f(n)=0.$
• Transitivity of equality.
• The proof is obtained by applying the function corresponding to the transitivity of equality to the two objects corresponding to the other ingredients above.

This proof is remarkable in many ways. First of all, note that this is no longer or more complicated than an informal proof. Further, note that we did not have to invoke the usual induction axiom schema, but instead just used the rules for constructing objects. Most significantly, as most of our types are inductive type (or type families), we get recursive definitions and inductive proofs in all these cases.

Indeed, using recursive definitions for inductive types we get all so called universal properties. Furthermore, traditionally universal properties require a separate uniqueness statement. But recursion-induction is powerful enough to even give the uniqueness statements for universal properties. This means a great deal of mathematical sophistication (universal algebra, various aspects of category theory) are encapsulated in these simple functions.

More types for propositions

We now see the types corresponding to the other ways of combining propositions : and, or and there exists.

Firstly, if $A$ and $B$ are types corresponding to propositions, then there are objects with each of these types if and only if there is a pair $(a, b)$ of the pair type $A \times B$, which we define as follows.

1
2

data _×_ (A B : Set) : Set where
  [_,_] : A → B → A × B

We have to use square brackets as parenthesis have a special meaning in Agda. Observe that there is a single constructor that takes as input an object in $A$ and an object in $B$. We regard the result as the pair.

Next, suppose $A$ and $B$ are types corresponding to propositions and we wish to construct a type corresponding to $A$ or $B$, then we require a type whose elements are elements of $A$ and elements of $B$, or more accurately the images of such elements under constructors. This is the direct sum type.

1
2
3

data _⊕_ (A B : Set) : Set where
  i₁ : A → A ⊕ B
  i₂ : B → A ⊕ B

Finally, if we are given a collection of types $B(a)$ for objects $a$ of type $A$, we construct the type corresponding to at least one of these types having an element, i.e., a there exists type.

1
2

data Σ(A : Set) (B : A → Set) : Set where
  ι : (a : A) → B a → Σ A B

Notice that the constructor for this type has as input an element $a$ and an element of type $B(a)$. Such elements exist if and only if some $B(a)$ is non-empty, i.e., the corresponding proposition is true.

As we see, we can express all the usual mathematical statements using types built up using our basic constructions: inductive types, functions and dependent functions. We have also seen that the basic rules for constructing objects are powerful rules of deduction. However, there are some things they cannot deduce, for instance the statement (called the axiom of extensionality) that if $f, g: A\to B$ are function with $f(a)=g(a)$ for all $a \in A$, then $f=g$. Hence, we have to introduce this as a postulate - we just postulate that there is an object (which we give a name) of a given type.

1
2

postulate
  extensionality : {A B : Set} → (f g : A → B) → ((x : A) → (f x) == (g x)) → f == g

We can similarly introduce axioms specific to a domain, say Euclidean geometry, by postulating them in a module.