My question is whether a symmetric monoidal $2$-category of ``cohomological correspondences'' has been been rigorously constructed anywhere in the literature. 

Let me be more precise about what I mean.

Let us fix a base field $k$ and a prime $\ell$ invertible on $S$. This ``category'' is supposed to be a $2$-category such that 

1) its objects are pairs $(X,\mathcal{F})$ of a finite type $k$-scheme $X$ and an object $\mathcal{F}\in D(X; \mathbf{F}_\ell)$;

2) $1$-morphisms between $(X, \mathcal{F})$ and $(Y, \mathcal{G})$ are given by $(S, f, g, \varphi)$, where $S$ is a correspondence $X\xleftarrow{f} S\xrightarrow{g} Y$ and $\varphi\colon f^*\mathcal{F}\to g^!\mathcal{G}$ is a morphism in $D(S, \mathbf{F}_\ell)$. 

3) Composition of $1$-morphisms $(S,f, g, \varphi_S)\in \mathrm{Hom}\left((X, \mathcal{F}), (Y, \mathcal{G})\right)$ and $(S', f', g', \varphi_{S'})\in\mathrm{Hom}\left((Y, \mathcal{G}), (Z,\mathcal{H})\right)$ is $(S\times_{Y}S', f\circ p_1, g'\circ p_2, \psi)$ where $p_1\colon S\times_Y S' \to S$ (and similarly $p_2$) is the projection map, and $\psi$ is the composition
$$
p_1^*f^*\mathcal{F}\xrightarrow{p_1^*(\varphi_S)} p_1^*g^!\mathcal{G} \to p_2^!{f'}^*\mathcal{G}\xrightarrow{p_2^!(\varphi_{S'})} p_2^!{g'}^!\cal{H},
$$
where the middle morphism is the base change transformation. 


3) $2$-morphisms between $(S,f, g, \varphi_S)$ and $(S', f', g', \varphi_{S'})$ are given by proper morphisms $h\colon S \to S'$ such that $f=f'\circ h$, $g=g'\circ h$, and the composition
$$
{g'}^*\mathcal{F} \to \mathrm{R}h_*h^*(g')^*\mathcal{F} \simeq \mathrm{R}h_!g^*\mathcal{F}\xrightarrow{\mathrm{R}h_!(\varphi)}\mathrm{R}h_!f^!\mathcal{F} \simeq \mathrm{R}h_!h^!{f'}^!\mathcal{F}\to {f'}^!\mathcal{F}
$$ 
is equal to $\varphi'$, where the first and the last maps are induced by adjunctions. 

4) Symmetric monoidal structure should be given by $(X, \mathcal{F})\otimes (Y,\mathcal{G})=(X\times Y, \mathcal{F} \boxtimes \mathcal{G})$.

In order to make this into an actual symmetric monoidal $2$-category, one needs to specify higher data and check certain compatibilities. However, it seems pretty tricky to do explicitly. One reason is that one needs to check that certain morphisms are equal in the derived category, and this seems quite tricky. The second issue is that (to the best of my understanding) it is pretty difficult to write down explicitly all higher coherence data needed to define a symmetric monoidal $2$-category. 

However, I have seen various authors using this $2$-category without really specifying higher data. Has it been really worked out anywhere? 

P.S. As far as I understand, an $(\infty, 2)$-analogue of this category has been claimed in a book of Gaitsgory and Rozenblyum, and that category has not been constructed since then. But I wonder if even the usual $2$-categorical version was rigorously constructed.