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 ...
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 ...
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, ...
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 ...
It is a classical fact (e.g. here) that for an (accessible) right adjoint comonad on a (sheaf) topos, its Eilenberg-Moore category of coalgebras is itself a (sheaf) topos. I suppose this remains true ...