updated link to point to my paper in addition to blog post

]]>Updated idempotent complete (infinity,1)-category with the new, simpler definitions (and updated page references).

]]>Apparently the answer to the question asked (over 7 years ago) in #3 above is “if it isn’t, it should have been”. Lurie has now changed the definition of $Idem$ to be the nerve of the free category containing an idempotent; see here and here. We should update the definition on the lab.

]]>I have added pointer to Mike’s HoTT wrapup here

]]>Awesome, together those answer the question completely, thanks! I’ve recorded these facts on the page.

]]>cf. also Warning 1.2.4.8 for a counterexample if we try to weaken this criterion. (though there are no counterexamples if C is stable.)

]]>Suppose I have an $(\infty,1)$-category $C$ and an idempotent in its homotopy 1-category. Can it be lifted to a “coherent” idempotent in $C$ itself? Is there an obstruction theory?

]]>Lurie defines a simplicial set $Idem$ such that an idempotent in an $(\infty,1)$-category $C$ is the same as a functor $Idem\to C$. Is this $Idem$ the same as the nerve of the free 1-category containing an idempotent?

]]>Sorry for the typo, I was originally planning to say the thing in two steps, but then decided it is better to just quote the reference and the phrase was left...

]]>At first Zoran's reply to my query at structured (infinity,1)-topos sounded as though he were saying "being idempotent-complete" were a structure on an (oo,1)-category rather than just a property of it. That had me worried for a while. It looks, though, like what he meant is that "being idempotent" is structure rather than a property, and that makes perfect sense. So I created idempotent complete (infinity,1)-category.

]]>