Berthelot's coherence and overconvergence conjecture for relative rigid cohomology

Let $(S,S,\mathcal{S})$ be a triple endowed with a lift of Frobenius on $\mathcal{S}$, and let

$$(X,\overline{X}) \xrightarrow{f} (Y,\overline{Y}) \xrightarrow{g} (S,S)$$

be a diagram of pairs such that $f:\overline{X}\to\overline{Y}$ is proper, $f^{-1}(Y)=X$, and $f|_X:X\to Y$ is smooth. Let $\mathcal{E}$ be an overconvergent $(F\text{-})$isocrystal on $(X,\overline{X})/\mathcal{S}_K$, and let $q\geq 0$. For the subcategory $\mathcal{C}$ of $(Y,\overline{Y})$-triples over $(S,S,\mathcal{S})$ specified by the conjecture, write $I^{\dagger}((Z,\overline{Z})/\mathcal{S}_K,\mathcal{Z})$ for the category of overconvergent isocrystals over $\mathcal{Z}$, and let $p_i$ denote the projections from the realization over $\mathcal{Z}\times_{\mathcal{S}}\mathcal{Z}$ to that over $\mathcal{Z}$. Berthelot's conjecture. There exists a subcategory $\mathcal{C}$ such that there exists uniquely an overconvergent $(F\text{-})$isocrystal $\mathcal{F}$ on $(Y,\overline{Y})/\mathcal{S}_K$ whose restriction to every $(Z,\overline{Z},\mathcal{Z})\in\mathcal{C}$ with $\mathcal{Z}$ formally smooth over $\mathcal{S}$ near $Z$ is functorially given by

$$\left(R^qf_{(X\times_Y Z,\overline{X}\times_{\overline{Y}}\overline{Z})/\mathcal{Z},\operatorname{rig}*}\mathcal{E},\epsilon\right),$$

where $\epsilon$ is the canonical pair of base-change isomorphisms through $\mathcal{Z}\times_{\mathcal{S}}\mathcal{Z}$. This weaker version is intended to be sufficient for the unique existence of the $q$-th rigid-cohomology overconvergent isocrystal, while the stronger version requires the condition for every suitable triple.