nLab (infinity,2)-topos

Idea

An (∞,2)-category of (∞,2)-sheaves. The joint higher generalization of the notion of (∞,1)-topos and 2-topos.

The archetypical example is the (infinity,2)-category of (infinity,1)-categories $Cat_{(\infty,1)}$. See also at formal category theory.

Related concepts

• formal $(\infty,1)$-category theory

• directed homotopy type theory

flavors of higher toposes

• 1-topos

  • (0,1)-topos

  • (1,1)-topos = topos

  • (2,1)-topos

  • $(n,1)$-topos

  • (∞,1)-topos ($n$-localic)

    $\;\;\;\;$ model topos

• 2-topos

  • (2,2)-topos ($n$-localic)

  • (∞,2)-topos

• $n$-topos

  • $(\infty,n)$-topos

References

Discussion of, potentially, the internal language of $(\infty,2)$-toposes as a form of directed homotopy type theory:

• Denis-Charles Cisinski, Hoang Kim Nguyen, Tashi Walde: Univalent Directed Type Theory, lecture series in the CMU Homotopy Type Theory Seminar (13, 20, 27 Mar 2023) [web]

  Abstract: We will introduce a version of dependent type theory that is suitable to develop a synthetic theory of 1-categories. The axioms are both a fragment and an extension of ordinary dependent type theory. The axioms are chosen so that (∞,1)-category theory (in the form of quasi-categories or complete Segal spaces) gives a semantic interpretation, in a way which extends Voevodsky‘s interpretation of univalent dependent type theory in the homotopy theory of Kan complexes. More generally, using a slight generalization of Shulman’s methods, we should be able to see that the theory of (∞,1)‑categories internally in any ∞‑topos (as developed by Martini and Wolf) is a semantic interpretation as well (hence so is parametrized higher category theory introduced by Barwick, Dotto, Glasman, Nardin and Shah). There are of course strong links with ∞-cosmoi of Riehl and Verity as well as with cubical HoTT (as strongly suggested by the work of Licata and Weaver), or simplicial HoTT (as in the work of Buchholtz and Weinberger). We will explain the axioms in detail and have a glimpse at basic theorems and constructions in this context (Yoneda Lemma, Kan extensions, Localizations). We will also discuss the perspective of reflexivity: since the theory speaks of itself (through directed univalence), we can use it to justify new deduction rules that express the idea of working up to equivalence natively (e.g. we can produce a logic by rectifying the idea of having a locally cartesian type). In particular, this logic can be used to produce and study semantic interpretations of HoTT.