Forcing in Homotopy Type Theory

2013-01-14T05:11:17Z

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

Answer by Urs Schreiber for Forcing in Homotopy Type Theory

2013-01-14T16:11:03Z

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 )

Forcing in Homotopy Type Theory - MathOverflow

Forcing in Homotopy Type Theory

Answer by Urs Schreiber for Forcing in Homotopy Type Theory