Not every weakly constant function is conditionally constant

As discussed at length on the mailing list some time ago, there are several different things that one might mean by saying that a function f:A\to B is “constant”. Here is my preferred terminology:

  • f is constant if we have b:B such that f(a)=b for all a:A.
    This is equivalent to saying that f factors through \mathbf{1}.
  • f is conditionally constant if it factors through \Vert A \Vert.
  • f is weakly constant if for all a_1,a_2:A we have f(a_1)=f(a_2).

In particular, the identity function of \emptyset is conditionally constant, but not constant. I don’t have a problem with that; getting definitions right often means that they behave slightly oddly on the empty set (until we get used to it). The term “weakly constant” was introduced by Kraus, Escardo, Coquand, and Altenkirch, although they immediately dropped the adjective for the rest of their paper, which I will not do. The term “conditionally constant” is intended to indicate that f is, or would be, constant, as soon as its domain is inhabited.

It’s obvious that every constant function is conditionally constant, and \mathrm{id}_{\emptyset} shows the converse fails. Similarly, it’s easy to show that conditionally constant implies weakly constant. KECA showed that the converse holds if either B is a set or \Vert A \Vert \to A, and conjectured that it fails in general. In this post I will describe a counterexample proving this conjecture.

First of all, we have to be a little careful, because for general types none of the notions of constancy are mere propositions. So it’s a different thing to ask whether “weakly constant implies conditionally constant” or whether “merely weakly constant implies merely conditionally constant”. In fact, the latter is consistent, because it follows from \forall A, \Vert \, \Vert A \Vert \to A \Vert, which in turn follows from LEM (it is the “propositional axiom of choice”). In particular, in the simplicial set model, merely weakly constant does imply merely conditionally constant.

However, I claim that the stronger statement “weakly constant implies conditionally constant” is actually inconsistent with univalence. The consistency of the truncated version of the statement means that we can’t expect to exhibit a single counterxample to the stronger statement in the empty context. But we can hope to find a family of counterexamples, along the lines of Theorem 3.2.2 in the book, showing that there cannot be any uniform proof of conditional constancy from weak constancy. To do this, we will use two standard techniques for constructing counterexamples: (1) consider the universal case, and (2) make simplifying assumptions.

To start with, we’re looking for a family of functions f : \prod_{x:A} (B(x) \to C(x)) which are all weakly constant, but which are not all conditionally constant. A first simplification we can try is to let C:A\to \mathrm{Type} be a constant family, so that we’re looking for f : \prod_{x:A} (B(x) \to C).

But now, given A and B, there is a universal such family, where C = \sum_{x:A} B(x) and f is the pairing function. What does it mean to say that for all a:A the function b \mapsto (a,b) is weakly constant? Well, it means that for any a:A and b_1,b_2:B(a) we have an identification (a,b_1)=(a,b_2), which is to say we have p:a=a such that p_*(b_1) =b_2. In other words, the loops at a act “transitively” on the points of B(a). (Of course there is no hope of this happening nontrivially if A is a set, but we already knew we would need types that aren’t sets for our counterexample.)

Now let’s consider a universal case again: fix a type X and let A = \mathrm{B}\mathrm{Aut}(X) = \sum_{Z:\mathrm{Type}} \Vert Z = X \Vert, with B:A \to \mathrm{Type} the universal family defined by B(Z,e) = Z. Now weak constancy of each f(a,-) means that if \Vert Z=X\Vert, then the automorphisms of Z act transitively on Z, i.e. for any x,y:Z there is e:Z\simeq Z such that e(x)=y. This is something we’ve seen before: Nicolai called this property of Z being homogeneous. Types with decidable equality are homogeneous, including finite types, and decidable equality is preserved by mere equivalence (since it is itself a mere property). So now we have a bunch of examples of families of weakly constant functions, and we can ask whether any of them fail to be all conditionally constant.

Going back to a general A:\mathrm{Type} and B:A\to \mathrm{Type} with C = \sum_{x:A} B(x), what does it mean to say that for all a:A the function b \mapsto (a,b) is conditionally constant? Let’s suppose for simplicity that every type B(x) is inhabited, so that conditional constancy is the same as constancy. In that case, what we would be claiming is that there is a function g: A \to \sum_{x:A} B(x) such that for all a:A and b:B(a) we have (a,b) = g(a). Note that the first component of g need not be the identity map. However, we can re-express this by saying that the composite (\sum_{x:A} B(x)) \to A \xrightarrow{g} (\sum_{x:A} B(x)) is the identity, where the first map is the first projection. In other words, \sum_{x:A} B(x) would be a retract of A.

