Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
But that result is restricting to "small" objects; roughly, it's like only having a categorical Künneth formula for $\mathrm{Perf}$ as opposed to $D_{\mathrm{qc}}$.
That is a nice paper, but it does not really show the right version of the categorical Künneth formula; it gives a fully faithful functor. And I think the case of rigid cohomology is "new", although the translation from the usual picture is rather straightforward.
Definition 0 is a bit ambiguous -- it depends on whether you defined Gpd in the weak or strong sense (i.e. as 2-category or as a 1-category). The strong sense is equivalent to Definition 1. And the relation between weak and strict versions is as usual: There is a natural functor from the strong version to the weak version, and it universally "inverts weak equivalences". (All of this holds in any topos.)
My gut feeling is that you don't actually want to consider this tensor product. I don't know what your motivation is, so it's hard to say, but if I would run into this tensor product, I'd try to see if I can either replace $\breve{\mathbb Q}_p$ by its uncompleted version, or the tensor product by its completion.
Q0: yes, Q1: yes. I disagree however with the premise of Q2. From what I understand, much of Connes' motivation is to do geometry with "wild" quotient spaces. But many of the "wild" quotient spaces he cared about make sense as condensed sets (or maybe condensed groupoids). Also note that the gluing axiom does not even translate to the noncommutative case, as you can't form a $C^*$-algebra $B\otimes_A B$.
The problem from the cited question disappears because I've renamed $f^!$ and $f_\ast$ into $f^\ast$ and $f_!$, and their right adjoint do exist (as well as internal Hom), so you get a 6-functor formalism. (It doesn't "feel" like one, but we have a definition, and it fits the bill!) It's just that the functors don't quite mean what you'd think they mean. But they do once you pass to opposite categories. (But then it's just a 3-functor formalism as the required right adjoints cease to exist; also, your categories are no longer presentable.)
@Gabriel As I say towards the end, if you take the $\mathrm{Pro}$-perspective (and restrict to coherent $D$-modules), you get the standard $\otimes,f^\ast,f_!$ functors. You can then further restrict to holonomic $D$-modules, and then some hard theorems tell you that this category is stable under all six operations. But for the construction of the functors, you don't need the theorems.
Maybe it's better to continue further discussion by e-mail, but a quick answer: This minimal collection certainly contains everything like $n$-Artin stacks, but is even wider, as instead of quotients by smooth equivalence relations, you can also (for example) take quotients by proper equivalence relations. I don't think it's possible to describe explicitly. (Fun example: Considering a f.d. locally compact Hausdorff space as a pro-etale algebraic space (i.e., as a pro-etale quotient of a locally profinite set), the !-functors are defined for it and agree with the usual topological ones.)
Some people are starting to write arguments in the generality of an abstract 6-functor formalism (that one would usually write just for etale cohomology or so), and it seems there's really a lot one can do. See also the appendix to Lecture 4, that you can introduce a Grothendieck topology and pass to stacks, and then one can even do descent, work proper or smooth-locally, etc, and suddenly working in an abstract 6-functor formalism feels like doing geometry. Even somewhat nontrivial things like hyperbolic localization seem to be possible in extremely high abstraction.