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):

`X`

is h-separated, i.e.`∀ x y → (x ≡ y)* → x ≡ y`

`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`

`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

`A`

is h-stable, i.e.`A* → A`

`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:

`X`

is h-separated, i.e.`∀ x y → (x ≡ y)* → x ≡ y`

`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`

`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:

`A`

is h-stable, i.e.`A* → A`

`A`

has a constant endofunction, i.e.`f: A → A`

and a proof of`∀ a b → fa ≡ fb`

`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?

Nice! From the point of view of categorical semantics, being h-stable means having a “split support” — the h-prop reflection is categorically called the “support” (the image of the map to the terminal object) and h-stability says that the map from a type to its support is split. On the other hand, a constant endofunction is necessarily idempotent, and it makes sense that when you split such an idempotent, what you get is the support.

Can’t you just look at semantics in some locally cartesian closed category that doesn’t have any images?

A question for which we don’t know the answer is whether (h-stable X)* for all types X is provable. This shouldn’t be the case. If it were, then h-propositional reflection would definable in MLTT with function extensionality. This is discussed further in the Agda file linked in Nicolai’s post, in Section 4.

What is (h-stable X) ? Is it ?

I don’t really understand what you’re going for here: being an hprop is a much stronger condition than having a split support, i.e. being “h-stable”. Moreover, it is itself an hprop, whereas “being h-stable” is in general not.

X*->X is in general not inhabited. But is it hinhabited? That is, can you prove (X*->X)*? We very much doubt. If you have an argument why not, I would like to know.

Why do you say that would allow you to define h-propositional reflection in MLTT with function extensionality? The Agda file seems to say that if you had , then the h-prop reflection “X is hinhabited” would be equivalent to what is there called “X is populated”. But why does that imply that in the

absenceof the h-prop reflection, the type “X is populated” would still have the same universal property as “X is hinhabited”?Here is an argument. In the Agda file, we have hinhabited : Type -> Type, given by postulates, and we have hinhabited1 : Type -> Type1, defined explicitly in the usual way, making the universal property true but with the wrong size. Here X* is written hinhabited X. And we also have an obvious proof in the file that hinhabited X iff inhabited1 X, using both universal properties (one postulated, the other true). Hence if we have that hinhabited X iff populated X, we also have have hinhabited1 X iff populated X, and so populated X inherits the universal property from hinhabited1, which is definable in MLTT with universes Type and Type1, but now “populated X” has the universal property of the right size. We should implement this argument in the Agda file to clear any doubts and see whether it really works (I think it does).

In any case, it is interesting that populated can be defined in MLTT without any extensions as populated X = (f : X -> X) -> constant f -> fix f, where fix f is the type of fixed-points of f. Moreover, by Nicolai’s proof that fix f is an hproposition if f is constant, we have that populated X is an hproposition if function extensionality is available, and all this can be proved without having hpropositional reflection available. Now, including hpropositional reflections, (X*->X)* implies (populated X iff X*). Because both are propositions, we get an isomorphism and hence a w-equivalence.

This is why I think it would be interesting to have (X*->X)*. But, as I said, I very much doubt that this is the case. We would like to have an answer to this question!

Thanks, that seems plausible. I forgot that “MLTT” includes lots of universes.

I agree it does seem unlikely that . Categorically, this seems to be the roughly the assertion that all subterminal objects are internally projective. I doubt that is the case, but I’m having trouble thinking of any counterexamples offhand.

What is somewhat puzzling is this. We know that we cannot inhabit the type (X*->X) in general. What we don’t know is whether we can always h-inhabited it. But we can always populate it. Population is much stroger that non-emptiness. (If from non-emptiness we can always get population, the excluded middle for h-proposition follows). But knowing this doesn’t seem to help.

This is an interesting connection with Hedberg’s theorem. Incidentally, Bas Spitters and I are working on similar ideas from a different perspective and we found the following.

For any type A, the -truncation of A is a strict coequalizer of the two projections in the following sense:

The function denotes the canonical map to the truncation. This is _not_ a homotopy coequalizer. It is a bit stronger since it is a coequalizer for more cocones (some data in the cocones should be truncated).

There is a special case one can consider here and it is if the identity function admits a homotopy . In that case, the strict coequalizer property of above gives that is a retract of . Also, if a type is a retract of a type of level n, then is itself of level (this is a lemma in Voevodsky’s files, see library uu0). Generalization (i) of Hedberg’s theorem at the beginning of the post is this observation in the case .

That doesn’t seem right to me. Take ; then your projections are . Let , so that . Suppose

fis constant at some point . Then to give with a homotopy amounts to giving a loop inXbased atx, which is not generally a contractible space.In particular, I think the rules for bracket types in the Awodey-Bauer paper aren’t quite right when eliminating into non-hsets.

Suppose instead of _* we’re allowed joins and ordered colimits.

The definition of “constant function” here is equivalently that there is an extension of to the (unreduced) join along the usual inclusion — I think this must be something of what Mike is getting at here, but he may correct me if not. But for an

endofunction, that means we have, among other things, an actual map ; and then, since is fine for a bifunctor, a map , which one can then compose… and then by cellular induction, a map from the colimit of all these iterated joins, which is contractible as soon as there is a term in and certainly empty if is empty.But I’m glad that an argument from reflection-in-subsingletons directly also works! Among other things, it means the cellular argument can be concentrated in formalizing that the iterated join colimit is a reflection-in-subsingletons.

Sorry; of course you can see where I dropped my latexs…

I put the latex back where it belongs.

I’m not sure what “cellular induction” means in type theory, or why that colimit is necessarily contractible. But in general, I think you do need *some* kind of fancier colimit than just a coequalizer, although I would be more inclined to consider a sort of Cech nerve.

Sorry, I dropped into nonstandard informal speak; one does an induction on the dimension of a cell. But the contractibility of an infinite join of a thing with a term in it is easy: a path to the image of included by one copy of can be constructed by first connecting everything in the join of the first copies to the same thing in the join of the copies 2 through , and then via the join back to .

I said cellular induction

in type theory, where types don’t generally have cells or dimensions of them. But it sounds maybe like you are talking about classical homotopy theory instead?Well, yes, probably; and of course I am not a type theorist by any stretch, anyways; but being an informal description, it is meant to suggest a proof one might try to write, if he had definitions/hypotheses of join and colimit handy, whether in xTT or or whatever. Of course, the cells aren’t a feature of the space even then, but of a

presentationof the space; indeed the constructors of a Type aren’t intrinsic to the type itself — nat doesn’t know that its terms are zero or successors, it’s C(co)IC that knows this, and it’s us who prove things about nats from that dichotomy.