Bi-interpretability conjecture for the internal language of derived $\Gamma$-geometry

Let the internal language of derived $\Gamma$-geometry be the language associated with its $\Gamma$-topoi, and let dependent type theory be extended by a ternary connective modeling the $\Gamma$-multiplication. Bi-interpretability conjecture. The internal language of derived $\Gamma$-geometry is bi-interpretable with dependent type theory equipped with a ternary connective modeling the $\Gamma$-multiplication. This proposes a foundational logical equivalence between derived $\Gamma$-geometry and an enriched dependent type theory; the source gives no resolution or supporting theorem.