Splitting Idempotents, II

I ended my last post about splitting idempotents with several open questions:

If we have a map $f:X\to X$ , a witness of idempotency $I:f\circ f = f$ , and a coherence datum $J: \prod_{x:X} \mathsf{ap}_f(I(x)) = I(f(x))$ , and we use them to split $f$ as in the previous post, do the new witnesses $I,J$ induced from the splitting agree with the given ones?
How many different ways can a given map $f$ “be idempotent” — can you give an example of a map that is idempotent in two genuinely different ways, perhaps with non-equivalent splittings?
Given $f,I,J$ , can we also split it with $A = \sum_{x:X} \sum_{p:f(x)=x} (\mathrm{ap}_f(p)=I(x))$ ?
(I didn’t ask this one explicitly, but I should have) Can we define the type of fully-coherent idempotents in HoTT?

The third question was answered negatively by Nicolai. The second one is, in my opinion, still open. In this post, I’ll answer the first and fourth questions. The answers are (1) the induced $I$ agrees, but the induced $J$ does not in general, and (4) Yes — by splitting an idempotent! They have also been formalized; see the pull request here.

Preservation of I

The proof that $I$ can be recovered from the splitting is an easy computation. Given a splitting $s:A\to X$ and $r:X\to A$ such that $H : r\circ s = 1$ and $s\circ r = f$ , the induced $I$ is $x\mapsto \mathsf{ap}_s (H(r(x)))$ . For the splitting we constructed with $A = \sum_{a:\mathbb{N}\to X} \prod_{x:X} f(a_{n+1})=a_n$ , we have $r(x) = (\lambda n. f(x), \lambda n.I(x))$ and $s(a,b) = a_0$ , so the induced $I'(x)$ is just the $0$ -component of the homotopy $H:r\circ s = 1$ at $r(x)$ . By construction, this is

$f(f(x)) \xrightarrow{\mathsf{ap}_f(I(x))^{-1}} f(f(f(x))) \xrightarrow{I(f(x))} f(f(x)) \xrightarrow{I(x)} f(x).$

where $I$ is the given witness of idempotence. But by the given coherence datum $J$ , we have $\mathsf{ap}_f(I(x)) = I(f(x))$ , so this reduces to just $I(x)$ .

Recovering a retract

Before attacking $J$ , let’s consider a dual question: given a retraction $(A, r:X\to A, s:A\to X, H:r\circ s = 1)$ , is it equivalent to the splitting of the induced idempotent $s r : X \to X$ ?

Actually, before we can even ask that, we have to check that $s r$ comes with not just $I$ but also $J$ . The definition of $I$ is easy: to get $s r s r = 1$ we take $x\mapsto \mathsf{ap}_s (H(r(x)))$ . For $J$ we have to identify $x\mapsto \mathsf{ap}_{srs} (H(r(x))) : srsrsrx = srsrx$ with $x\mapsto \mathsf{ap}_s (H(rsrx)) : srsrsrx = srsrx$ , which may seem impossible until you think of concatenating them both with $\mathsf{ap}_s (H(r(x))) : srsrx = srx$ , after which the equality becomes just a naturality square.

Now, what happens when we split $s r$ ? We end up with a new retraction $(A',r',s',H')$ such that $s r = s' r'$ (in fact this equality holds judgmentally). The standard argument from 1-category theory gives us an equivalence $A\simeq A'$ composed of $g = r' s : A \to A'$ and $h = r s' : A' \to A$ , with $\eta : g h = r' s r s' = r' s' r' s' = 1 1 = 1$ and dually $\epsilon : h g = r s' r' s = r s r s = 1 1 = 1$ . Moreover, this equivalence respects the sections and retractions, e.g. we have $P : h r' = r s' r' = r s r = r$ and $Q : s' g = s' r' s = s r s = s$ .

