In as far as we regard forcing as forming internal sheaves, the question is asking how to say "internal category of sheaves" in homotopy type theory.
It is expected that this works in directed analogy with the situation in ordinary type theory by considering internal sites, except that there is a technical problem currently not fully solved: in homotoy type theory an internal category is necessarily an internal (infinity,1)-category and in order to say this one needs to be able to say "(semi-)simplicial object in the homotopy type theory". This might seem immediate, but is a little subtle, due to the infinite tower of higher coherences involved. For truncated internal categories one might proceed "by hand" as indicated here. A general formalization has recently been proposed by Voevodsky -- see the webpage UF-IAS-2012 -- Semi-simplicial types -- but this definition does not in fact at the moment work in homotopy type theory. (Last I heard was that Voevodsky had been thinking about changing homotopy type theory itself to make this work. But this is second-hand information only, we need to wait for one of the IAS-HoTT fellows to see this here and give us first-order news on this.)
However, that all said, there is something else which one can do and which does work: if an $\infty$-topos is equipped with a notion of (formally) étale morphisms, then one can speak about internal sheaves over the canonical internal site of any object without explicitly considering the internal site itself: the "petit (infintiy,1)-topos" of sheaves on a given object $X \in \mathbf{H}$ is the full sub-(oo,1)-category of the slice over $X$ on the (formally) étale maps
It may seem surprising on first sight, but this can be saiD in homotopy type theory and it can be said naturally and elegantly:
For this we simply add the axioms of differential cohesive homotopy type theory to plain homotopy type theory. This means that we declare there to be two adjoint triples of idempotent (co)monadic modalities called
shape modality $\dashv$ flat modality $\dashv$ sharp modality
and
reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality .
Using this we say: a function is formally étale if its naturality square of the unit of the "infinitesimal shape modality" is a homotopy pullback square. Then we have available in the homotopy type theory the sub-slice over any $X$ on those maps that are formally étale. This is internally the $\infty$-topos of $\infty$-stacks over $X$, hence the "forcing of $X$" in terms of the standard interpretation of forcing as passing to sheaves.
What I just indicated is discussed in detail in section 3.10.4 and 3.10.7 of the notes
Differential cohomology in a cohesive $\infty$-topos
( http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos )
For more details on the above axioms of cohesive homotopy type theory see the first section of my article with Mike Shulman:
Quantum gauge field theory in Cohesive homotopy type theory
( http://ncatlab.org/schreiber/show/Quantum+gauge+field+theory+in+Cohesive+homotopy+type+theory )
There are two kinds of answers as to what kind of category a "homotopy type theory" is the internal language of. On the one hand there is a kind of $(\infty,1)$-category that is the semantic object of real interest; but on the other hand there is a 1-categorical presentation of the latter that corresponds more closely to the syntax of the type theory. The latter kind of category (whose variants go by names like "contextual category", "category with families", "category with attributes", "type-theoretic fibration category", "tribe", etc.) is also closely related to the model categories and fibration categories used to present $(\infty,1)$-categories in classical abstract homotopy theory.
For instance, HoTT with $\mathrm{Id},\Sigma,\Pi$ and function extensionality, but no universes, corresponds (conjecturally) to locally cartesian closed $(\infty,1)$-categories — presented by means of "$\Pi$-tribes" (or whatever other name you prefer for the latter).
Cubical type theory is a syntactic variation which changes the corresponding 1-categorical presentations, but not the desired $(\infty,1)$-categorical semantics. That is, the analogous cubical type theory, with $\mathrm{Id},\Sigma,\Pi$ (and, in the cubical case, provable function extensionality), but no universes, also corresponds (conjecturally) to locally cartesian closed $(\infty,1)$-categories, but now presented in a different way by $\Pi$-tribes containing (or more precisely, fibered over the theory of) some kind of "interval object". There is a sketch of the latter kind of category (for a more general kind of "type theory with shapes") in appendix A of https://arxiv.org/abs/1705.07442.
Best Answer
Mike Shulman has a good discussion of what exactly needs to be shown in his
The issue is that in the type theory the classification of objects is by strict pullbacks. So roughly the problem is that one has to show the object classifier of a random $\infty$-topos is, when the latter is presented by a type-theoretic model category, presented by an object which classifies other objects by strict pullbacks with strict respect for composition. Establishing this in generality is (or would be) a kind of semi-strictification result for $\infty$-toposes.
See also the other references in the nLab entry.