It might be of interest to people in here that there is a new chat area for category theory. It's open to all who are interested, but very focused on category theory, and it relies on an app called "Zulip." The link is here: categorytheory.zulipchat.com

@S.carmeli Ok, thanks!!

@JonathanBeardsley It appears one needs an invitation to join this group. Do you know what the criteria/procedures are for obtaining such an invitation?

@Dedalus if $S$ is a quasicategory then $f$ is cocartesian iff it is an initial object in $X_{x/}\times_{S_{p(x)}}\{p(f)\}$, so in that case the answer is yes.

I missed a ‘/‘, but it should be clear

Nevermind, only one side of that implication is valid ( see Rmk 2.4.1.9 in HTT)

Although it seems that if you are over an $\infty$-category and you use the criterion with the Cartesian square at the level of hom $\infty$-groupoids, then even equivalence in $X_{x/}$ suffices.

@EdoardoLanari That was basically my argument as well. The reason I am asking this question is that I saw the exercise in math.univ-paris13.fr/~harpaz/lecture_notes.pdf Exercise 2.6.10 3), pg. 26. The solution I have is using some machinery not developed at this point (quoting non-trivial theorems from HTT) , so I thought maybe some easy solution should be available

@EdoardoLanari But if I understand, this is not "obvious", right?

@AdrianClough From what I can tell, that's not true. There are hundreds of people in there already. However, I also recall getting some kind of message telling me I needed an invitation, and then messing around with it and eventually getting in. I think it's a glitch, but I don't understand the app well enough to tell you exactly what's going on. :-(

@Dedalus by inspecting low dimensional cases I convinced myself that you may not need fibrant base. In fact, suppose $f\simeq f’$, with $f$ being a $p$-Cart 1-simplex. You can use the data of the equivalence to transform any $n$-dimensional outer horn for $f’$ into an $n+1$-dimensional one for $f$, whose solution provides one for the original problem.

But I wouldn’t consider that a simple proof, only elementary. Now I am a bit unsure what Lurie means in 2.4.1.9 in HTT, since I don’t believe that to be an ‘iff’, although then I don’t understand why he does not expand in Prop.2.4.2.4 on the reason why he can complete the proof of $(3) \Rightarrow (1)$

@JonathanBeardsley I am having the same issue as Adrian.

Hm weird....

@MattFeller @AdrianClough one thing I know I can do is send an invite directly to your e-mails, if you want to send me your e-mail addresses in some way

I think another thing that might work is to just create a Zulip account without reference to that particular chatroom, and then use it to log in??

Also, this is the person that created the chat, so it might be worth contacting him directly. I don't think I can be much assistance (also the link is coming from his Twitter account): julesh.com

The link posted here worked for me: twitter.com/_julesh_/status/1242141831057616896

@RuneHaugseng Thanks, that worked!

I had no idea there were that many people doing applied category theory

@JonathanBeardsley Thanks, that worked!

@Dedalus I suppose one could prove it this way: suppose you have this 1-simplex $\alpha$ which witness that $f\simeq f’$, and assume $f’$ i $p$-Cartesian. Then given a lifting problem to check whether $f$ is also $p$-CArtesian, I.e. a commutative square with $p$ on the right and an inclusion $\Lambda^n_n \to Delta^n$, you can extend this (using the 2-simplex corresponding to $\alpha$) to another lifting problem

Which has the inclusion $\Lambda^n_n + \Delta^2 \hookrightarrow \Delta^{n+1}$, where the domain is the gluing of $\Lambda^n_n$ and $\Delta^2$ along, respectively, $[n-1,n]\colon\Delta^1\to \Lambda^n_n$ And $[0,2]\colon \Delta^1 \to \Delta^2$

as the map on the left. You can obtain the bottom horizontal map using a degenerate $n+1$-simplex. Now you simply pullback along this map to obtain a fibrant codomain, then you can use the fact that it is valid in this case.

@AdrianClough that's a neat question, for which i have no intuition. do you have any that you could share? (about hypercompletion and/or about having locally constant shape.)

@AaronMazel-Gee So here is my attempt to prove that such a topos does not exist, which I think pins down where (some of) the difficulties lie: Let $\mathcal{X}$ be a topos in which all hypercomplete objects have constant shape. We then obtain a geometric morphisms $\mathcal{X}^{\wedge} \xrightarrow{\iota} \mathcal{X} \xrightarrow{\pi} \mathcal{S}$. The functor $\sigma := \iota^* \circ \pi^*$ by assumption admits a left adjoint $\sigma_!$.

An obvious guess would be that $\pi_!$ (which a priori lands in pro-spaces) takes a sheaf $F$ in $\mathcal{X}$ to $\sigma_! \circ \iota^*F$, i.e. that the shape of an object does not see the “$\infty$-connected part”. This would follow from $\pi^*$ landing in $\mathcal{X}^{\wedge}$; this seems plausible, as all spaces are hypercomplete. By adjointness, this is equivalent to the assertion that $\pi_*$ carries $\infty$-connected maps to equivalences.

I have not been able to show this, quite possibly because it is false. One could try finding an example of a $\mathcal{X}$ containing an $\infty$-connected sheaf with no global section; as the hypercompletion of any $\infty$-connected a sheaf is the final object.

This might give an indication of why such a topos might exist in the first place.

this example of course was the reason for the nonsense I tried to write before.

oh, sorry, I meant @AdrianClough