Finally, to be higher-categorically consistent, we should also check that this equivalence respects the homotopies $H$ and $H'$ ; one sensible way to say this would be that $\mathsf{ap}_h (H'(ga)) \cdot \epsilon_a = P(s' g a) \cdot \mathsf{ap}_r(Q a) \cdot H(a)$ . Both of these are homotopies $r s' r' s' r' s = 1$ ; note that in our case the domain is judgmentally equal to $rsrsrs$ . Substituting the definitions of $r',s',H'$ from the previous post (this is one of the places a proof assistant comes in handy), we see that the first one is

$rsrsrsa \xrightarrow{\mathsf{ap}_{rsrs}(H(rsa))^{-1}} rsrsrsrsa \xrightarrow{\mathsf{ap}_{rs}(H(rsrsa))} rsrsrsa \xrightarrow{\mathsf{ap}_{rs}(H(rsa))} rsrsa \xrightarrow{H(rsa)} rsa \xrightarrow{Ha} a$

while the second one is

$rsrsrsa \xrightarrow{H(rsrsa)} rsrsa \xrightarrow{\mathsf{ap}_{rs}(Ha)} rsa \xrightarrow{Ha} a.$

Now by naturality, we have ${\mathsf{ap}_{rs}(H(rsrsa))} \cdot {\mathsf{ap}_{rs}(H(rsa))} = {\mathsf{ap}_{rsrs}(H(rsa))} \cdot {\mathsf{ap}_{rs}(H(rsa))}$ . Applying this in the middle of the first composite, and canceling ${\mathsf{ap}_{rsrs}(H(rsa))}$ with its inverse on the left, we reduce it to

$rsrsrsa \xrightarrow{\mathsf{ap}_{rs}(H(rsa))} rsrsa \xrightarrow{H(rsa)} rsa \xrightarrow{Ha} a.$

Now naturality again gives us ${\mathsf{ap}_{rs}(H(rsa))} \cdot {H(rsa)} = H(rsrsa) \cdot {H(rsa)}$ , so this is equal to

$rsrsrsa \xrightarrow{H(rsrsa)} rsrsa \xrightarrow{H(rsa)} rsa \xrightarrow{Ha} a.$

Comparing this to the second composite, we can cancel $H(rsrsa)$ on the left, reducing the problem to ${\mathsf{ap}_{rs}(Ha)}\cdot Ha = {H(rsa)} \cdot Ha$ , which is another naturality. Whew!

Let’s step back a moment and think about what we just proved. It turns out that the equivalence $A\simeq A'$ together with $P,Q$ and our final coherence is exactly what we need to show that $(A,r,s,H) = (A,r',s',H')$ as elements of the type of retractions of $X$ :

$\sum_{(A:\mathsf{Type})} \sum_{(r:X\to A)} \sum_{{s:A\to X}} (r\circ s = 1).$

This claim is one of those things that I think seems fairly intuitively obvious (at least, once you’ve fully internalized Chapter 2 of the Book), but is surprisingly difficult to convince a proof assistant of. (There’s another such “doozy” in the Book itself, in the proof of Theorem 7.6.6.)

In this case the crucial fact turns out to be a coherence law that I’m currently calling transport_path_universe_pV. It applies when we have an equivalence $f : A\simeq B$ and a point $b:B$ . In this case we can make $f$ into a path $\mathsf{ua}(f):A=B$ and transport $b$ along $\mathsf{ua}(f)^{-1}$ in the tautological type family $X\mapsto X$ , and then transport the result forwards again along $\mathsf{ua}(f)$ . On one hand, by the “computation rule for univalence” (third bullet following remark 2.10.4 in the book), these two operations are equivalent respectively to applying $f^{-1}$ and then applying $f$ , and the result $f(f^{-1}(b))$ is of course equivalent to $b$ . But on the other hand, for any type family $Z:Y\to \mathsf{Type}$ , we have $\mathsf{transport}^Z(p,\mathsf{transport}^Z(p^{-1},z)) = z$ . These two hands give us two ways of identifying this double transport with $b$ ; the lemma transport_path_universe_pV says that they are equal.

It didn’t take me all that long to notice and prove this lemma in this case, but that was only because I had already noticed and proven the dual version transport_path_universe_Vp, for transporting along $\mathsf{ua}(f)$ and then along $\mathsf{ua}(f)^{-1}$ in the other order, when formalizing Theorem 7.6.6. In that case it took me quite a while to isolate this transport coherence law as the crucial thing I needed.

Anyway, once we make it through that proof, we see that what we’ve shown is that the type of retracts of $X$ is itself a retract of the type of partially-coherent idempotents $\sum_{(f:X\to X)} \sum_{(I:f\circ f = f)} (\mathsf{ap}_f(I) = I\circ f)$ . The section constructs the idempotent induced by a retract, while the retraction is the splitting construction from the last post.

With a bit more work, we can deduce from this that for any fixed $f$ , the type of splittings of $f$ (meaning $(A,r,s,H)$ together with $K:s\circ r = f$ ) is a retract of the type of partial-coherences for $f$ , i.e. $\sum_{(I:f\circ f = f)} (\mathsf{ap}_f(I) = I\circ f)$ . Similarly, given $f$ and $I$ , the type of splittings of $f$ respecting $I$ (that is, $(A,r,s,H,K)$ together with $L: \mathsf{ap}_s(H\circ r) = I$ ) is a retract of the type $\mathsf{ap}_f(I) = I\circ f$ of $J$ ‘s.

