1 Introduction↩︎

An \(\infty\)-logos, also known as an \(\infty\)-topos [1], [2]¹, is an \((\infty, 1)\)-category that looks like the \((\infty, 1)\)-category of spaces, among other aspects of it. An \(\infty\)-logos is a place where one can do homotopy theory just as an ordinary logos is a place where one can do set-level mathematics.

Homotopy type theory [3] is another place to do homotopy theory. It is a type theory in the style of Martin-Löf [4] extended by the univalence axiom and higher inductive types. The former forces types to behave like spaces rather than sets, and the latter allow us to build types representing spaces such as spheres and tori.

\(\infty\)-logoses are conjectured to admit interpretations of homotopy type theory so that theorems proved in homotopy type theory can be translated in an arbitrary \(\infty\)-logos. Although the conjecture has not yet been fully solved (see, for example, [5] for substantial progress), homotopy type theory has brought insight to \(\infty\)-logos theory. For example, the proof of the Blakers-Massey connectivity theorem in homotopy type theory [6] has led to a new generalized Blakers-Massey theorem that holds in an arbitrary \(\infty\)-logos [7].

An \(\infty\)-logos, however, does not live alone. \(\infty\)-logoses are often connected by functors which are also connected by natural transformations. Plain homotopy type theory is, at first sight, not sufficient to reason about a diagram of \(\infty\)-logoses, because the actions of the functors and natural transformations are not internalized to type theory. Even worse, it is impossible to naively internalize some diagrams: some internal adjunction leads a contradiction [8]; there are only trivial internal idempotent comonads [9]. While there is no chance of naive internalization of such interesting but problematic diagrams to plain homotopy type theory, some other diagrams can be internalized in a clever way pointed out by Shulman². A minimal non-trivial example is a diagram consisting of two \(\infty\)-logoses and a lex, accessible functor between them in one direction. The two \(\infty\)-logoses are lex, accessible localizations of another \(\infty\)-logos obtained by the Artin gluing for the functor, and the functor is reconstructed by composing the inclusion from one localization and the reflector to the other. Moreover, this reconstruction is internal to the glued \(\infty\)-logos, because lex, accessible localizations of an \(\infty\)-logos are expected to correspond to lex, accessible modalities in its internal language. Hence, plain homotopy type theory as a language for the glued \(\infty\)-logos is sufficient to reason about the original diagram.

In this paper, we propose a class of shapes of diagrams of \(\infty\)-logoses for which the internal reconstruction technique explained in the previous paragraph works. We call shapes in the proposed class mode sketches. Our main results are summarized as follows. Let \(\modesketch\) be a mode sketch.

1. We associate to \(\modesketch\) certain axioms in type theory, one of which is to postulate some lex, accessible modalities from which one can construct a diagram of \(\infty\)-logoses internally to type theory ([sec:modes] [sec:mode-sketches-1]).

2. We show that the \((\infty,1)\)-category of models of the axioms associated to \(\modesketch\) in \(\infty\)-logoses is equivalent to the \((\infty,1)\)-category of diagrams of \(\infty\)-logoses indexed over \(\modesketch\) ([thm:main-theorem]), where \(\modesketch\) is regarded as a presentation of an \((\infty, 2)\)-category. The right to left construction is given by oplax limits, a generalization of the Artin gluing [10], [11].

In [sec:synth-tait-comp-1] [sec:modal-local] [sec:oplax-limits-1] below, we explain other new results ([prop:canonical-join-accessible] [thm:equiv-two-mode-sketch-axioms] [prop:logos-accessible-oplax-limit] [prop:oplax-univalence] [prop:mate-correspondence]).

This paper is an extended version of our conference paper [12]. The conference version presents [prop:canonical-join-accessible] and proof sketches of [thm:main-theorem] [thm:equiv-two-mode-sketch-axioms]. The current version includes every detail of those results. The statement of [thm:main-theorem] is modified not to rely on an interpretation of type theory in \(\infty\)-logoses.

1.1 Modalities in homotopy type theory↩︎

A modality in homotopy type theory [13]–[15] is a subuniverse satisfying certain conditions. A modality that is moreover lex and accessible is expected to correspond to a sub-\(\infty\)-topos or a localization of a \(\infty\)-logos [16], [17]. The fracture and gluing theorem of Rijke, Shulman, and Spitters [13] Theorem 3.50 gives a construction of the join \(\mode \lor \modeI\) of two lex modalities \(\mode\) and \(\modeI\) under some assumption. The join obtained by this theorem satisfies that every type \(\ty\) in \(\mode \lor \modeI\) is canonically fractured into a type \(\ty_{\modeI}\) in \(\modeI\) and a type family \(\ty_{\mode}\) on \(\ty_{\modeI}\) valued in \(\mode\), and \(\ty\) is reconstructed as \(\ty \simeq \ilexists_{\var : \ty_{\modeI}} \ty_{\mode}(\var)\).

In this paper, we improve the fracture and gluing theorem. We show that the construction of joins of lex modalities preserves accessibility as well ([prop:canonical-join-accessible]).

1.2 Synthetic Tait computability↩︎

The fracture and gluing theorem is used in Sterling’s synthetic Tait computability [18], [19]. It is a technique of working with logical relations, which are used in the study of type theories and programming languages, in an internal language for the Artin gluing and has applications to, for example, normalization theorems for complex type theories [20], [21]. There the fracture and gluing theorem is instantiated by the closed and open modalities associated to a proposition. Then every type in the internal language is canonically fractured into an open type and a closed (unary, proof-relevant) relation on it which are glued back together. The internal language for the Artin gluing is thus a type theory with an indeterminate proposition in which types are relations and provides a synthetic method of working with logical relations.

