@HarryGindi I think it's important to clarify that Gaitsgory and Rozenblyum do define a Gray tensor product, and their various unproved propositions concern this definition. Yuki has proved things about a differently defined Gray tensor product; Dom years ago gave yet another different definition. So until one of these definitions is shown to be equivalent to G&R's definition, we can't really say that G&R's unproved propositions have been proved.

(And of course there remain statements in G&R which have not been proven for any definition.)

@AlexanderCampbell Yeah, that's sort of my point by 'none of them are afaik drop-in theorems'

actually proving all of the stuff in that appendix is the subject of a few papers or a small monograph

@HarryGindi Aye, we are in agreement.

and I mean a few papers or small monograph, taking already as input either Yuki's or Dom's construction of the tensor product

idk it's a bit unfortunate that whoever sits down and does all that work probably won't really ever get cited (one of the reasons why I thought I'd advertise Yuki's paper in here!!)

I'm glad you did! And of course we both know that the value of Yuki's work (and the work of Edoardo & co.) extends far beyond just assisting in cleaning up G&R.

Here's an interesting question that I had the other day

So it's a pretty immediate observation that the lax tensor product and its adjoints cannot be enriched functors

because ⊗ cannot associate with ×

Okay, so what structure do we really have on 2-Cat/(∞,2)-Cat

that we would want to be able to generalize to other '2-categories that behave like 2-Cat'

The Gray tensor product is at least functorial at the level of (∞,1)-categories.

like, you could have a notion of lax,pseudo,and oplax 2-cells

yeah, I know that

But the reason I was thinking about this was something like ∞-cosmoi but ∞,2

I'm not finished ;)

oh, go on

And I expect it to be functorial at the level of (∞,2)-categories if we take icons as 2-cells.

But that's all I had to say, so please go on

Oh, well, I was just thinking if you wanted to sort of build an 'informal language of 2-categories', you need a few inputs, one of them being at least a notion of lax and oplax natural transformation

or sorry, an informal language of 2-Cat

so at some point I came up with this idea that you should have three separate Hom objects, all of which have the same vertices, but where each one gives you like a cotensoring by 2-Cat with each of its exponential structures, if that makes sense

here 2-Cat means ∞,2-Cat

Yep

yeah, I was wondering if this has a name or has been worked out anywhere is all

also, have you thought at all about icons for ∞,2-Cats?

Rune at least has (see his latest preprint).

I don't think this has a name, and I haven't seen it worked out anywhere

The first thing that pops into mind is having an enrichment of the category of 2-categories over "intercategories" (à la Grandis-Paré). But I don't know if that would work out.

I remember seeing the term 'f-category' at one point

but it looked like only half of what I wanted

Yeah so there you have a 2-category-like structure which has two notions of 1-morphism, one contained in the other.

ah, I guess it's not really similar

oh, by the way, with icons, does one expect something like

Roughly speaking, a category enriched over intercategories would have 3 notions of 2-cell, which with any luck would behave like strict, lax, and oplax natural transformations. But you'd have to be very lucky for this to work, I think.

the ∞,n-category of ∞,n-1-categories with 1-cells being functors, 2-cells being icons, 3-cells being modifications of icons, and so on?

Well, one gets an (∞,2)-category of (∞,2)-categories, functors, and icons.

Richard Garner and Nick Gurksi constructed a tricategory of tricategories, where the 2-cells and 3-cells and icon-like.

mhm, I don't really know where to place icons

are they a fundamental notion or a useful one

So extrapolating, maybe one should expect to get an (∞,n)-category of (∞,n)-categories with icon-like things in dimensions 2 and above?

yeah that's what I was thinking

I dunno, it would be interesting to see what an expert has to say about how sort of all of the structure on 2-Cat fits together

If you consider the standard embedding of 2-categories into simplicial objects in Cat to be fundamental, then I guess icons are fundamental.

because there is an absolute ton of structure compared to Cat

that seems like a double notion to me

is that wrong?

Not at all. Between double categories there is the standard notion of natural transformation; if we embed 2-categories into double categories in the easy way, these become icons.

I personally don't see all the baggage carried by 2-Cat as fitting into one cohesive whole.

Haha, me neither

as in, not that I don't want to see it or believe it's impossible, just that I definitely don't see it. =)

The first thing I want to see is an equipment (as in proarrow equipment) of (∞,2)-categories (and of V-enriched ∞-categories more generally). Of course this doesn't capture all the lax business, but it gives a great framework for doing a lot of enriched category theory.

We were discussing this at MSRI before our semester was rudely interrupted.

Keep me updated =)

Thanks everyone for the update on the situation. I guess the "GR saga" continues... And I certainly did not want to imply that $(\infty,2)$-category theory is all about justifying this damned Appendix; clearly it is a fundamental endeavour and it is great to see it progress.

The forgetful functor for algebras over a monad is faithful. Is there an analogous statement in the world of quasicategories?

A useful and easy (imho) analog is that the functor is conservative. I don't know anything about faithfulness so I will let the experts answer :)

yeah... I actually want something rather like faithfulness

not conservativity

in a form as simple as $Uf\simeq Ug$ implies $f\simeq g$ where U denotes the forgetful functor

(Again, it is probably better to wait for experts, but my gut feeling is that this is false in general.)

@BrunoStonek I don't think you can ask too much here. For example, connective spectra are monadic over spaces, but Map(HF_p,HF_p[1]) is disconnected whereas Map(K(F_p,0),K(F_p,1)) is connected.

Or for another example, any element of pi_n S for n>0 gives a map HF_p[n] -> HF_p[0] which is null as spectra but generally not null as modules over the endomorphism spectrum of HF_p.

@WilliamBalderrama: that was very useful. thanks

@S.carmeli Ok, I got it now. Thank you for all your help!