Thorsten Altenkirch, Thierry Coquand, Martin Escardo, Nicolai Kraus

Overview

Hedberg’s theorem states that decidable equality of a type implies that the type is an h-set, meaning that it has unique equality proofs. We describe how the assumption can be weakened. Further, we discuss possible improvements if h-propositional reflection (“bracketing”/”squashing”) is available. Write X* for the h-propositional version of a type X. Then, it is fairly easy to prove that the following are logically equivalent (part of which Hedberg has done in his original work):

1. X is h-separated, i.e. ∀ x y → (x ≡ y)* → x ≡ y
2. X has a constant endofunction on the path spaces, i.e. we have a function f: (x y: X) → x ≡ y → x ≡ y and a proof that f x y is constant for all x and y
3. X is an h-set, i.e. ∀ x y: X → ∀ p q: x ≡ y → p ≡ q

We then state the three properties for arbitrary types instead of path spaces. For a type A, the first two statements become

1. A is h-stable, i.e. A* → A
2. A has a constant endofunction, i.e. f: A → A and a proof of ∀ a b → fa ≡ fb

Clearly, the first statement is at least as strong as the second, but somewhat surprisingly, the second also implies the first. The proof of this fact is non-trivial.
In this blog post, we mainly talk about the mentioned results and try to provide some intuition. This is actually only a small part of our work. Many additional discussions, together with formalized proofs, can be found in this Agda file. Thanks to Martin, it is a very readable presentation of our work.

Generalizations of Hedberg’s Theorem

Having this proof of Hedberg’s Theorem in mind, the essence of the theorem can be read as:

(i) If we can construct an equality proof whenever we have h-propositional evidence that there should be one, then the type is an h-set.

Here, we call a type h-propositional (or an h-proposition) if all its elements are equal. Intuitively, decidable equality is much stronger than the property mentioned above: If we have a function dec that decides equality and x, y are two terms (or points), we do not even require evidence to get a proof that they are equal. Instead, we can just apply dec to get such a proof or the information that none exists.

It is therefore not surprising that Hedberg’s theorem can be strengthened by weakening the assumption. For example, a proof of ¬¬ x ≡ y could serve as evidence that x, y are equal; and indeed, if we know that a type is separated, i.e. that we have ∀ x y → (¬¬ x ≡ y) → x ≡ y, then the type is an h-set. This requires a weak form of extensionality (to show that ¬¬ x ≡ y is an h-proposition) and the controverse is not true.

In the presence of h-propositional reflection, we can do much better. We define h-propositional reflection as an operation _* from types to h-propositions (viewed as a subsets of types) that is left adjoint to the embedding, i.e. we have a universal property. These are Awodey’s and Bauer’s bracket types: The idea is that, given a type X, the type X* corresponds to the statement that there exists an inhabitant of X (we say that X is h-inhabited if we have p: X*). We always have the map η: X → X*. From X*, we do usually not get X, but if we could prove an h-proposition from X, then X* is sufficient. It is natural to consider h-propositional reflection in our context, because the informal notion “h-propositional evidence, that a type is inhabited” can now directly be translated. We call a type satisfying (i) in this sense h-separated: h-separated X = ∀ x y → (x ≡ y)* → x ≡ y.

In Hedberg’s original proof, it is shown that a constant parametric endofunction on the path spaces is enough to ensure that a type is an h-set. For a function f, we define that f is constant by constant f = ∀ x y → fx ≡ fy. As already mentioned above, it is fairly straightforward to show:

Theorem. For a type X, the following properties are logically equivalent:

1. X is h-separated, i.e. ∀ x y → (x ≡ y)* → x ≡ y
2. X has a constant endofunction on the path spaces, i.e. we have a function f: (x y: X) → x ≡ y → x ≡ y and a proof that f x y is constant for all x and y
3. X is an h-set, i.e. ∀ x y: X → ∀ p q: x ≡ y → p ≡ q

For this reason, we consider h-separated X → h-set X the natural strengthening of Hedberg’s theorem. The assumption is now the exact formalization of the condition in (i), the assumption is as weak as it can be (as it is necessary) and, in particular, it is immediately implied by Hedberg’s original assumption, namely the decidable equality property.

H-propositional Reflection and Constant Endofunctions

The list of equivalent statements above suggests that one could look at these statements for an arbitrary type A, not only for the path spaces. Of course, they do not need to be equivalent any more, but they become significantly simpler:

1. A is h-stable, i.e. A* → A
2. A has a constant endofunction, i.e. f: A → A and a proof of ∀ a b → fa ≡ fb
3. A is an h-proposition, i.e. ∀ a b: A → a ≡ b

