Homotopy type theory as internal languages of diagrams of \infty-logoses

arXiv2212.02444MaRDI QIDQ6507239FDOQ6507239

Authors: Taichi Uemura 

Abstract: We show that certain diagrams of $infty$-logoses are reconstructed in internal languages of their oplax limits via lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single $infty$-logos but also a diagram of $infty$-logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability -- a type theory for higher dimensional logical relations. To prove the main result, we establish a precise correspondence between the lex, accessible localizations of an $infty$-logos and the lex, accessible modalities in the internal language of the $infty$-logos. To do this, we also partly develop the Kripke-Joyal semantics of homotopy type theory in $infty$-logoses.

Mathematics Subject Classification ID

Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60)

This page was built for publication: Homotopy type theory as internal languages of diagrams of $\infty$-logoses

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6507239)