In this paper, we relate synthetic Tait computability and mode sketches. The core axiom for synthetic Tait computability is to postulate some indeterminate propositions. We show that part of the axioms associated to a mode sketch is equivalent to postulating a lattice of propositions ([thm:equiv-two-mode-sketch-axioms]).

Mode sketches thus provide a synthetic method of working with logical relations that is alternative to and generalizes synthetic Tait computability. This is also natural from Shulman’s point of view [11] that interpretations of type theory in oplax limits are generalized logical relations. Since we work in homotopy type theory, what we get is actually higher-dimensional logical relations, and our primary application of mode sketches in upcoming paper(s) [22] will be normalization for \(\infty\)-type theories introduced by Nguyen and Uemura [23] as a higher-dimensional generalization of type theories.

1.3 Oplax limits of \((\infty, 1)\)-categories↩︎

Oplax limits are special \((\infty, 2)\)-categorical limits and analogous to oplax limits in \(2\)-category theory [24]–[26]. Oplax limits indexed over \((\infty, 1)\)-categories are studied by Gepner, Haugseng, and Nikolaus [27] and generalized to arbitrary indexing \((\infty, 2)\)-categories by Gagna, Harpaz, and Lanari [28].

Oplax limits of \(\infty\)-logoses are of our interest. Wraith [10] shows that the oplax limit of a diagram of (elementary) logoses and lex functors is a logos. Lurie [1] Proposition 6.3.2.3 shows that the conical limit of a diagram of \(\infty\)-logoses is an \(\infty\)-logos.

The oplax limit of a diagram classifies oplax natural transformations from a constant diagram to the given diagram just as a (conical) limit classifies natural transformations from a constant diagram. It is known [29] Theorem 3.8.1 that natural transformations between diagrams of \((\infty ,1)\)-categories correspond to fibered functors between the \((\infty, 2)\)-categories of elements of the diagrams. Oplax natural transformations between diagrams of \((\infty, 1)\)-categories are to correspond to not necessarily fibered functors between the \((\infty, 2)\)-categories of elements. Some special cases of this have already been proved: Haugseng et al. [30] Theorem E show the case when the diagrams are indexed over an \((\infty ,1)\)-category; Gagna, Harpaz, and Lanari [28] Corollary 4.4.3 show the case when the domain is constant on the point.

The mate correspondence is a useful source of oplax natural transformations. In the \(2\)-categorical case [31], it asserts that given two diagrams \(\fun\) and \(\funI\) of categories, oplax natural transformations \(\fun \to \funI\) that are point-wise left adjoints correspond to lax natural transformations \(\funI \to \fun\) that are point-wise right adjoints. An \((\infty, 2)\)-categorical version is proved by Haugseng et al. [30] Corollary F in the form of an equivalence between the \((\infty, 1)\)-categories of oplax/lax natural transformations in the special case when the diagrams are indexed over an \((\infty, 1)\)-category.

In this paper, we show some new results on oplax limits of \((\infty, 1)\)-categories. All of them are consequences of results in the literature, but it is worth stating them explicitly. We prove an \(\infty\)-analogue of the result of Wraith [10]: the oplax limit of a diagram of \(\infty\)-logoses and lex, accessible functors is an \(\infty\)-logos ([prop:logos-accessible-oplax-limit]). We show that oplax natural transformations between diagrams of \((\infty, 1)\)-categories correspond to arbitrary functors between the \((\infty, 2)\)-categories of elements ([prop:oplax-univalence]) by reducing it to the special cases proved by Haugseng et al. [30] and Gagna, Harpaz, and Lanari [28]. We show the mate correspondence for diagrams indexed over an arbitrary \((\infty, 2)\)-category in the form of an equivalence between the spaces of oplax/lax natural transformations ([prop:mate-correspondence]).

1.4 Organization↩︎

The paper is split into two parts. The first part ([sec:modal-homot-type] [sec:mode-sketches] [sec:mode-sketch-synth]) provides the theory of mode sketches internally to type theory. The second part ([sec:high-categ-theory] [sec:semant-mode-sketch]) is devoted to semantics of mode sketches in \(\infty\)-logoses. The two parts are independent of each other on a technical level.

In 2, we review the theory of modalities in homotopy type theory [13]. Our focus is on the poset of lex, accessible modalities and on the open and closed modalities associated to propositions.

[sec:mode-sketches,sec:mode-sketch-synth] are the core of the paper. We introduce the notion of a mode sketch ([def:mode-sketch]). For every mode sketch, we introduce two equivalent sets of axioms to encode a certain diagram of universes. One postulates some lex, accessible modalities while the other postulates a lattice of propositions. The open and closed modalities give a construction of the former from the latter which we show is an equivalence ([thm:equiv-two-mode-sketch-axioms]). The latter is a higher dimensional analogue of Sterling’s synthetic Tait computability [19].

5 is a preliminary section needed for the semantics of mode sketches.

Finally in 6, we show our main result ([thm:main-theorem]): for any mode sketch, the \((\infty,1)\)-category of models of the axioms associated to the mode sketch in \(\infty\)-logoses is equivalent to the \((\infty,1)\)-category of diagrams of \(\infty\)-logoses and lex, accessible functors indexed over the mode sketch.

1.5 Related work↩︎

An earlier version of cohesive homotopy type theory [32] uses modalities in plain homotopy type theory to internalize a series of adjunctions that arises in Lawvere’s axiomatic cohesion [33]. However, because naive internalization of adjunctions do not work well [8], [9], the axiomatization is tricky and not ideal to work with. The newer version of cohesive homotopy type theory [9] instead extends homotopy type theory by another layer of context and new modal operators. The resulting type theory works well for axiomatic cohesion but is complicated compared to plain homotopy type theory. It is also too optimized for axiomatic cohesion.

