A categorical K\"unneth formula for constructible Weil sheaves

We prove a K\"unneth-type equivalence of derived categories of lisse and constructible Weil sheaves on schemes in characteristic $p > 0$ for various coefficients, including finite discrete rings, algebraic field extensions $E \supset \mathbf Q_\ell$, $\ell \ne p$ and their rings of integers $O_E$. We also consider a variant for ind-construtible sheaves which applies to the cohomology of moduli stacks of shtukas over global function fields.