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? ...
It can be shown (see Is every paracompact, Hausdorff, locally contractible space homotopy equivalent to a CW complex?) that if $X$ is a locally contractible paracompact Hausdorff space such that the ...
Edit: The claim below is wrong, as explained in the comments, because infinite homotopy products of simplicial sets require their components to be fibrantly replaced first, unlike finite homotopy ...
By site of manifolds Man, I mean the category of manifolds (maybe submanifolds to obtain a small category) with continuous maps between them. A Grothendieck topology is given by open covers. Actually, ...
Consider the global projective model category of simplicial presheaves on some category (the category of smooth manifolds is particularly interesting to me). In Section 9.1 of Dugger's paper ...