A more general framework for internal diagrams is multimodal dependent type theory [34]. It is roughly a family of type theories related to each other via modal operators and interpreted in a diagram of presheaf categories. The shape of diagram is specified directly by an arbitrary \(2\)-category which is called a mode theory in this context. Our terminology “mode sketch” is chosen to mean a sketch of a mode theory. Multimodal dependent type theory is potentially an internal language for diagrams of \(\infty\)-logoses, but for this one would have to rectify not only \(\infty\)-logoses but also functors and natural transformations between them.

Our work brings back the ideas of earlier cohesive homotopy type theory. Although it might not be the best type theory, it has a lot of advantages: modalities are internal to plain homotopy type theory, and thus all results are ready to formalize in existing proof assistants; keeping type theory simple is also important in informal use of type theory in which the correctness of application of inference rules is not checked by computer; the semantics is no more complicated than the \(\infty\)-logos semantics of homotopy type theory; it also opens the door to internalization of more general diagrams in a uniform way, which is the motivation for the current work.

2 Modalities in homotopy type theory↩︎

We review the theory of modalities in homotopy type theory [13]. In this section, we work in homotopy type theory. By homotopy type theory we mean dependent type theory with (dependent) function types, (dependent) pair types, a unit type, identity types (without equality reflection), at least two univalent universes $ : ,$ an empty type, pushouts, and localizations [13, Sec. 2.2]. Note that truncations are instances of localization. We mainly follow the HoTT Book [3] for terminologies and notations in homotopy type theory.

A modality is in short a reflective subuniverse closed under pair types.

An important class of modalities is accessible modalities which are roughly modalities “presented by small data”.

Another important class of modalities is lex modalities.

Modalities that are both lex and accessible are of particular importance because they correspond to subtoposes of an \(\infty\)-topos under the interpretation of types as sheaves on the \(\infty\)-topos. From now on, we are mostly interested lex, accessible modalities, so we give them a short name.

Fundamental examples of are open and closed modalities which correspond to open and closed, respectively, subtoposes.

2.1 The poset of lex, accessible modalities↩︎

Let \(\ilSU\) denote the poset of subuniverses where \(\mode \le \modeI\) if \(\ilIn_{\mode}(\ty) \to \ilIn_{\modeI}(\ty)\) for every \(\ty : \univ\). We have the full subposets of \(\ilSU\) \[\ilRSU \supset \ilModality \supset \ilAccModality \supset \ilLexAcc\] consisting of reflective subuniverses, modalities, accessible modalities, and lex, accessible modalities, respectively. We also have the full subposet $ $ of lex modalities. By definition, \(\ilLexAcc = \ilLex \cap \ilAccModality\). We study the poset \(\ilLexAcc\) in more detail.

The canonical meet of an arbitrary family of exists [13] Theorem 3.29 and Remark 3.23. Canonical joins are less understood than canonical meets. One important case when canonical joins exist and can be computed is the following.

The distributive law holds in some special cases.

2.2 Accessibility of the canonical join↩︎

Let us fill the gap in the proof of [prop:join-strongly-disjoint].

We have to find a null generator for \(\mode \lor \modeI\). A natural guess is the following.

[lem:nullgen-join-connected] shows \(\mode \lor \modeI \le \modeNull(\nullgen \join \nullgenI)\) for arbitrary accessible modalities \(\mode\) and \(\modeI\) and for arbitrary choices of \(\nullgen\) and \(\nullgenI\). We know neither if the other direction holds in general for some choices of \(\nullgen\) and \(\nullgenI\) nor if \(\modeNull(\nullgen \join \nullgenI)\) is independent of \(\nullgen\) and \(\nullgenI\). Note that Finster [35] observed that \(\modeNull(\nullgen \join \nullgenI)\) is lex whenever \(\modeNull(\nullgen)\) and \(\modeNull(\nullgenI)\) are lex. In the special case when \(\mode \le {}^{\orthMark} \modeI\), the idea of the proof of \(\mode \lor \modeI = \modeNull(\nullgen \join \nullgenI)\) is to show that \(\modeI\) is an open modality within the subuniverse of \(\modeNull(\nullgen \join \nullgenI)\)-modal types.

As a by-product, we have the following.

2.3 Open and closed modalities↩︎

We collect some properties of open modalities and closed modalities.

3 Mode sketches↩︎

We introduce mode sketches as shapes of diagrams of subuniverses definable internally to type theory. We work in homotopy type theory through the section.

3.1 Internal diagrams induced by modalities↩︎

We consider postulating some to encode some diagram of subuniverses. The fundamental observation is that a pair of induces a canonical functor between them.

We have two functors \(\opModality^{\mode}_{\modeI} : \univ_{\mode} \to \univ_{\modeI}\) and \(\opModality^{\modeI}_{\mode} : \univ_{\modeI} \to \univ_{\mode}\) for every pair of \(\mode\) and \(\modeI\), but we are often interested in only one direction. It is thus useful to cut off one direction by postulating that \(\mode \le {}^{\orthMark}\modeI\): by the definition of \(\modeI\)-connectedness, \(\opModality^{\mode}_{\modeI}\) becomes constant at the unit type. The other direction \(\opModality^{\modeI}_{\mode} : \univ_{\modeI} \to \univ_{\mode}\) remains non-trivial. Therefore, a pair \((\mode, \modeI)\) of such that \(\mode \le {}^{\orthMark}\modeI\) encodes a functor \(\univ_{\modeI} \to \univ_{\mode}\). When \(\modeI \le {}^{\orthMark} \mode\) is also assumed, \(\univ_{\mode}\) and \(\univ_{\modeI}\) are considered unrelated.

Given more than two , we have canonical natural transformations between the canonical functors.