For the third, it is pretty clear what this means and it is obviously strictly stronger than the first and the second. If A is h-stable, we get a constant endofunction by composing η: A → A* with A* → A. However, it is nontrivial whether a type with a constant endofunction is h-stable. Somewhat surprisingly, it is.

But let us first consider the question we get if we drop the condition that we are dealing with endofunctions. Say, we have f: X → Y and a proof c: constant f. Can we get a function X* → Y?
Consider the chaotic equivalence relation on X, which just identifies everything: x ~ y for all x and y, which is h-propositional (~: X → X → hProp with x ~ y = True for all x and y, if we want). According to the usual definition of a quotient, our constant map f can be lifted to X/~ → Y. So, what we asked can be formulated as: Does X* have the properties of X/~? If Y is an h-set, this lifting exists (Voevodsky makes use of this fact in his definition of quotients), but otherwise, our definition of constant is too naïve, as it involves no coherence conditions at all. If we know that Y has h-level n, we can try to formulate a stronger version of constant that solves this issue. This could be discussed at another opportunity. With the naïve definition of constant, we would have to make a non-canonical choice in X, but f only induces an “asymmetry” in Y.

Let us get back to the case where f is a constant endofunction. We still do not have the coherence properties mentioned above, but the asymmetry of Y is now an asymmetry of X and, somewhat surprisingly, this is sufficient. We have the following theorem:

Theorem. A type X is h-stable (X* → X) iff it has a constant endofunction.

Note that the direction from right to left is easy. For the other direction, we need the following crucial lemma:

Fixpoint Lemma (N.K.). If f: X → X has a proof that it is constant, then the type of fixed points Σ(x:X) → x ≡ fx is h-propositional.

Let us write P for the type Σ(x:X) → x ≡ fx. A term of P is a term in X, together with the proof that it is a fixed point. With the lemma, we just have to observe that there is the obvious map X → P, namely λx → (fx , constant x fx) to get, by the universal property of *, a map X* → P. Composed with the projection map P → X, this gives us the required map showing that X is h-stable.

To prove the lemma, we need the following two observations. For both, we assume that X, Y are types and x,y: X terms. Further, we write p • q for trans p q, so that this typechecks if p: x ≡ y and q: y ≡ z. We use subst (weak version of J) and cong (to apply functions on proofs) in the usual sense.

Observation 1. Assume h, k: X → Y are two functions and t: x ≡ y as well as p: h(x) ≡ k(x) are paths. Then, subst t p is equal to (cong h t)⁻¹ • p • (cong k t).

This is immediate by applying the equality eliminator on (x,y,t). We will need this fact for a proof of type t : x ≡ x, but this required special case cannot be proved directly.

The second observation can be considered the key insight for the Fixpoint Lemma:

Observation 2. If f: X → Y is constant, then cong f maps any proof of x ≡ x to reflexivity.

It is not possible to prove this directly. Instead, we formulate the following generalization: If c: constant f is the proof that f is constant, then cong f maps any proof p: x ≡ y to (c x x)⁻¹ • (c x y). This is immediate by using induction (i.e. the J eliminator) on (x,y,p), and it has the above statement as a consequence.

Proof (of the Fixpoint Lemma). Assume we have f: X → X, c: constant f and (x,p), (x',p'): Σ (x: X) → x ≡ fx. We need to show that these pairs are equal. It is easy to prove x ≡ x' by composing the proofs p: x ≡ fx, constant x x': fx ≡ fx' and (p')⁻¹: fx' ≡ x'. We call this proof p'': x ≡ x'. Clearly, we have that (x, subst (p'')⁻¹ p') and (x',p') are equal now, just by the proof p'' for the first component, and the equality of the second components is immediate. We choose to write q for the proof subst (p'')⁻¹ p'. Now, we are in a slightly simpler situation: We need to show that (x,p) and (x,q) are equal.

If we prove that the first components are equal using some proof t: x ≡ x, then what we need for the second components is p ≡ subst t q. Clearly, using refl for t would not work.

By Observation 1, our goal is equivalent to proving p ≡ t⁻¹ • q • (cong f t).
Using Observation 2, this simplifies to p ≡ t⁻¹ • q. Let us therefore just choose t to be q • p⁻¹. This completes the proof of the Fixpoint Lemma and the Theorem. □

As mentioned, there is a bunch of possible further questions and considerations, but for now, we want to conclude with a question that we are not so sure about anymore: Is h-propositional reflection definable in MLTT (with extensionality)? With heavy use of the Fixpoint Lemma, we have come fairly close to such a definition. It should not be possible, but is there a proof of that fact?