# Forcing in Homotopy Type Theory

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

-
and, while we are at it, what could it be used for? –  Jacob Bell Jan 14 '13 at 8:16
Probably improving the efficiency of the internal combustion engine. –  Jon Beardsley Jan 14 '13 at 15:40
Can you add the tag lo.logic ? Thanks! (Later on, there will perhaps be a need for a HoTT tag, but in the meantime I think adding logic as a tag to questions like this will help, as the people interested in HoTT aren't necessarily interested in set theory, nor abstract homotopy or infinity-topos theory outside of the type-theoretic context.) –  Ulrik Buchholtz Jan 14 '13 at 16:40

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

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

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

-
Not to say that the people at nForum only consider useless stuff! =P –  Jon Beardsley Jan 14 '13 at 16:26
Nice summary, Urs. I don't know of any further developments on the semisimplicial objects front, except that Hugo Herbelin has attacked it from a similar but different direction to Voevodsky and come quite close; he might even have succeeded by now. It's not entirely clear to me whether the problem is merely a (terrifically difficult) bookkeeping one, or something more basic. –  Mike Shulman Jan 14 '13 at 20:56
One other thing which I might add is that for a very simple class of cases, there is an alternative approach: arxiv.org/abs/1203.3253 –  Mike Shulman Jan 14 '13 at 20:57
Jon, we have no use for things that have no use. And if it has no use, you cannot force it. –  Urs Schreiber Jan 14 '13 at 23:37
@Urs, haha, no it's great. People are too serious on here anyway. –  Jon Beardsley Jan 18 '13 at 18:36