Let \(\mode_{0}, \mode_{1}, \mode_{2}, \mode_{3}\) be . By naturality, the following diagram commutes. \[\begin{tikzcd} \opModality^{\mode_{3}}_{\mode_{0}} \arrow[r, "\unitModality^{\mode_{0}; \mode_{3}}_{\mode_{1}}"] \arrow[d, "\unitModality^{\mode_{0}; \mode_{3}}_{\mode_{2}}"'] & [8ex] \opModality^{\mode_{1}}_{\mode_{0}} \opModality^{\mode_{3}}_{\mode_{1}} \arrow[d, "\opModality^{\mode_{1}}_{\mode_{0}} \unitModality^{\mode_{1}; \mode_{3}}_{\mode_{2}}"] \\ [2ex] \opModality^{\mode_{2}}_{\mode_{0}} \opModality^{\mode_{3}}_{\mode_{2}} \arrow[r, "\unitModality^{\mode_{0}; \mode_{2}}_{\mode_{1}} \opModality^{\mode_{3}}_{\mode_{2}}"'] & \opModality^{\mode_{1}}_{\mode_{0}} \opModality^{\mode_{2}}_{\mode_{1}} \opModality^{\mode_{3}}_{\mode_{2}} \end{tikzcd}\] For more than four , higher coherence laws are also satisfied. Hence, a tuple $ ({0}, , {})$ of such that \(\mode_{\idx} \le {}^{\orthMark}\mode_{\idxI}\) for all \(\idx < \idxI\) encodes an \(\nat\)-simplex with vertices \(\univ_{\mode_{\idx}}\), edges \(\opModality^{\mode_{\idxI}}_{\mode_{\idx}} : \univ_{\mode_{\idxI}} \to \univ_{\mode_{\idx}}\) for \(\idx < \idxI\), triangles \[\begin{tikzcd} \univ_{\mode_{\idx}} & [3ex] & [3ex] \univ_{\mode_{\idxII}} \arrow[dl, "\opModality^{\mode_{\idxII}}_{\mode_{\idxI}}"] \arrow[ll, "\opModality^{\mode_{\idxII}}_{\mode_{\idx}}"', "\phantom{a}"{name = a0}] \arrow[from = a0, dl, Rightarrow, "\unitModality^{\mode_{\idx}; \mode_{\idxII}}_{\mode_{\idxI}}"{near start}, end anchor = {[yshift = 1ex]}] \\ & \univ_{\mode_{\idxI}} \arrow[ul, "\opModality^{\mode_{\idxI}}_{\mode_{\idx}}"] \end{tikzcd}\] for \(\idx < \idxI < \idxII\), and higher homotopies.

Shapes other than simplices are expressed by postulating invertibility of some of \(\unitModality^{\mode_{\idx}; \mode_{\idxII}}_{\mode_{\idxI}}\)’s. For example, let \(\mode_{0}, \mode_{1}, \mode_{2}, \mode_{3}\) be and suppose that \(\mode_{\idx} \le {}^{\orthMark}\mode_{\idxI}\) for all \(\idx < \idxI\), that \(\mode_{2} \le {}^{\orthMark}\mode_{1}\), and that \(\unitModality^{\mode_{0}; \mode_{3}}_{\mode_{1}}\) is invertible. We have a diagram \[\begin{tikzcd}[column sep = 14ex, row sep = 8ex] & \univ_{\mode_{1}} \arrow[dl, "\opModality^{\mode_{1}}_{\mode_{0}}"'] \\ \univ_{\mode_{0}} & & \univ_{\mode_{3}} \arrow[ul, "\opModality^{\mode_{3}}_{\mode_{1}}"'] \arrow[dl, "\opModality^{\mode_{3}}_{\mode_{2}}"] \arrow[ll, "\opModality^{\mode_{3}}_{\mode_{0}}"{description}, "\phantom{a}"'{name = a0}, "\phantom{a}"{name = a1}] \arrow[from = a0, to = ul, To, "\unitModality^{\mode_{0}; \mode_{3}}_{\mode_{1}}"', "\simeq", start anchor = {[yshift = 1ex]}, end anchor = {[yshift = -1ex]}] \arrow[from = a1, to = dl, To, "\unitModality^{\mode_{0}; \mode_{3}}_{\mode_{2}}", start anchor = {[yshift = -1ex]}, end anchor = {[yshift = 1ex]}] \\ & \univ_{\mode_{2}} \arrow[ul, "\opModality^{\mode_{2}}_{\mode_{0}}"] \end{tikzcd}\] which is equivalent to a diagram of the form \[\begin{tikzcd} & \univ_{\mode_{1}} \arrow[dl, "\opModality^{\mode_{1}}_{\mode_{0}}"'] \arrow[dd, To, start anchor = {[yshift = -2ex]}, end anchor = {[yshift = 2ex]}] \\ \univ_{\mode_{0}} & & \univ_{\mode_{3}}. \arrow[ul, "\opModality^{\mode_{3}}_{\mode_{1}}"'] \arrow[dl, "\opModality^{\mode_{3}}_{\mode_{2}}"] \\ & \univ_{\mode_{2}} \arrow[ul, "\opModality^{\mode_{2}}_{\mode_{0}}"] \end{tikzcd}\] We cannot, however, naively postulate some properties of the functors \(\opModality^{\modeI}_{\mode}\)’s such as conservativity, fullness, faithfulness, adjointness, and invertibility. This is because the internal statements of these conditions are too strong due to stability under substitution, and indeed some “no-go” theorems on internalizing properties of functors are known [[8] Theorem 5.1][9] Theorem 4.1.

3.2 Mode sketches↩︎

We introduce mode sketches as shapes of diagrams definable by the methodology explained in 3.1.

Let \(\modesketch\) be a mode sketch and \(\mode : \modesketch \to \ilLexAcc\) a function. We consider the following axioms.

[axm:mode-sketch-disjoint,axm:mode-sketch-invertible] are motivated by the observation made in 3.1. That is, when \(\idxI \not\leq \idx\), the functor in the direction \(\univ_{\mode(\idx)} \to \univ_{\mode(\idxI)}\) is cut off.

3.3 Intended models, internally↩︎

Let \(\modesketch\) be a mode sketch. In this subsection, we see, internally to type theory, what kind of an \(\infty\)-logos is a model of \(\modesketch\). Here, by a model of \(\modesketch\) we mean an \(\infty\)-logos that admits an interpretation of a postulated function \(\mode : \modesketch \to \ilLexAcc\) satisfying 1 2 and the following additional axiom.

3 roughly asserts that the whole universe \(\univ\) is reconstructed from the subuniverses \(\univ_{\mode(\idx)}\)’s. This is meant to exclude models other than intended models.

A generalization of the Artin gluing is oplax limits. In the setting of [exm:intended-model-mode-sketch-for-functors], \(\univ\) fits into the following universal oplax cone over the diagram \(\univ_{\mode(0)} \xleftarrow{\opModality^{\mode(1)}_{\mode(0)}} \univ_{\mode(1)}\). \[\labelX[diagram]{eq:gluing-as-oplax-limit} \begin{tikzcd} & \univ \arrow[dl, "\phantom{a}"{name = a0}] \arrow[dr, "\phantom{a}"'{name = a1}] \arrow[from = a0, to = a1, To] \\ \univ_{\mode(0)} & & \univ_{\mode(1)} \arrow[ll, "\opModality^{\mode(1)}_{\mode(0)}"] \end{tikzcd}\] An oplax cone over a diagram is a kind of cone but every triangle formed by two projections and a functor in the diagram is only filled by a not necessarily invertible natural transformation in the direction of [eq:gluing-as-oplax-limit]. The universal oplax cone or oplax limit is the terminal object in the \((\infty, 1)\)-category of oplax cones.

For a general mode sketch \(\modesketch\), we apply [prop:join-strongly-disjoint] for a minimal element \(\mode(\idx_{0})\) and the rest \(\biglor_{\idx : \modesketch \setminus \idx_{0}} \mode(\idx)\) and repeat this for \(\modesketch \setminus \idx_{0}\) to fracture types into modal types. [exm:intended-model-mode-sketch-for-functors,exm:intended-model-mode-sketch-for-trans] suggest that \(\univ\) is the oplax limit of the diagram formed by \(\univ_{\mode(\idx)}\)’s explained in [rem:2-cat-mode-sketch]. Thus, our intended models of \(\modesketch\) are oplax limits of \(\infty\)-logoses indexed over the \((\infty, 2)\)-category presented by \(\modesketch\). The formal account of this is described in 6.

4 Mode sketches and synthetic Tait computability↩︎

We give an alternative set of axioms for mode sketches and exhibit a connection between mode sketches and synthetic Tait computability of Sterling [19]. The core axiom of synthetic Tait computability is to postulate a proposition. The proposition induces the open and closed modalities, and then every type is fractured into an open type equipped with a closed type family and behaves like a logical relation. In this story, the open and closed modalities seem more essential than the postulated proposition, so we aim to formulate synthetic Tait computability purely in terms of modalities. We work in homotopy type theory.

4.1 Alternative mode sketch axioms↩︎

The \(\infty\)-logoses obtained by the Artin gluing can be characterized as \(\infty\)-logoses equipped with a subterminal object (cf. [38, p. A4.5.6]). We generalize this from the Artin gluing to oplax limits indexed by mode sketches, internally to type theory: the type of functions \(\modesketch \to \ilLexAcc\) satisfying 1 3 is equivalent to the type of lattice morphisms \(\ilCosieve(\modesketch) \to \ilProp\) ([thm:equiv-two-mode-sketch-axioms]).

Before giving a proof of [thm:equiv-two-mode-sketch-axioms], let us relate [thm:equiv-two-mode-sketch-axioms] to synthetic Tait computability [18], [19], [39]. The core axiom of synthetic Tait computability is to postulate some propositions. One can work with those propositions directly but also with the induced open and closed modalities. [thm:equiv-two-mode-sketch-axioms] says that synthetic Tait computability can, in fact, be formulated completely in terms of modalities. The simplest version of synthetic Tait computability postulates a single proposition. The corresponding mode sketch is \(\{0 \to 1\}\) as follows.

The rest of this subsection is devoted to the proof of [thm:equiv-two-mode-sketch-axioms]. We first show that 1 is restricted to a function $ .$

We prepare a couple of lemmas.

We then construct the inverse function $ .$ The key observation is that canonical joins of \(\mode(\idx)\)’s exist and are well-behaved under 1.

4.2 Logical relations as types↩︎

We have seen in 4.1 that synthetic Tait computability is reformulated in terms of . The slogan of synthetic Tait computability is “logical relations as types” [18]. This is also formulated purely in terms of .

[prop:fracture-and-gluing-alt] asserts that a type in \(\univ_{\mode \lor \modeI}\) is a \(\modeI\)-modal type equipped with a \(\mode\)-modal unary (proof-relevant) relation on it, so types (in \(\univ_{\mode \lor \modeI}\)) are relations. More generally, for a mode sketch \(\modesketch\) and a function \(\mode : \modesketch \to \ilLexAcc\) satisfying 1, types in \(\univ_{\biglor_{\modesketch}\mode}\) are fractured into a sort of generalized relations by iterated applications of [prop:fracture-and-gluing-alt]. Intuitively, the ordering on \(\modesketch\) is understood as “dependency”: every type \(\ty : \univ_{\biglor_{\modesketch} \mode}\) is fractured into a family of type families \(\{\ty_{\mode(\idx)}\}_{\idx : \modesketch}\) such that \(\ty_{\mode(\idx)}\) depends on \(\ty_{\mode(\idxI)}\) for all \(\idxI > \idx\). One may also regard the underlying finite poset of \(\modesketch\) as a FOLDS signature [40].

The equivalence in [prop:fracture-and-gluing-alt] nicely interacts with type constructors, and we derive the logical relation translation (also called the parametricity translation) of dependent type theory [11], [41]–[43] as a theorem in type theory. Let \(\mode\) and \(\modeI\) be such that \(\mode \le {}^{\orthMark}\modeI\). Type constructors in \(\univ_{\mode \lor \modeI}\) behave in the same way as the definition of the logical relation translation of type constructors [43, Sec. 3] as follows.

• \(\univ_{\mode \lor \modeI} : \enlarge \univ_{\mode \lor \modeI}\) corresponds to the pair $ ({}, . {});None$

• \(\ilUnit : \univ_{\mode \lor \modeI}\) corresponds to the pair $ (, . );None$

• Suppose that \(\ty : \univ_{\mode \lor \modeI}\) corresponds to a pair \((\ty_{\modeI}, \ty_{\mode})\). Then \((\ty \to \univ_{\mode \lor \modeI}) : \enlarge \univ_{\mode \lor \modeI}\) corresponds to the pair \[(\ty_{\modeI} \to \univ_{\modeI}, \ilAbs \tyI. \ilforall_{\var : \ty_{\modeI}}\ty_{\mode}(\var) \to \tyI(\var) \to \univ_{\mode}).\] Indeed,

  \[\begin{align} & \term{\ty \to \univ_{\mode \lor \modeI}} \\ \simeq& \by{fracture and gluing} \\ & \term{(\ilexists_{\var : \ty_{\modeI}}\ty_{\mode}(\var)) \to (\ilexists_{\tyI : \univ_{\modeI}}\tyI \to \univ_{\mode})} \\ \simeq& \by{\(\ilforall\) distributes over \(\ilexists\)} \\ & \term{\ilexists_{\tyI : \ilforall_{\var : \ty_{\modeI}}\ty_{\mode}(\var) \to \univ_{\modeI}}\ilforall_{\var}\ilforall_{\varI}\tyI(\var, \varI) \to \univ_{\mode}} \\ \simeq& \by{\(\univ_{\modeI} \simeq (\ty_{\mode}(\var) \to \univ_{\modeI})\) since \(\mode \le {}^{\orthMark}\modeI\)} \\ & \term{\ilexists_{\tyI : \ty_{\modeI} \to \univ_{\modeI}}\ilforall_{\var}\ty_{\mode}(\var) \to \tyI(\var) \to \univ_{\mode}}; \end{align}\]

• Suppose that \(\ty : \univ_{\mode \lor \modeI}\) corresponds to a pair \((\ty_{\modeI}, \ty_{\mode})\) and that \(\tyI : \ty \to \univ_{\mode \lor \modeI}\) corresponds to a pair \((\tyI_{\modeI}, \tyI_{\mode})\). Then \(\ilforall_{\var : \ty}\tyI(\var) : \univ_{\mode \lor \modeI}\) corresponds to the pair \[(\ilforall_{\var_{\modeI} : \ty_{\modeI}}\tyI_{\modeI}(\var_{\modeI}), \ilAbs \map. \ilforall_{\var_{\modeI}}\ilforall_{\var_{\mode} : \ty_{\mode}(\var_{\modeI})}\tyI_{\mode}(\var_{\modeI}, \var_{\mode}, \map(\var_{\modeI})))\] by a similar calculation to the previous clause. \(\ilexists_{\var : \ty}\tyI(\var) : \univ_{\mode \lor \modeI}\) corresponds to the pair \[(\ilexists_{\var_{\modeI} : \ty_{\modeI}}\tyI_{\modeI}(\var_{\modeI}), \ilAbs (\el_{\modeI}, \elI_{\modeI}). \ilexists_{\var_{\mode} : \ty_{\mode}(\el_{\modeI})}\tyI_{\mode}(\el_{\modeI}, \var_{\mode}, \elI_{\modeI}));\]

• Suppose that \(\ty : \univ_{\mode \lor \modeI}\) corresponds to a pair \((\ty_{\modeI}, \ty_{\mode})\), that \(\el : \ty\) corresponds to a pair \((\el_{\modeI}, \el_{\mode})\), and that \(\el' : \ty\) corresponds to a pair \((\el'_{\modeI}, \el'_{\mode})\). Then \(\el = \el' : \univ_{\mode \lor \modeI}\) corresponds to the pair \[(\el_{\modeI} = \el'_{\modeI}, \ilAbs \pth. \el_{\mode} =^{\ty_{\mode}}_{\pth} \el'_{\mode}).\]

Thus, any type \(\ty : \univ_{\mode \lor \modeI}\) constructed using these type constructors is fractured into a type \(\ty_{\modeI} : \univ_{\modeI}\) and a type family \(\ty_{\mode} : \ty_{\modeI} \to \univ_{\mode}\), and \(\ty_{\mode}\) is equivalent to the logical relation translation of \(\ty_{\modeI}\). In this sense, types in \(\univ_{\mode \lor \modeI}\) are logical relations. The interaction of the equivalences in [exm:fracture-span] [exm:fracture-0-1-2] and type constructors is similarly calculated. We thus conclude that types in \(\univ_{\biglor_{\modesketch} \mode}\) are generalized logical relations.

5 Higher category theory↩︎

We collect facts about higher categories needed to develop semantics of mode sketches in \(\infty\)-logoses.

We work with a model-independent language of \((\infty, 1)\)-category theory rather than choosing a specific model of \((\infty, 1)\)-categories. An \((\infty, 1)\)-category \(\cat\) consists of a space \(\Obj(\cat)\) of objects of \(\cat\), a space \(\Map_{\cat}(\obj, \objI)\) of morphisms from \(\obj\) to \(\objI\) for any objects \(\obj\) and \(\objI\), and composition operators unital and associative up to coherent homotopy. Concepts in category theory such as functors, natural transformations, equivalences, adjoints, (co)limits, and Kan extensions have \((\infty, 1)\)-categorical analogues. We refer the reader to [1], [44], [45] for general \((\infty, 1)\)-category theory.

At least two Grothendieck universes \(\setuniv \in \enlarge \setuniv\) are assumed to exist. By small we mean \(\setuniv\)-small and by large we mean \(\enlarge \setuniv\)-small. For an \((\infty,1)\)-category \(\cat\) of small objects of some kind, we write \(\enlarge \cat\) for the \((\infty,1)\)-category of large objects of the same kind. Let \(\Space\) denote the \((\infty, 1)\)-category of small spaces. Let \(\Cat\) denote the \((\infty, 1)\)-category of small \((\infty, 1)\)-categories. For \((\infty, 1)\)-categories \(\cat\) and \(\catI\), let \(\Fun(\cat, \catI)\) denote the \((\infty, 1)\)-category of functors from \(\cat\) to \(\catI\) and natural transformations between them. For a functor \(\obj : \idxsh \to \cat\), we write \(\{\proj_{\idx} : \lim_{\idxI \in \idxsh} \obj_{\idxI} \to \obj_{\idx}\}_{\idx \in \idxsh}\) for the limit cone if it exists and \(\{\inc_{\idx} : \obj_{\idx} \to \colim_{\idxI \in \idxsh} \obj_{\idxI}\}_{\idx \in \idxsh}\) for the colimit cocone if it exists.

Accessible and presentable \((\infty,1)\)-categories [1, Ch. 5] are important classes of \((\infty,1)\)-categories. We do not need precise definitions of them. Every presentable \((\infty,1)\)-category is accessible and has small colimits and limits.

5.1 \(\infty\)-logoses↩︎

We review the theory of \(\infty\)-logoses, also known as \(\infty\)-toposes. The standard reference is [1, Ch. 6].

The following are immediate from the definition.

in homotopy type theory are expected to correspond to (lex, accessible) localizations of \(\infty\)-logoses.

\((\infty, 1)\)-categorical counterparts of open and closed modalities are open and closed, respectively, localizations (1).

5.2 The language of \((\infty, 2)\)-category theory↩︎

We formulate concepts in \((\infty, 2)\)-category theory using the \((\infty, 1)\)-category \(\nPrefix{2}\Cat\) of \((\infty, 2)\)-categories axiomatized and proved to be equivalent to various models of \((\infty, 2)\)-categories by Barwick and Schommer-Pries [46].

Among Barwick and Schommer-Pries’s axioms, the following are important to us.

Let us fix terminology and notation.

1 is particularly useful and mostly used in the following form.

[cst:2-category-obj,cst:2-category-core,cst:2-category-dual] below are easily justified by using the 2-fold complete Segal spaces model [47].

The unicity theorem [46] Theorem 7.3 asserts that there are exactly \((\Integer/2 \Integer)^{2}\) automorphisms on \(\nPrefix{2}\Cat\). Those automorphisms are opposite constructions.

The following is an \((\infty, 2)\)-categorical version of the fact that a natural transformation is invertible if it is point-wise invertible. It is proved without using a specific model.

5.3 Scaled simplicial sets↩︎

We review one of models for \((\infty, 2)\)-categories, scaled simplicial sets [29]. This model is convenient for presenting \((\infty, 2)\)-categories by combinatorial data, provides computation of colimits of \((\infty, 2)\)-categories, and gives the \((\infty, 2)\)-category of \((\infty, 1)\)-categories a useful universal property.

A scaled simplicial set \(\sh\) is thought of as a presentation of an \((\infty, 2)\)-category: the \(0\)-cells are the \(0\)-simplices of \(\sh\); the \(1\)-cells are generated by \(1\)-simplices of \(\sh\); the \(2\)-cells are generated by \(2\)-simplices of \(\sh\) in the following direction; \[\begin{tikzcd} \el_{0} \arrow[rr, "\phantom{a}"'{name = a0}] \arrow[dr] & \arrow[from = a0, to = d, To, end anchor = {[yshift = 1ex]}] & \el_{2} \\ & \el_{1} \arrow[ur] \end{tikzcd}\] thin \(2\)-simplices are made invertible \(2\)-cells; higher simplices presents homotopies filling certain diagrams.

We can calculate colimits in \(\nPrefix{2}\Cat\) via homotopy colimits of scaled simplicial sets. We do not need much details, but a useful consequence is the following.

Lurie [29, Sec. 4.5] shows that the \((\infty, 2)\)-category of \((\infty, 1)\)-categories is presented by the scaled simplicial set classifying locally cocartesian fibrations.

The notion of locally cocartesian fibration is, however, specific to the scaled simplicial sets model. A more model-independent notion is as follows.

An object in \(\ptCat^{\nMark{2}, \rightMark}\) is a pair \((\cat, \obj)\) consisting of an \((\infty, 1)\)-category \(\cat\) and an object \(\obj \in \cat\). A morphism \((\cat, \obj) \to (\catI, \objI)\) in \(\ptCat^{\nMark{2}, \rightMark}\) is a pair \((\fun, \mor)\) consisting of a functor \(\fun : \cat \to \catI\) and a morphism \(\mor : \fun(\obj) \to \objI\). A \(2\)-morphism \((\fun, \mor) \To (\funI, \morI) : (\cat, \obj) \to (\catI, \objI)\) in \(\ptCat^{\nMark{2}, \rightMark}\) is a pair \((\trans, \pth)\) consisting of a natural transformation \(\trans : \fun \To \funI\) and a path \(\pth : \mor \sim \morI \comp \trans_{\obj}\).

For the purpose of 5.4, we introduce a variant of \(\ptCat^{\nMark{2}, \rightMark}\).

In other words, \(\ptCat^{\nMark{2}, \leftMark}\) is the fiberwise opposite of \(\ptCat^{\nMark{2}, \rightMark}\). Thus, the objects of \(\ptCat^{\nMark{2}, \leftMark}\) are the same as \(\ptCat^{\nMark{2}, \rightMark}\), but a morphism \((\cat, \obj) \to (\catI, \objI)\) in \(\ptCat^{\nMark{2}, \leftMark}\) is a pair \((\fun, \mor)\) consisting of a functor \(\fun : \cat \to \catI\) and a morphism \(\mor : \objI \to \fun(\obj)\).

5.4 Oplax limits↩︎

Oplax limits in general \((\infty, 2)\)-categories are defined by Gagna, Harpaz, and Lanari [28]. In this paper, we only need oplax limits of \((\infty, 1)\)-categories which have the following simple construction [28] Example 5.3.12.

Concretely, an object \(\obj\) in \(\opLaxLim_{\idx \in \idxsh} \cat_{\idx}\) consists of: an object \(\obj_{\idx} \in \cat_{\idx}\) for any object \(\idx \in \idxsh\); a morphism \(\obj_{\moridx} : \obj_{\idx} \to \cat_{\moridx}(\obj_{\idxI})\) for any morphism \(\moridx : \idx \to \idxI\) in \(\idxsh\); some coherence data. A morphism \(\mor : \obj \to \objI\) in \(\opLaxLim_{\idx \in \idxsh} \cat_{\idx}\) consists of: a morphism \(\mor_{\idx} : \obj_{\idx} \to \objI_{\idx}\) for any object \(\idx \in \idxsh\); a homotopy \(\mor_{\moridx}\) filling the square \[\begin{tikzcd} \obj_{\idx} \arrow[r, "\mor_{\idx}"] \arrow[d, "\obj_{\moridx}"'] & [4ex] \objI_{\idx} \arrow[d, "\objI_{\moridx}"] \\ \cat_{\moridx}(\obj_{\idxI}) \arrow[r, "\cat_{\moridx}(\mor_{\idxI})"'] & \cat_{\moridx}(\objI_{\idxI}) \end{tikzcd}\] for any morphism \(\moridx : \idx \to \idxI\) in \(\idxsh\); some coherence data.

We show that \(\infty\)-logoses are closed under oplax limits. For this, we consider a weaker notion of morphism of \(\infty\)-logoses.

The rest of this subsection is devoted to the proof of [prop:logos-accessible-oplax-limit].

5.5 Oplax natural transformations↩︎

An alternative description of oplax limits is that they are \((\infty, 1)\)-categories of oplax natural transformations ([prop:oplax-limit-universal-property]).

Lax natural transformations correspond to functors between \(1\)-cocartesian \(2\)-right fibrations.

[prop:lax-univalence] follows from the following special cases which are already known.

A dual argument shows the following.

Natural transformations correspond to functors preserving cocartesian morphisms.

Oplax limits are \((\infty, 1)\)-categories of oplax natural transformations in the following sense.

A useful source of oplax natural transformations is the following mate correspondence whose special case when \(\cat\) is an \((\infty, 1)\)-category is shown by Haugseng et al. [30] Corollary F in a stronger form of an equivalence between \((\infty, 1)\)-categories of (op)lax natural transformations.

6 Semantics of mode sketches↩︎

We show that models of a mode sketch \(\modesketch\) are equivalent to diagrams of \(\infty\)-logoses indexed over \(\modesketch\).

The rest of this section is devoted to the proof of [thm:main-theorem]. In 6.1, we give a construction of a model of \(\modesketch\) from a functor \(\realize{\modesketch}^{\opMark(1, 2)} \to \Logos^{\nMark{2}}_{\LexAccMark}\). In 6.2, we give an inverse construction.

6.1 Models of mode sketches in oplax limits↩︎

We first show that the oplax limit of a functor \(\realize{\modesketch}^{\opMark(1, 2)} \to \Logos_{\LexAccMark}^{\nMark{2}}\) is part of a model of \(\modesketch\). We fix a functor \(\logosI : \realize{\modesketch}^{\opMark(1, 2)} \to \Logos^{\nMark{2}}_{\LexAccMark}\).

[thm:intended-model-mode-sketch] breaks into three parts ([thm:intended-model-mode-sketch-c] [thm:intended-model-mode-sketch-a] [thm:intended-model-mode-sketch-b]). [axm:model-top] is immediate from the construction.

For [axm:model-disjoint] [axm:model-invertible], we calculate \(\opModality^{\mymode_{\logosI}(\idx)}_{\mymode_{\logosI}(\idxI)}\) and \(\unitModality^{\mymode_{\logosI}(\idxII); \mymode_{\logosI}(\idx)}_{\mymode_{\logosI}(\idxI)}\).

6.2 Fracture and gluing↩︎

We show that any model of a mode sketch \(\modesketch\) induces a functor \(\realize{\modesketch}^{\opMark(1, 2)} \to \Logos^{\nMark{2}}_{\LexAccMark}\) and that this gives an inverse of the construction given in 6.1. This is an externalization and generalization of the fracture and gluing theorem ([prop:join-strongly-disjoint]).

We have constructed back and forth constructions between the \((\infty,1)\)-category of models of \(\modesketch\) and the \((\infty,1)\)-category of functors \(\realize{\modesketch}^{\opMark(1, 2)} \to \Logos^{\nMark{2}}_{\LexAccMark}\). We turn these constructions into an adjunction (1) and then show that its unit and counit are invertible ([thm:fracture-gluing] [thm:gluing-fracture]).

Acknowledgements↩︎

The author thanks Jonathan Sterling for useful conversations on the current work. The author was supported by KAW Grant “Type Theory for Mathematics and Computer Science” investigated by Thierry Coquand and Peter LeFanu Lumsdaine.

References↩︎