12:54 AM
The cech complex of a map A -> B is contractible as soon as the map has a section...

1 hour later…
1:59 AM
I don't understand this simplicial set $\mathcal B$ (as Saal is calling it) or $\mathcal Q$ (as Nguyen calls it). The simplicial operators are supposed to be defined by making some choices of pullback squares. But Nguyen never says anything about how to ensure these choices are strictly functorial...
I also wonder how it relates to the model of $Cat_\infty$ in Ayala-Francis-Tanaka
That is, the set of $n$-simplices of $\mathcal Q$ is supposed to be the set of small simplicial sets $X$ equipped with a cocartesian fibration $X \to \Delta[n]$. Then the face maps are defined by pullback. But how does one make these pullbacks into an actual, strict functor $\Delta^{op} \to Set$?
Okay, I guess I can see how for face maps, there is a canonical choice of pullback, given by literally taking the subset of $X$ which lies over the inclusion of $\Delta[n-1]$
And this is strictly functorial.
Do degeneracies have something similar you can do?

In Definition 5.2.3 of his new book, Cisinski defines an $n$-simplex of an analogous simplicial set $\mathscr{S}$ to be a left fibration over $\Delta[n]$ together with a choice of pullback of it along each morphism in $\Delta$.
Presumably one must do the same to define this simplicial set $\mathscr{Q}$.

Interesting. I'm having trouble interpreting the definition given in 3.4 of Nguyen's thesis as doing something similar. But maybe that's what's intended
I suppose this does indeed work, even if it's a little bit cumbersome

2:19 AM
Do you mean Cisinski's definition?

yeah

What is the model of $Cat_{\infty}$ in Ayala--Francis--Tanaka?

Well, it's jazzed up a bit
They have a model of $Cat_\infty$ where an $\infty$-category is a certain kind of fibration over a category of stratified spaces
I think I'm free-associating too much, though
Because really what it comes down to for them is that among the stratified spaces are certain simplices, and you extract a complete Segal space by restricting to these
and that's one direction of the equivalence
So maybe what I really want to say is that $\mathcal Q$ seems to be most naturally defined as a complete Segal space rather than a quasicategory?

Presumably one would still have to do some kind of strictification as in Cisinski's definition to get a bisimplicial set?

2:27 AM
I'm imagining that Q will be the "0th row" of this complete Segal space.

One model for $Cat_\infty$ is that an $\infty$-category is a quasicategory equipped with a cocartesian fibration over $\Delta^{op}$ satisfying the complete Segal conditions. I guess that's the kind of thing I'm imagining that $Q$ exists most naturally as.

Ah, I see.

But maybe you lose all the benefits by working with such a baroque model :)

Perhaps. A useful model-specific corollary of the result that $\mathscr{S}$ is a quasi-category is that left fibrations "tightly extend" along trivial cofibrations in the Joyal model structure.

Is $\mathcal S$ the same as $Q$?

2:33 AM
(Meaning that for any Joyal trivial cofibration u : A --> B and any left fibration p : X --> A, there exists a left fibration q : Y --> B such that p is the pullback of q along u.)

Oh -- $S$ is to left fibrations as $Q$ is to cocartesian fibrations
Yeah, that's a pretty interesting fact

