Previously: Modeling Identity Types.

On first viewing, the identity type seems odd. Does it make sense to replace the traditional yes/no equality predicate with an elaborate type of equality proofs? In fact the father or modern type theory Martin Löf had his doubts, and initially tried to reflect all identity proofs into more basic judgmental or definitional equalities. This turned out to be too restrictive for many applications.

Still, some modern theorem provers like Lean impose the uniqueness of identity proofs (UIP) condition as an axiom. This so called axiom K states that reflexivity:

\text{refl} (a) : \text{Id}_A (a, a)

is the only possible proof of equality. Two things are equal if they are the same thing, otherwise they’re not. This works for most common data types.

Universes

There is, however, a much more interesting use case for non-trivial identity types. This happens when we apply equality to types themselves.

Since type theory is all about types, the question naturally arises, what is a type of a type? In Haskell, we call it a kind and denote as Type (or *, in legacy code).

In type theory we say that types form a universe. In Agda, the lowest such universe, U_0, is called Type l-zero (level zero), often abbreviated to Type. Of course, this begs the next question, what is the type of Type? Well, Type is a member of the next universe U_1, and so on, ad infinitum.

But if Type is a type then, like all types, it must be equipped with its own identity type. In other words, we should be albe to compare types for equality. The most obvious choice would be to say that two types are equal if they are isomorphic. We define an isomorphism as a pair of functions that are the inverse of each other. This makes perfect sense for sets, but we don’t want to treat types as sets. Types have more structure: every type comes equipped with its own identity type.

Equivalences

We’ve seen before that to model identity types we may look at homotopy theory. We model types as topological spaces and equality as continuous paths between points. The notion of isomorphism is too strong for comparing such spaces. What we need is an equivalence, which is an isomorphism modulo equality.

Indeed, we don’t need the round trip to land us exactly where we started — it’s enough that we land at a point that is equal to the original point. Here, equal means: there is a path that connects these two points. And once we have loosened the definition of what an inverse is, there is no reason to insist that the right inverse be the same as the left inverse. We can as well use two different functions, g and h.

Thus a function f \colon A \to B is called an equivalence iff:

  • there exists a function g \colon B \to A such that the composite f \circ g \sim id_B\;, that is \forall b \colon B . \; f (g\, b) =_B b
  • there exists a function h \colon B \to A such that the composite h \circ f \sim id_A, that is \forall a \colon A . \; h (f \, a) =_A a.

If such functions exist, we say that A is equivalent to B, A \simeq B.

Univalence

Equivalence is the only relation between types that behaves exactly like equality. Can we use it to define equality of types? This is what Vladimir Voevodsky postulated as the axiom of univalence.

For any A and B in a universe U, we postulate that:

(A =_U B) \simeq (A \simeq B)

in other words, equality is equivalent to equivalence.

Equivalences are much easier to prove than equalities. However, without univalence, they don’t satisfy the rule of substitution of equals for equals. This rule formulated by Leibniz reads: “Two terms are the same if one can be substituted for the other without altering the truth of any statement.”

In Martin Löf type theory it’s impossible to define a predicate that would distinguish between equivalent types. This is why imposing the axiom of univalence to extend type theory makes perfect sense.

Mathematician often apply the substitution rule to terms that are isomorphic rather than equal, essentially leaving the proof of the validity of a substitution as an “exercise to the reader.” Univalence legitimizes this practice and leads to substantial simplification of many mathematical proofs.

However, just like with isomorphisms, there may be several equivalences between two types. In fact, a type can be equivalent to itself in more than one way. For instance, not is a non-trivial equivalence for Bool — it’s clearly different from id. By univalence, such different equivalences introduce different equalities. Uniqueness of identity proofs is thus incompatible with univalence.

Higher Inductive Types

If identity is a type like any other, then we may use it to define types that contain their own proofs of identity. Such types are called higher inductive types. The simplest example is the circle, which you may think of as a singleton \text{base} plus a proof \text{loop} that \text{base} is equal to itself. In Agda, which is a dependently typed language, this translates to:

data S¹ : Type where
  base : S¹
  loop : base ≡ base

Here, base ≡ base denotes the type \text{Id}_{S^1} (\text{base}, \text{base}).

This definition is somewhat similar to, say, the definition of a boolean type:

data Bool : Type where
  true  : Bool
  false : Bool

except that, in the definition of the circle, the type of the second component depends on the value of the first component. This definition introduces explicitly an element of the identity type, \text{loop}, that is not \text{refl}. It is therefore incompatible with axiom K.

Higher inductive types can be used to prove theorems in topological homotopy. Such proofs would normally involve topology, but in HoTT they are just statements about types. They can be formalized using theorem provers, like Agda.

I’m grateful to Thorsten Altenkirch for valuable comments on the draft of this post.