Now let’s go back to our examples of families of weakly constant functions, and pick one that’s easy to reason about: let X be a finite set of cardinality n. Then A = \mathbf{B}\mathrm{Aut}(X) = \mathbf{B} S_n is the classifying space of the symmetric group S_n, incarnated as the “type of finite sets of cardinality n“. What is \sum_{x:A} B(x)? It’s the type of pointed finite sets of cardinality n. Since this is connected, it is also the classifying space of a group, and in fact the group in question is S_{n-1}: an automorphism of a pointed n-element set must fix the basepoint, hence is uniquely determined by an automorphism of the remaining n-1 elements. Under this identification, the projection (\sum_{x:A} B(x)) \to A is identified with the map \mathbf{B}S_{n-1}\to \mathbf{B}S_n induced by the inclusion S_{n-1}\hookrightarrow S_n.

Thus, if our family of functions in this case were all conditionally constant, this map \mathbf{B}S_{n-1}\to \mathbf{B}S_n would have a retraction. Taking loop spaces, we conclude that S_{n-1}\hookrightarrow S_n would have a retraction in the category of groups. This is starting to look fishy, and indeed it is rarely the case. It’s true “by accident” for n=1,2,3,4, but after that it starts failing. For instance, when n=5, we have |S_5|=120 and |S_{4}|=24, so the kernel of any surjection S_5 \to S_4 would have cardinality 5; but since 5 is coprime to 24, all 5-cycles would have to be in that kernel, and there are more than five 5-cycles in S_5. Thus, it is false that our family of maps are all conditionally constant; and since they are all weakly constant, it is false that every weakly constant function is conditionally constant.

I enjoy this example quite a lot, because in addition to concepts from HoTT, it uses some not-entirely-trivial facts from finite group theory, notably Lagrange’s theorem. (Of course, it could be that there’s a much simpler counterexample waiting to be found; consider that a challenge!) I’ve almost finished formalizing it in the HoTT Coq library. What’s left is to show that 5-cycles have order 5 and that there are more than 5 of them, which should be straightforward but is a little tedious. (I would have waited to post this until the formalization was done, but Martín Escardó is going to give a related talk in Poland in a few weeks, and asked that I make this example public before then.)

This entry was posted in Univalence. Bookmark the permalink.

13 Responses to Not every weakly constant function is conditionally constant

  1. Thanks, Mike, for making this publicly available. It is nice to have this recorded. Your construction is very nice, and I am glad to see our conjecture proved.

    Perhaps I would like to say why I think this problem is interesting from a “constructive” point of view: sometimes you would like to get X, but you are able to get ||X|| only. If you wish to use the “weaker” information ||X|| to get Y, where Y is a proposition, you simply have to exhibit a function f:X->Y. That is, if from X you can get to Y, then the weaker information ||X|| is enough to get to Y. This is the definition of what the propositional truncation ||X|| is (the universal map of X into a proposition).

    More generally, as you say, if Y is a set and f is weakly constant, we can still get ||X||->Y from a constant function f:X->Y (so ||X|| is the set quotient of X by the chaotic equivalence relation). What you say is that if Y is not a set, the weak constancy of f is not enough in general.

    The next question is what conditions on f:X->Y are sufficient/necessary to get ||X||->Y, which is something Nicolai has looked at. But there are more related questions on the theme of when we can disclose the information “hidden” in ||X||, and it would be nice to understand this more generally.

  2. You proved that if every weakly constant function f:X->Y factors through ||X||, then univalence fails.

    The following is a positive proposition, which strengthens this (for if every type is a set, then univalance fails):

    Conjecture: If every weakly constant function f:X->Y factors through ||X||, then all types are sets.

    • Mike Shulman says:

      That’s an interesting conjecture! I don’t have any thoughts at the moment about how one might prove or disprove it though. It seems like it would require very different methods.

  3. This is great! I had also tried to find such a consequence, but I didn’t succeed. The “mysterious” construction that you have linked to also came from similar considerations. At that time, I had tried to use that any path space is transitive/homogeneous, in order to show Martin’s conjecture.

  4. Another remark is this. Intensional MLTT+||-|| is consistent with “global choice” Pi(X:U).||X||->X. But global choice trivially proves that every weakly constant function X->Y factors through ||X||. Combining this with your proof above, we see that the constant factorization question is independent of MLTT+||-||. But notice that global choice proves excluded middle (and the negation of univalence, as shown in the HoTT book). Hence it is still possible that the constant factorization hypothesis proves a “constructive taboo” in MLTT+||-||, in addition to the negation of univalence.

    • Mike Shulman says:

      But UIP also proves that every weakly constant function is conditionally constant; so if the latter were a constructive taboo, then so would UIP be, and it isn’t usually regarded as such.

  5. Pingback: Universal Properties of Truncations | Homotopy Type Theory

  6. Pingback: Constructing the Propositional Truncation using Nonrecursive HITs | Homotopy Type Theory

  7. Jason Gross says:

    Was the Coq formalization of this ever finished? I spent a couple of minutes looking for it in HoTT/HoTT and was not able to find it.

Leave a Reply

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

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

Facebook photo

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

Connecting to %s