Preservation of J

Now let’s consider the question of preservation of $J$ . Since we now know that the type of retracts $(A,r,s,H)$ of $X$ is a retract of the type of triples $(f,I,J)$ , and we know that we can recover $f$ and $I$ from the splitting, if we could also recover $J$ , then the type of retracts $(A,r,s,H)$ would actually be equivalent to the type of triples $(f,I,J)$ .

This seems a bit implausible. To construct an actual counterexample, let’s consider the case $f=\mathsf{id}_X$ , with $I=\mathsf{refl}$ the obvious proof consisting of reflexivity. Then $(A,r,s,H,K,L)$ as above are more or less exactly the data of a type $A$ together with a (half-adjoint) equivalence $A\simeq X$ . In particular, the type of such data is (by univalence) a based path-type $\sum_{A:\mathsf{Type}}(A=X)$ (a “coconut”), hence contractible. Therefore, if it were equivalent to the type of $J$ ‘s, then the latter would also be contractible. So to show that $J$ is not generally recoverable, it suffices to exhibit a type $X$ such that $f=\mathsf{id}_X$ and $I=\mathsf{refl}$ admit more than one inequivalent $J$ .

Now when $f=\mathsf{id}_X$ and $I=\mathsf{refl}$ , the type of $J$ is $\prod_{x:X} \mathsf{refl}_x = \mathsf{refl}_x$ . This is what you might call the “2-center” of $X$ , so we need a type with a nontrivial inhabitant of this. One such type is $S^2$ ; another is $B\mathsf{Aut}(B\mathsf{Aut}(\mathbf{2}))$ , where $B\mathsf{Aut}(Y) = \sum_{(Z:\mathsf{Type})} \Vert Y=Z\Vert$ . I may have more to say about $B\mathsf{Aut}$ in another post.

Defining Coherent Idempotents

To conclude, let’s consider whether we can define the type of “fully-coherent idempotents”. What is that? Well, intuitively, in addition to $I$ and $J$ a fully-coherent idempotent should have higher coherences at all levels. A precise definition of coherent idempotents in $(\infty,1)$ -categories can be found in section 4.4.5 of Higher topos theory. However, by Corollary 4.4.5.14 therein, the space of coherent idempotents (in an $(\infty,1)$ -category where all coherent idempotents split) is equivalent to the type of retracts, where “retract” means in our simple $(A,r,s,H)$ sense (although there is also a notion of “fully coherent retract” that mediates between the two).

Thus, if we’re willing to believe that result, we already have the type of fully-coherent idempotents on $X$ : it’s just the type of retracts defined above. However, there’s something unsatisfying about defining an “idempotent” to be already equipped with its splitting! Moreover, this definition does have one concrete drawback: since it includes the type $A$ as data, it raises the universe level.

We can avoid both of those problems by recalling that we showed the type of retracts to be a retract of the type of partially-coherent idempotents $(f,I,J)$ — and we also showed that any retract is equivalent to the canonical splitting of its induced idempotent! Thus, we can define the type of coherent idempotents on $X$ to be the splitting (as constructed in the last post) of the idempotent on the type of $(f,I,J)$ ‘s induced by the splitting construction. I find this very cute, and also a nice example of applying a theorem at two different universe levels.

This motivates me to wonder what this idempotent actually behaves like: given $f,I,J$ , it essentially preserves $f$ and $I$ , but constructs a new $J$ out of the old one. In principle, this construction could be done without going through the splitting, and in fact you can ask Coq what it looks like and Coq will compute it for you. But what comes out is quite large and I haven’t been able to make any headway understanding it on its own.

Let me end by emphasizing an analogy with equivalences. In that case we also have a “fully coherent” notion $\mathsf{IsEquiv}(f)$ (which has many equivalent definitions) that is a retract of a type $\mathsf{QInv}(f)$ of “partially coherent” objects. Thus, in practice it suffices to construct partially-coherent objects (and we generally do), relying on the retraction to convert them into coherent ones. Moreover, the behavior of the retraction is similar: if we define $\mathsf{IsEquiv}(f)$ using half-adjoint equivalences, then the induced idempotent on $\mathsf{QInv}(f)$ (adjointification) preserves the quasi-inverse function and one of the homotopies, while modifying the other one. (There is a difference, of course, in that $\mathsf{IsEquiv}(f)$ is an hprop, whereas the type of coherent idempotents is (probably) not.)

Are there any other structures that behave like this? Are there any other “fully coherent” gadgets that we can obtain by splitting an idempotent on a type of partially-coherent ones?