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

13 Responses to Not every weakly constant function is conditionally constant

Martin Escardo says:

12 June 2015 at 16:50

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.

Martin Escardo says:

12 June 2015 at 18:47

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:
  
  14 June 2015 at 10:33
  
  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.
  
Nicolai Kraus says:

14 June 2015 at 20:21

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.

- Mike Shulman says:
  
  15 June 2015 at 10:07
  
  Ah, very interesting! Yes, I had wondered whether homogeneity of path spaces could be used as well, but didn’t get anywhere either.
  
Martin Escardo says:

15 June 2015 at 16:48

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:
  
  15 June 2015 at 17:25
  
  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.
  
almostrational says:

16 June 2015 at 16:56

Reblogged this on Almost Rational.

Pingback: Universal Properties of Truncations | Homotopy Type Theory
Pingback: Constructing the Propositional Truncation using Nonrecursive HITs | Homotopy Type Theory
Jason Gross says:

1 February 2021 at 08:41

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.

- Mike Shulman says:
  
  1 February 2021 at 10:31
  
  No, I never got around to formalizing enough group theory.
  
  - Jason Gross says:
    
    1 February 2021 at 12:13
    
    Ah, that’s too bad. Is the partial work you had available somewhere?