Forcing in Homotopy Type Theory - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-22T00:09:21Z http://mathoverflow.net/feeds/question/118857 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/118857/forcing-in-homotopy-type-theory Forcing in Homotopy Type Theory Jon Beardsley 2013-01-14T05:11:17Z 2013-01-14T17:04:45Z <p>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?</p> <p>Thanks</p> http://mathoverflow.net/questions/118857/forcing-in-homotopy-type-theory/118894#118894 Answer by Urs Schreiber for Forcing in Homotopy Type Theory Urs Schreiber 2013-01-14T16:11:03Z 2013-01-14T16:20:09Z <p>In as far as we regard <a href="http://ncatlab.org/nlab/show/forcing" rel="nofollow">forcing</a> as forming <a href="http://ncatlab.org/nlab/show/internal%20sheaf" rel="nofollow">internal sheaves</a>, the question is asking how to say "internal category of sheaves" in <a href="http://ncatlab.org/nlab/show/homotopy%20type%20theory" rel="nofollow">homotopy type theory</a>. </p> <p>It is expected that this works in directed analogy with the situation in ordinary type theory by considering <a href="http://ncatlab.org/nlab/show/internal%20site" rel="nofollow">internal sites</a>, except that there is a technical problem currently not fully solved: in homotoy type theory an internal category is necessarily an <a href="http://ncatlab.org/nlab/show/internal%20%28infinity,1%29-category" rel="nofollow">internal (infinity,1)-category</a> and in order to say this one needs to be able to say "(semi-)<a href="http://ncatlab.org/nlab/show/simplicial%20object%20in%20an%20%28infinity,1%29-category" rel="nofollow">simplicial object</a> in the homotopy type theory". This might seem immediate, but is a little subtle, due to the infinite tower of higher coherences involved. For <em>truncated</em> internal categories one might proceed "by hand" as indicated <a href="http://ncatlab.org/nlab/show/category+object+in+an+%28infinity%2C1%29-category#HomotopyTypeTheoryFormulation" rel="nofollow">here</a>. A general formalization has recently been proposed by Voevodsky -- see the webpage <em><a href="http://uf-ias-2012.wikispaces.com/Semi-simplicial+types" rel="nofollow">UF-IAS-2012 -- Semi-simplicial types</a></em> -- 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 <em>changing</em> 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.)</p> <p>However, that all said, there is something else which one can do and which <em>does</em> work: if an $\infty$-topos is equipped with a notion of (formally) <em>&eacute;tale morphisms</em>, 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) &eacute;tale maps</p> <p>It may seem surprising on first sight, but this can be saiD in homotopy type theory and it can be said naturally and elegantly:</p> <p>For this we simply add the axioms of <em>differential <a href="http://ncatlab.org/nlab/show/cohesive%20homotopy%20type%20theory" rel="nofollow">cohesive homotopy type theory</a></em> to plain homotopy type theory. This means that we declare there to be two adjoint triples of idempotent (co)monadic <a href="http://ncatlab.org/nlab/show/modal%20type%20theory" rel="nofollow">modalities</a> called</p> <p><a href="http://ncatlab.org/nlab/show/shape%20modality" rel="nofollow">shape modality</a> $\dashv$ <a href="http://ncatlab.org/nlab/show/flat%20modality" rel="nofollow">flat modality</a> $\dashv$ <a href="http://ncatlab.org/nlab/show/sharp%20modality" rel="nofollow">sharp modality</a></p> <p>and</p> <p><a href="http://ncatlab.org/nlab/show/reduction%20modality" rel="nofollow">reduction modality</a> $\dashv$ <a href="http://ncatlab.org/nlab/show/infinitesimal+shape+modality" rel="nofollow">infinitesimal shape modality</a> $\dashv$ <a href="http://ncatlab.org/nlab/show/infinitesimal+flat+modality" rel="nofollow">infinitesimal flat modality</a> .</p> <p>Using this we say: a function is formally &eacute;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 &eacute;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.</p> <p>What I just indicated is discussed in detail in section 3.10.4 and 3.10.7 of the notes</p> <p><em>Differential cohomology in a cohesive $\infty$-topos</em></p> <p>( <a href="http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos" rel="nofollow">http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos</a> )</p> <p>For more details on the above axioms of cohesive homotopy type theory see the first section of my article with Mike Shulman:</p> <p><em>Quantum gauge field theory in Cohesive homotopy type theory</em></p> <p>( <a href="http://ncatlab.org/schreiber/show/Quantum+gauge+field+theory+in+Cohesive+homotopy+type+theory" rel="nofollow">http://ncatlab.org/schreiber/show/Quantum+gauge+field+theory+in+Cohesive+homotopy+type+theory</a> )</p>