By a weakly constant function one means a function which is equipped with a certain sort of “witness of constancy”.
However, in higher category theory and homotopy theory, it is debatable whether or not this witness really exhibits “constancy”, hence the use of a different word. (The term “steady function” was suggested by Andrej Bauer but did not catch on.)
In homotopy type theory, a function
is weakly constant if we have a term of type of the dependent product over the identification types of all the values of on all pairs of arguments:
By regarding homotopy type theory as the internal logic of an (∞,1)-topos, we obtain a definition that makes sense in any -category with binary products: a morphism is weakly constant if the two composites are equivalent.
If is constant in the sense that it factors through the terminal object (i.e. we have for some ), then is obviously weakly constant. The converse holds if we know that the domain is inhabited, for if , then for all . However, the identity function of the empty type is weakly constant, yet not equal to for any (since no such exists).
More generally, if factors through the propositional truncation , then it is weakly constant, since any two elements of are equal (i.e. it is an h-proposition). In fact, this is true if factors through any h-proposition (in which case it in fact also factors through , by the universal property of the latter).
The converse to this last implication does hold for some specific , such as:
If is an h-set. For then factors through the 0-truncation , and the set-coequalizer of the two projections is the propositional truncation.
If has split support. For then we have a composite , whose restriction to is equal to by weak constancy.
If , with and h-propositions. For then is the join of and , i.e. the pushout of the two projections . The universal property of this pushout says exactly that any weakly constant map factors through .
If (see below).
However, it can fail in general, even when is merely inhabited (i.e. ). For instance, let for h-propositions , , and , and let be the triple pushout of , , and under , , and . Then there is a steady map , but there exist models in which but has no global element. The most straightforward such model is presheaves on the poset of proper subsets of , with , , and . In this model, we have for all nonempty proper subsets , while , and has no global sections.
See this discussion.
In general, being weakly constant may be regarded as an “incoherent approximation” to constancy in the sense of factoring through an h-proposition. Indeed for a set , its propositional truncation is the set-coequalizer of . However, in general such a construction requires the realization of a whole simplicial diagram (the simplicial kernel of the map ).
While an arbitrary weakly constant function is not very coherent, a weakly constant endofunction has some extra degree of “coherence”, as witnessed by the following results of (KECA).
If is weakly constant, then the type is an h-proposition, and equivalent to .
Suppose , and let ; we want to show . Let be the concatenated path
It will suffice to show that , where denotes the action of on paths. However, the dependent action of on paths implies that for any and any , and in particular . From this is immediate. Thus, is an h-proposition.
Now we have a map defined by , so by the universal property of , we have . On the other hand, we have the first projection , and hence . Thus, these two h-propositions are equal.
A type has split support if and only if it admits a weakly constant endomap .
Given , the composite is weakly constant. Conversely, if is steady, by the lemma, so splits the support of .
Note that , so that if we start with a weakly constant endomap of , deduce a splitting of the support of , and then reconstruct a weakly constant endomap, we obtain the same map. However, the proof of steadiness is generally different from the one we began with, so this “logical equivalence” is not an equivalence of types.
A type is an h-set if and only if every identity type admits a weakly constant endomap.
We know that is an h-set just when all have split support.
Nicolai Kraus and Martin Escardo and Thierry Coquand and Thorsten Altenkirch, “Generalizations of Hedberg’s theorem”, M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 173-188. Springer, Heidelberg 2013. PDF. In this paper, steady functions are called “constant”.
Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch, Notions of Anonymous Existence in Martin-Löf Type Theory, Logical Methods in Computer Science 13 1 [doi:10.23638/LMCS-13(1:15)2017, arXiv:1610.03346]
Last revised on December 9, 2023 at 02:56:47. See the history of this page for a list of all contributions to it.