In section 10.5 of the HoTT book, the cumulative hierarchy V is defined as a rather non-standard higher inductive type. We can then define a membership relation ∈ on this type, such that (V, ∈) satisfies most of the axioms of set theory. In particular, if we assume the axiom of choice, V models ZFC.

This post summarizes the work that I did during my masters internship with Bas Spitters. We formalized most of the results of section 10.5 of the HoTT book in Coq. Moreover, while trying to formalize exercise 10.11, we found out that the induction principle of V given in the book was not entirely correct. After discussions with Mike Shulman and Peter Lumsdaine, we defined a new induction principle which is more satisfactory.
The Coq code is available here. My internship report is available there.

Induction principle of V

First, let us recall the definition of the higher inductive type V. In pseudo-Coq code, it would be :

Inductive V : Type :=
 | set (A : Type) (f : A -> V) : V.
 | setext : forall (A B : Type) (f : A -> V) (g : B -> V),
    (∀a, ∃b, (f a = g b) /\ ∀b, ∃a, (f a = g b))
    -> set (A, f) = set (B, g).
 | is0trunc_V : IsTrunc 0 V.

The first constructor, set, is easily described by the framework of inductive types, and behaves as expected. The third one merely says that the type V is an h-set, and is also easily dealt with. The tricky constructor is the second one, setext. Indeed, its fifth argument refers to the identity type of V, which doesn’t really fit in our current understanding of higher inductive types. Worse, the existential ∃ hides a -1-truncation, which makes things even more complicated.

Fortunately, there is an alternative definition that allows us to bypass this issue : this is the purpose of exercise 10.11. Still, it would be interesting to have an induction principle associated to this definition. But what should it be ?

The (dependent) induction principle of V has the following form : in order to prove ∀ (x :V). P(x), we need to prove three conditions (one for each constructor). The condition for the 0-truncation constructor says that P(x) must be an h-set for all x. The one for set says that given A and f, and assuming that P(f(a)) is proved for all a : A, we must prove P(set(A, f)).

What about setext ? We are given A, B, f and g. Like for the first constructor, we also assume recursively that P(f(a)) and P(g(b)) are proved for all a and b. This means that we have two dependent functions, H_f : Π ({a : A} P(f(a)) and H_g : Π {b : B} P(g(b)).
We also know that f and g are such that ∀ a. ∃ b. (f(a) = g(b)) (and ∀ b. ∃ a …).
But since, as we said before, this property refers to the identity type of V, we must have another recursive assumption corresponding to it. An ill-typed version would be : ∀ a. ∃ b. (H_f(a) = H_g(b)). The problem here is that H_f(a) and H_g(b) are not of the same type, we must transport over some path p : f(a) = g(b). The intuitive idea would be to transport over the corresponding path that we get thanks to the hypothesis on f and g. But that path is hidden behind the truncated existential, so we cannot talk about it.

The induction principle given in the HoTT book formulates it this way:

∀ (p : f(a) = g(b)). p_* (H_f(a)) = H_g(b).

The problem is that, when trying to prove this induction principle from the one that we get from the alternative definition of exercise 10.11, we need to know that the path p over which we are transporting actually comes from the hypothesis on f and g. Hence, we cannot quantify over any p.

Our proposal is the following :

∀ a. ∃ b. ∃ (p : f(a) = g(b)). p* (Hf(a)) = Hg(b) (and ∀ b. ∃ a. ∃ p …).

This way, when proving the induction principle, we can choose p to be the path we need it to be. This makes the induction principle of V a bit weaker, but it is still able to prove all the results of the HoTT book.

Explicit Universes

An interesting point about our implementation is that we had to use one of the new features of Coq: the ability to explicitly specify the universe levels.

In order to prove one of the lemmas, the HoTT book defines a bisimulation relation on V, and proves that it is a smaller resizing of the equality in V. When doing this in Coq, even with the recent implementation of universe polymorphism by Matthieu Sozeau, we had to deal with quite a lot of universe inconsistencies. The solution was to use explicit universes. For example, instead of having ~: V → V → hProp, the type of the bisimulation relation becomes:

Definition bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}.

This ensures that the two arguments are in `the same V’‘, and that the bisimulation relation lives in a lower universe than the equality on V.