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

Not every weakly constant function is conditionally constant

Not every weakly constant function is conditionally constant

Recommend

Constructing the Propositional Truncation using Nonrecursive HITs

A new class of models for the univalence axiom

Real-cohesive homotopy type theory

Combinatorial Species and Finite Sets in HoTT

HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics

Parametricity, automorphisms of the universe, and excluded middle

Type theoretic replacement & the n-truncation

A hands-on introduction to cubicaltt

In memoriam: Vladimir Voevodsky

Impredicative Encodings of Inductive Types in HoTT

About Joyk