nLab steady function

Steady functions

Steady functions


A steady function is one 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 word “steady” was suggested by Andrej Bauer.)


In homotopy type theory, a function f:ABf:A\to B is steady if we have a term of type

(x,y:A)(fx=fy). \prod_{(x,y:A)} (f x = f y).

By regarding homotopy type theory as the internal logic of an (∞,1)-topos, we obtain a definition that makes sense in any higher category with binary products: a morphism f:ABf:A\to B is steady if the two composites A×AAfBA\times A \rightrightarrows A \xrightarrow{f} B are equivalent.

Relationship to constancy

If ff is constant in the sense that it factors through the terminal object (i.e. we have f=λ = \lambda x. b for some b:Bb:B), then ff is obviously steady. The converse holds if we know that the domain AA is inhabited, for if a 0:Aa_0:A, then fa=fa 0f a = f a_0 for all a:Aa:A. However, the identity function of the empty type is steady, yet not equal to λx.b\lambda x.b for any b:b:\emptyset (since no such bb exists).

More generally, if ff factors through the propositional truncation A{\|A\|}, then it is steady, since any two elements of A{\|A\|} are equal (i.e. it is an h-proposition). In fact, this is true if ff factors through any h-proposition (in which case it in fact also factors through A{\|A\|}, by the universal property of the latter).

The converse to this last implication does hold for some specific f:ABf:A\to B, such as:

  • If BB is an h-set. For then ff factors through the 0-truncation A 0{\|A\|_0}, and the set-coequalizer of the two projections A 0×A 0A 0{\|A\|_0} \times {\|A\|_0} \to {\|A\|_0} is the propositional truncation.

  • If AA has split support. For then we have a composite AAfB{\|A\|} \to A \xrightarrow{f} B, whose restriction to AA is equal to ff by steadiness.

  • If A=P+QA=P+Q, with PP and QQ h-propositions. For then A{\|A\|} is the join P*QP*Q of PP and QQ, i.e. the pushout of the two projections PP×QQP \leftarrow P\times Q \to Q. The universal property of this pushout says exactly that any steady map P+QBP+Q\to B factors through P*Q=P+QP*Q = \Vert P+Q\Vert.

  • If A=BA=B (see below).

However, it can fail in general, even when AA is merely inhabited (i.e. A=1{\|A\|}= 1). For instance, let A=P+Q+RA=P+Q+R for h-propositions PP, QQ, and RR, and let BB be the triple pushout of PP, QQ, and RR under P×QP\times Q, P×RP\times R, and Q×RQ\times R. Then there is a steady map f:ABf:A\to B, but there exist models in which A=1{\|A\|} = 1 but BB has no global element]. The most straightforward such model is [[presheaves? on the poset of proper subsets of {a,b,c}\{a,b,c\}, with P={a,b}P=\{a,b\}, Q={b,c}Q=\{b,c\}, and R={a,c}R=\{a,c\}. In this model, we have B(S)=1B(S) = 1 for all nonempty proper subsets SS, while B()=S 1B(\emptyset) = S^1, and BB has no global sections.

See this discussion.

In general, being steady may be regarded as an “incoherent approximation” to constancy in the sense of factoring through an h-proposition. Indeed for a set AA, its propositional truncation is the set-coequalizer of A×AAA\times A\rightrightarrows A. However, in general such a construction requires the realization of a whole simplicial diagram (the simplicial kernel of the map A1A\to 1).

Steady endomaps

While an arbitrary steady function is not very coherent, a steady endofunction f:AAf:A\to A has some extra degree of “coherence”, as witnessed by the following results of (KECA).


If f:AAf:A\to A is steady, then the type Fix(f) x:A(fx=x)Fix(f) \coloneqq \sum_{x:A} (f x = x) is an h-proposition, and equivalent to A{\|A\|}.


Suppose H: (x,y:A)(fx=fy)H: \prod_{(x,y:A)} (f x = f y), and let (a,p),(b,q):Fix(f)(a,p),(b,q):Fix(f); we want to show (a,p)=(b,q)(a,p)=(b,q). Let r:a=br:a=b be the concatenated path

ap 1faH a,a 1faH a,bfbqb. a \xrightarrow{p^{-1}} f a \xrightarrow{H_{a,a}^{-1}} f a \xrightarrow{H_{a,b}} f b \xrightarrow{q} b.

It will suffice to show that pr=ap f(r)qp \bullet r = ap_f(r) \bullet q, where ap fap_f denotes the action of ff on paths. However, the dependent action of HH on paths implies that H x,yap f(s)=H x,yH_{x,y} \bullet ap_f(s) = H_{x,y'} for any x:Ax:A and any s:y=ys:y=y', and in particular ap f(r)=H a,a 1H a,bap_f(r) = H_{a,a}^{-1} \bullet H_{a,b}. From this pr=ap f(r)qp \bullet r = ap_f(r) \bullet q is immediate. Thus, Fix(f)Fix(f) is an h-proposition.

Now we have a map g:AFix(f)g:A\to Fix(f) defined by g(x)(fx,H fx,x)g(x) \coloneqq (f x, H_{f x,x}), so by the universal property of A{\|A\|}, we have AFix(f){\|A\|} \to Fix(f). On the other hand, we have the first projection pr 1:Fix(f)Apr_1:Fix(f) \to A, and hence Fix(f)AFix(f) \to {\|A\|}. Thus, these two h-propositions are equal.


A type AA has split support if and only if it admits a steady endomap f:AAf:A\to A.


Given AA{\|A\|} \to A, the composite AAAA\to {\|A\|} \to \A is steady. Conversely, if ff is steady, Fix(f)=AFix(f) = {\|A\|} by the lemma, so pr 1:Fix(f)Apr_1:Fix(f) \to A splits the support of AA.

Note that pr 1g=fpr_1 \circ g = f, so that if we start with a steady endomap of AA, deduce a splitting of the support of AA, and then reconstruct a steady 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 AA is an h-set if and only if every identity type x= Ayx=_A y admits a steady endomap.


We know that AA is an h-set just when all x= Ayx=_A y have split support.


Last revised on October 12, 2013 at 20:54:29. See the history of this page for a list of all contributions to it.