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? ...
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 ...