Right. (That result is Cor 5.2.11 in Cisinski's book.)
Cisinski uses that it in the proof of the important theorem that, for any weak categorical equivalence f : A --> B, the adjunction (f_!,f^*) is a Quillen equivalence between the covariant model structures on sSet/A and sSet/B.

Is that without fibrancy hypotheses on $A$ and $B$?

That's right.

pretty neat!
There are places in Lurie where he talks about fibrations over simplicial sets which are not quasicategories and I always wondered whether this is for added generality, or for convenience.
I suppose this means that it's the latter

2:41 AM
What sort of convenience do you mean?

Just that if you want to think about fibrations over some $\infty$-category, you're free to work with a non-fibrant model. Like for example if you want to think about sequences $C_0 \to C_1 \to \dots$ in $Cat_\infty$, you could model this with cocartesian fibrations over the 1-skeleton of the ordinal $\omega$, which might be easier to think about than cocartesian fibrations over $\omega$ itself.

Right, I get you, I agree.

4 hours later…
6:39 AM
I thought you could define degeneracies for Q by doing certain pushouts (which kind of already come with a strictly functorial model in Set and hence in Simplicial sets). For instance if $X \to \Delta^1$ is a cocartesian fibration one can define one of the degeneracies of it to be the pushout $(X \coprod_{X_{0}} X) \coprod_{X_{1} \corpod X_{1}} X_{1} \times \Delta^1$.
I imagined there's something similar one can do in the general case..
Oh in my definition there's a missing 2-simplex as well. It can also be glued canonically though I think

7:19 AM
I can't find any mention of degeneracies around the definition of $Q$ in Nyugen's Thesis. I wonder what they are in his case.

My understanding is that the definition of Q should read that an n-simplex is a cocartesian fibration over Delta[n] together with a choice of pullback along each map Delta[m] --> Delta[n] (as in the definition of Cisinski I cited above). The face and degeneracy operations of Q are defined by these chosen pullbacks.

hmmm so these choices are only for defining the degeneracies?
Isn't it awkward to choose this arbitrarily
I guess it gives the benifit that the statement is stronger.

The benefit is that it defines a simplicial set.

For a semi-simplicial set you don't need to choose anything though. Isn't that right?
You cna define faces by just doing pullbacks.

I suppose so.

7:33 AM
@SaalHardali Why are faces and degeneracies different here?
I thought that the problem is that the pullbacks were not defined on the nose, but only up to (a unique) isomorphism of simplicial sets

Could you just define the degeneracies by the following: For $X \to \Delta^n$ a cocartesian fibration we have $n$ degeneracies given by pulling back $X\times \Delta^1$ along the $n$ different nndegenerate n-simplices of $\Delta^n \times \Delta^1$ which are non constant in the $\Delta^1$ direction.

My favourite solution to this problem would be to apply the 1-categorical straightening/unstraightening, but of course this is not that different from the more explicit approach in Nyugen's thesis

But pullbacks in Set are strictly functorial.
The same is true for Simplicial Sets.
And canonically so.

@SaalHardali They aren't, that's the whole point.

@SaalHardali I thought that the canonical bijection A×(B×C)\cong (A×B)×C in sets was not literally the identity arrow of some object, which is what you seem to be claiming

7:38 AM
Sorry you are completely correct. I hd in mind the case of pullback along monomorphisms
But maybe these fail to be functorial for exactly the same reason I'm not seeing.

Even for monomorphisms, technically you need to identify two different forms of ordered triples with a canonical bijection which is not the identity
Ofc in some sense it is a dumb problem with standard solutions, but it is a problem

Without making choices of pullbacks beforehand, one ends up with some kind of pseudofunctor (to Cat, say). But, as Denis mentions, one can strictify such pseudofunctors; making choices of pullbacks is more or less like taking the "right adjoint" strictification of this pseudofunctor.

I see. I did miss this detail. Thak you for pointing that out.
@DenisNardin Why is that similar to Nyugen's thesis. I guess I don't seem to understand this arbitrary choice of pullback squares. How does it help with defining the degeneracies?
I guess I'm having trouble with the quantifiers in his definition.

@SaalHardali In the straightening/unstraightening perspective, if you have a Grothendieck fibration $E→B$, instead of choosing a point in the fiber E_b for every b, you are choosing a cartesian lift of the map B_{/b}→B
(here B=Δ)
This makes it functorial, since if you have an arrow b'→b you can send it to the map sending a cartesian lift B_{/b}→E to the composite B_{/b'}→B_{/b}→E

@SaalHardali I don't think the definition in Nguyen's thesis is quite correct (as it is written there, an n-simplex is just a cocartesian fibration over Delta[n]). It's better to follow Cisinski's definition, as I described above (where an n-simplex is a cocartesian over Delta[n] with chosen pullbacks).

7:52 AM
(disclaimer: this works fine since we're working in 1-categories and we have a canonical choice of functor B_{/b'}→B_{/b}, making this work for higher categories is more complicated and it's very close to just proving the S/U theorem)

@AlexanderCampbell Aha, so that simplicial set is quite a lot bigger.
Interesting.
Let me ask again about the functoriality issue. Sorry if I'm being dense. In the case of monomorphisms isn't the set theoretic inverse image a strictly functorial pullback (for monomorphisms).
I'm talking about the case of taking pullbacks w.r.t. a fixed morphism.

