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 )
With respect to the first question, expanding on my comment which pointed out the nLab page dependent linear type theory and the article by Urs Schreiber, 'Quantization via Linear homotopy types', I'd like to pass on some additional relevant commentary by Urs.
There is a way to express linearity for homotopy types, see stable homotopy type. As Simon pointed out in his comment, the category of parametrized spectra is an ∞-topos, indeed a tangent ∞-topos. One can then look to add an axiom to HoTT that makes it the internal language for tangent ∞-toposes. That axiom should be:
there is a pointed type $X_\ast$
the morphism $\Sigma \Omega X_\star \to X_\star$ is an equivalence
So far this makes the ambient category "linear" in the terminology of Schwede's old article on parameterized spectra. One could now continue to add the axioms
- the morphism $\Sigma \Omega(X_\star^{S_\star}) \to X_\star^{S_\star}$ is an equivalence, for finite pointed powers.
If one could add the infinite set of these axioms, that would be Goodwillie's localization for the tangent $\infty$-topos.
There's work in preparation by Mathieu Anel, Eric Finster, and André Joyal along these lines.
Best Answer
Perhaps this will help: in homotopy type theory, to say that $x$ and $y$ of type $A$ are different corresponds intuitively to the fact that they are in different connected components, i.e., there is no path between them.
Specifically, for the circle $S^1$:
The statement $\Pi(x, y: S^1).\, x = y$ ("All points are equal") should be understood geometrically as saying that there is a continuous map which to each pair of points assigns a path between them.
The statement $\Sigma(x, y : S^1).\, x \neq y$ ("There are two different points") should be understood as saying that there are points on the circle which are not connected by a path.
Neither of the above is the case. What is the case, though is that $\Pi (x, y : S^1) . \|x = y\|_{-1}$ ("Every two points are in the same connectedness component.")