Modeling Univalence in Subtoposes

Homotopy Type Theory

In my recent post at the n-Category Café, I described a notion of « higher modality » in type theory, which semantically ought to represent a left-exact-reflective sub-$latex (infty,1)$-category of an $latex (infty,1)$-topos ? once we can prove that homotopy type theory has models in $latex (infty,1)$-toposes. I’ve since realized that this theory may also be useful in proving that latter fact itself. For if we have a set-theoretic model which contains such a modality $latex sharp$, then we ought to be able to show that the resulting left-exact-reflective subcategory of the model also supports such a model. If this works, it should simplify the search for models of univalence in $latex (infty,1)$-toposes, since any $latex (infty,1)$-topos is a left-exact localization of an $latex (infty,1)$-category of presheaves, and the latter can be presented by model categories that are easier to understand concretely.

Moreover, given a suitable inductive definition of type theory…

View original post 749 mots de plus