On h-Propositional Reflection and Hedberg’s Theorem

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?

About these ads

About Nicolai Kraus

Student at the University of Nottingham
This entry was posted in Code, Foundations. Bookmark the permalink.

17 Responses to On h-Propositional Reflection and Hedberg’s Theorem

  1. Mike Shulman says:

    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.

    Is h-propositional reflection definable in MLTT (with extensionality)? … It should not be possible, but is there a proof of that fact?

    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.

      • Steve Awodey says:

        What is (h-stable X) ? Is it X^* \to X?
        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.

      • Mike Shulman says:

        Why do you say that \forall X, (X^*\to X)^* would allow you to define h-propositional reflection in MLTT with function extensionality? The Agda file seems to say that if you had \forall X, (X^*\to X)^*, 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 absence of 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!

        • Mike Shulman says:

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

          I agree it does seem unlikely that \forall X, [[X]->X]. 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.

          • Martin Escardo says:

            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.

  2. Egbert Rijke says:

    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 n+1-truncation of A is a strict coequalizer of the two projections \pi_1,\pi_2:\sum(x,y:A),\ [ x \equiv y ]_n\to A in the following sense:

    \prod(X:\mathsf{Type})(f:A\to X)(H:f\circ\pi_1\sim f\circ\pi_2),\ \mathsf{isContr}\big(\sum(g:[ A]_{n+1}\to X),\ g\circ \tau_{n+1}\sim f\big)

    The function \tau_{n+1}:A\to [A]_{n+1} 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 \mathsf{idmap}_A:A\to A admits a homotopy \mathsf{idmap}_A\circ\pi_1\sim\mathsf{idmap}_A\circ\pi_2. In that case, the strict coequalizer property of above gives that A is a retract of [A]_{n+1}. Also, if a type A is a retract of a type B of level n, then A is itself of level n (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 n=1.

    • Mike Shulman says:

      That doesn’t seem right to me. Take n=-2; then your projections are \pi_1,\pi_2: A\times A\to A. Let A=1+1, so that [A]_{-1} = 1. Suppose f is constant at some point x:X. Then to give g: [A]_{-1}\to X with a homotopy g \circ \tau_{-1} \sim f amounts to giving a loop in X based at x, 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.

  3. Jesse McKeown says:

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

    The definition of “constant function” here is equivalently that there is an extension of f \sqcup f to the (unreduced) join A \star A 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 A \star A \to A; and then, since \star is fine for a bifunctor, a map A\star A \star A \star A \to A \star A, 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 A and certainly empty if A 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.

    • Jesse McKeown says:

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

    • Mike Shulman says:

      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.

      • Jesse McKeown says:

        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 a : A included by one copy of A can be constructed by first connecting everything in the join of the first n copies to the same thing in the join of the copies 2 through n + 1, and then via the join back to a.

      • Mike Shulman says:

        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?

        • Jesse McKeown says:

          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 (h-)colimit handy, whether in xTT or Ho^\infty(Top_*) or whatever. Of course, the cells aren’t a feature of the space even then, but of a presentation of 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.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s