9 problems

Awodey's conjecture. Every $(\infty,1)$-topos admits a model-categorical presentation that supports a full model of HoTT.

Grothendieck infinity-topos conjecture. Every Grothendieck infinity-topos gives rise to a model of homotopy type theory.

Let an object of the $\infty$-topos of parametrised pointed spaces consist of a space $B$ together with a family $E:\mathrm{Fun}(B,\mathcal{S}_\star)$ of pointed spaces. In the int…

An $\infty$-topos is an infinity-categorical analogue of a topos, and axiomatic homotopy type theory (axiomatic HoTT) is the version of homotopy type theory including Martin–Löf ty…

Let $\mathbb{T}\mathrm{opos}_\infty^{op} \subseteq {\mathbb{C}\mathrm{at}_\infty^{\mathrm{diff}}}$ be the subcategory consisting of $\infty$-toposes and left exact colimit-preservi…

Strict univalent universes conjecture. Any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent u…

Elementary infinity-topos model conjecture. It is conjectured that every elementary $(\infty,1)$-topos is a model of HoTT.

An $(\infty,1)$-topos is a left-exact localization of the functor category … for a small $(\infty,1)$-category $\mathcal{C}$. Interpretability conjecture. Elementary homotopy type…

Internal-language conjecture. Homotopy type theory is conjectured to be the internal language of elementary $\infty$-toposes.