I apologize if this question doesn't make any sense. I'll just go ahead and delete it if that's the case. But the question is just the title. Is there a notion of forcing in homotopy type theory? Presumably we do homotopy type theory in some $(\infty,1)$-topos, so we can axiomatize the notions accordingly? Does anyone know of a reference for this kind of thing if it does exist or makes sense?


Thanks



Forcing in Homotopy Type Theory
In as far as we regard [forcing](http://ncatlab.org/nlab/show/forcing) as forming [internal sheaves](http://ncatlab.org/nlab/show/internal%20sheaf), the question is asking how to say "internal category of sheaves" in [homotopy type theory](http://ncatlab.org/nlab/show/homotopy%20type%20theory). 


It is expected that this works in directed analogy with the situation in ordinary type theory by considering [internal sites](http://ncatlab.org/nlab/show/internal%20site), 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](http://ncatlab.org/nlab/show/internal%20%28infinity,1%29-category) and in order to say this one needs to be able to say "(semi-)[simplicial object](http://ncatlab.org/nlab/show/simplicial%20object%20in%20an%20%28infinity,1%29-category) 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](http://ncatlab.org/nlab/show/category+object+in+an+%28infinity%2C1%29-category#HomotopyTypeTheoryFormulation). A general formalization has recently been proposed by Voevodsky -- see the webpage *[UF-IAS-2012 -- Semi-simplicial types](http://uf-ias-2012.wikispaces.com/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](http://ncatlab.org/nlab/show/cohesive%20homotopy%20type%20theory)* to plain homotopy type theory. This means that we declare there to be two adjoint triples of idempotent (co)monadic [modalities](http://ncatlab.org/nlab/show/modal%20type%20theory) called


[shape modality](http://ncatlab.org/nlab/show/shape%20modality) $\dashv$ [flat modality](http://ncatlab.org/nlab/show/flat%20modality) $\dashv$ [sharp modality](http://ncatlab.org/nlab/show/sharp%20modality)


and


[reduction modality](http://ncatlab.org/nlab/show/reduction%20modality) $\dashv$ [infinitesimal shape modality](http://ncatlab.org/nlab/show/infinitesimal+shape+modality) $\dashv$ [infinitesimal flat modality](http://ncatlab.org/nlab/show/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> )