At some point you'll have to tell me your precise definition of pullback, since we're arguing set-theoretic technicalities here
Because the functor I am thinking of is not strict
(also, I've got to go now, so sorry to leave in the middle of the conversation)

@DenisNardin np. I think it's better I sit down with pen and paper to figure out exactly what my brain is having trouble with...

9 hours later…
4:55 PM
Older versions of Cisinski's book did define the quasicategory S of spaces via 1-categorical straightening/unstraightening, i.e. defining S_n to be the set of presheaves on the slice Δ/[n] that unstraighten to left fibrations over Δ^n.
This definition feels more elegant, so I'm surprised it changed.

5:47 PM
Oh wow -- that does seem elegant! I do have an old version of Cisinski's book, but I think it's too old -- I can't find this stuff at all! So to spell it out for myself: we define $U$ to be the simplicial set $[n] \mapsto Psh(\Delta/[n])$. There's a standard equivalence (what is it called?) $Psh(C)/y(c) \simeq Psh(C/c)$ where $y$ is Yoneda, so this is equivalent to what we want.
But $[n] \mapsto \Delta/[n]$ and $C \mapsto Psh(C)$ are strictly functorial -- the former covariant and the latter contravariant. So we get a bona fide functor $U: \Delta^{op} \to Set$.
Then $S$ and $Q$ are defined as certain sub-simplicial sets of $U$.
This gives us the codomain of the universal fibration. Does something along these lines also work to construct the domains $U_\bullet, S_\bullet Q_\bullet$?
I suppose there's a canonical terminal object in any presheaf category -- the presheaf which is literally constant at the set $\{\emptyset\}$ or something.
And this is preserved by the reindexing.
So you can define $U_\bullet([n])$ to be the set of presheaves on $\Delta/[n]$ equipped with a map from this copy of the terminal object.
Or maybe the choice of terminal object isn't important
You simply let $U_\bullet([n])$ be the set of presheafs on $\Delta/[n]$ equipped with a chosen element.

Or equivalently, U_•([n]) to be the set of presheaves of pointed sets on Δ/[n].

6:07 PM
nice
This stuff reminds me of things I've vaguely heard about modeling univalence in homotopy type theory
strictification problems
and in particular, universal fibrations
i wonder if understanding the universal (co)cartesian fibration might shed light on what directed type theory should be

1 hour later…
7:35 PM
@TimCampion I'm confused about the degenracies. Seems like the degeneracies for $U$ are just postcomposition with the coface maps. Unfortunatelt this doesn't really correspond to what degeneracies in the quasi category of quasi categories should be, that is insertions of the identity functor. Here's what I believe to possibly be the quasi-category of quasi categories (I'm not sure if this is what's done in Nyugen's thesis because I 'm having trouble parsing some of the definitions.
So $Q_n$ could be the set of small cocartesian fibrations over $\Delta^n$
The faces can be define by doing 1-straightning to the pullbacks.
The degeneracies from n-simplices to n+1 simplices are defined by taking a cocartesian fibration over $\Delta^n$ and multiplying it by $\Delta^1$ and restricting to a nondegenerate $n+1$-simplices in the base $\Delta^n \times \Delta^1$ of which there are exactly n+1.
I have checked that this is a simplicial category. And for low values I have checked that the degeneracies do correspond via straightning to what we think of as inserting the identity functor.
I would love to know if this simplicial set is a quasi-category.
On the other hand maybe this is actually equivalent to the thing with the $U$ and I just failed to compile the definition correctly...
*"I have checked tha this is a simplicial set"

7:58 PM
@SaalHardali Why cannot you take as degeneracies simply the pullback along the degeneracy maps?

8:11 PM
@SaalHardali Say I start with $p: X \to \Delta[n]$ in $Q_n$ under your definition. Then $s_i^\ast(d_i^\ast(p))$ is a certain simplicial subset of $d_i^\ast(p) \times \Delta[1]$. By the simplicial identities, this should be equal to $p$. I have trouble believing this, assuming you're using Kuratowski ordered pairs say for your cartesian products.
The thing I said about face maps being easier than degeneracies is irrelevant in either of Cisinski's approaches which we've been discussing.
Er -- my wording was imprecise. I meant to say that $s_i^\ast(d_i^\ast(p))$ is a certain simplicial subset of $d_i^\ast(p) \times \Delta[1]$ equipped with a certain map to $\Delta[n]$, which should be equal to $X$ equipped with the map $p$ to $\Delta[n]$. Its the equality of the domain sets which I find fishy.

@DenisNardin Actually think you get the same thing upto changing the strictification of the relevant pseudo-functors.
So I guess you don't gain a lot...

Well, "just pullbacks" gains in simplicity for me but YMMV :)

I think I prefer the pullbacks too. I wasn't sure it was the same up until this moment.
The definition with the multiplication has some sort of intuitive meaning...
I mean it's helpful for clarifying why cocartesian fibrations are the same as coherent functors.
Because the case of $\Delta^1$ is easy to do by hand and then you can bottstrap in some sense.
(What I mean is that it helped me understand why the degeneracies are the same as identirt insertions...)
@TimCampion Is what you are having trouble with the fact that the pullbacks are not functorial? In that case I agree that strictification issues arise in the degeneracies as well as in the faces.
What is not clear to me is how either of these definitions (my definition, or the cisinski one which you mention with the neat trick of 1-categorical straightning) have to do with the definition which was proved is a quasi-category.
I belive making precise either my definition or the definition you mention of Cisinski will give isomorphic simplicial set. If this simplicial set is a quasi-category equivalent to one of the other "aproved" models for the infinity category of infinity categories I can die a happy man.