I ended my last post about splitting idempotents with several open questions:
- If we have a map , a witness of idempotency , and a coherence datum , and we use them to split as in the previous post, do the new witnesses induced from the splitting agree with the given ones?
- How many different ways can a given map “be idempotent” — can you give an example of a map that is idempotent in two genuinely different ways, perhaps with non-equivalent splittings?
- Given , can we also split it with ?
- (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 agrees, but the induced 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 can be recovered from the splitting is an easy computation. Given a splitting and such that and , the induced is . For the splitting we constructed with , we have and , so the induced is just the -component of the homotopy at . By construction, this is
where is the given witness of idempotence. But by the given coherence datum , we have , so this reduces to just .
Recovering a retract
Before attacking , let’s consider a dual question: given a retraction , is it equivalent to the splitting of the induced idempotent ?
Actually, before we can even ask that, we have to check that comes with not just but also . The definition of is easy: to get we take . For we have to identify with , which may seem impossible until you think of concatenating them both with , after which the equality becomes just a naturality square.
Now, what happens when we split ? We end up with a new retraction such that (in fact this equality holds judgmentally). The standard argument from 1-category theory gives us an equivalence composed of and , with and dually . Moreover, this equivalence respects the sections and retractions, e.g. we have and .
Finally, to be higher-categorically consistent, we should also check that this equivalence respects the homotopies and ; one sensible way to say this would be that . Both of these are homotopies ; note that in our case the domain is judgmentally equal to . Substituting the definitions of from the previous post (this is one of the places a proof assistant comes in handy), we see that the first one is
while the second one is
Now by naturality, we have . Applying this in the middle of the first composite, and canceling with its inverse on the left, we reduce it to
Now naturality again gives us , so this is equal to
Comparing this to the second composite, we can cancel on the left, reducing the problem to , which is another naturality. Whew!
Let’s step back a moment and think about what we just proved. It turns out that the equivalence together with and our final coherence is exactly what we need to show that as elements of the type of retractions of :
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 and a point . In this case we can make into a path and transport along in the tautological type family , and then transport the result forwards again along . 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 and then applying , and the result is of course equivalent to . But on the other hand, for any type family , we have . These two hands give us two ways of identifying this double transport with ; 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 and then along 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 is itself a retract of the type of partially-coherent idempotents . 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 , the type of splittings of (meaning together with ) is a retract of the type of partial-coherences for , i.e. . Similarly, given and , the type of splittings of respecting (that is, together with ) is a retract of the type of ‘s.
Preservation of J
Now let’s consider the question of preservation of . Since we now know that the type of retracts of is a retract of the type of triples , and we know that we can recover and from the splitting, if we could also recover , then the type of retracts would actually be equivalent to the type of triples .
This seems a bit implausible. To construct an actual counterexample, let’s consider the case , with the obvious proof consisting of reflexivity. Then as above are more or less exactly the data of a type together with a (half-adjoint) equivalence . In particular, the type of such data is (by univalence) a based path-type (a “coconut”), hence contractible. Therefore, if it were equivalent to the type of ‘s, then the latter would also be contractible. So to show that is not generally recoverable, it suffices to exhibit a type such that and admit more than one inequivalent .
Now when and , the type of is . This is what you might call the “2-center” of , so we need a type with a nontrivial inhabitant of this. One such type is ; another is , where . I may have more to say about 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 and a fully-coherent idempotent should have higher coherences at all levels. A precise definition of coherent idempotents in -categories can be found in section 4.4.5 of Higher topos theory. However, by Corollary 184.108.40.206 therein, the space of coherent idempotents (in an -category where all coherent idempotents split) is equivalent to the type of retracts, where “retract” means in our simple 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 : 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 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 — 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 to be the splitting (as constructed in the last post) of the idempotent on the type of ‘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 , it essentially preserves and , but constructs a new 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 (which has many equivalent definitions) that is a retract of a type 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 using half-adjoint equivalences, then the induced idempotent on (adjointification) preserves the quasi-inverse function and one of the homotopies, while modifying the other one. (There is a difference, of course, in that 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?