1 Introduction↩︎

1.1 Context and motivation↩︎

Fields, Hilbert spaces, and other set-based mathematical structures can be studied uniformly not only via category theory or mathematical logic, but also via a combination thereof, known as categorical logic, founded by Lawvere [1]. Categorical logic is based on three key ideas: first, logical theories can be identified with certain categories (via the construction of syntactic categories, for example); secondly, set-theoretic models of a theory can be regarded as structure-preserving functors into the category of sets; and, finally, categories of models can often be characterised in a purely categorical, syntax-free, way. For example, algebraic theories are identified with categories with finite products, their models are regarded as product-preserving functors into the category of sets, and their categories of models are characterised as algebraic varieties [2]. This point of view offers a powerful interplay of ideas. For example, categorical embedding theorems (such as the embedding theorem for regular categories [3]) are closely related to logical completeness theorems, reconstruction theorems (as in the theory of ultracategories [4], [5]) allow us to recover a theory from its category of models, and adjoint functor theorems (as available for locally presentable categories [6]) enable us to establish the existence of free models. In this context, accessible categories occupy a prominent role [7] since they are exactly the categories of set-based structures axiomatisable in (infinitary) first-order logic. For example, the categories of fields and of Hilbert spaces are accessible.

Motivation from several directions, including the research programme of categorification in algebra, the theory of stacks in algebraic geometry, and the semantics of programming language in theoretical computer science, leads naturally to the study of category-based, rather than set-based, structures, such as categories with additional structure or properties (e.g. monoidal categories or categories with finite limits). Additional complications and subtleties arise immediately. First, these structures assemble themselves most naturally into 2-categories, in which one has structure-preserving functors as morphisms, and appropriate natural transformations as 2-cells. Secondly, the morphisms of primary interest are those that preserve the structure only up to coherent isomorphism, not strictly (as this occurs rarely in practice). The theory of 2-categories developed over the last fifty years, most notably by the Australian school, provides an extensive analysis of categories with structure (see [8]–[10] for example). Part of the challenge of the subject is to work as strictly as possible, so as to exploit \(\mathsf{Cat}\)-enriched category theory and avoid the complex coherence considerations typical of the fully weak, bicategorical, setting, while retaining sufficient generality, which is often achieved via the proof of suitable strictification results [11]. In this context, the class of 2-categorical limits know as flexible limits [12] is of particular importance, for example because they can be understood as the homotopically well-behaved ones [13]. In recent years, there has also been significant interest and progress in developing a counterpart of the theory of accessible categories in the 2-dimensional setting [14]–[17].

Yet, some important questions remain open, for example regarding whether some 2-categories of interest in categorical logic and categorical algebra are accessible 2-categories with flexible limits or concerning the existence of free categories with various kinds of structure. The motivation for this paper was to solve some of these open questions. For this, we develop some aspects of categorical logic in the 2-categorical setting, building on earlier work of the second-named author and Rosický on an enriched version of categorical logic [18], [19].

The problems that we tackle can be readily understood in an example. Let us consider the 2-category \(\mathsf{Lex}\) of categories with finite limits, functors that preserve finite limits, and natural transformations. Here, by a category with finite limits we mean a category with the property that every finite diagram has a limit. Accordingly, by a finite limit-preserving functor we mean a functor that sends a finite limit diagram to a finite limit diagram. This is in contrast with categories with chosen finite limits and functors that preserve (up to canonical isomorphism) the chosen finite limits, which give rise to a 2-category, written \(\mathsf{Lex}_c\) here (where the subscript abbreviates ‘chosen’). The 2-category \(\mathsf{Lex}_c\) can be understood with 2-dimensional monad theory [8]. Indeed, there is a 2-monad \(T \colon \mathsf{Cat}\to \mathsf{Cat}\) such that the associated 2-category \(T\text{-}\mathsf{Alg}\) of strict algebras, pseudomorphisms and algebra 2-cells is \(\mathsf{Lex}_c\). The fact that limits exist up to unique isomorphism is then characterised by saying that the 2-monad \(T\) is a lax idempotent [20], or property-like [21]. With this results in place, one can establish various 2-categorical completeness and cocompleteness properties of \(\mathsf{Lex}_c\), which can be transferred to \(\mathsf{Lex}\) since the 2-functor \(U \colon\mathsf{Lex}_c \to \mathsf{Lex}\) forgetting the choice of limits is a 2-equivalence.

Pushing further this line of research, and building on earlier work by Makkai [22], [23], Bourke has recently shown that \(\mathsf{Lex}\) and related 2-categories, such as the 2-category \(\mathsf{Reg}\) of regular categories and the 2-category \(\mathsf{GFib}\) of Grothendieck fibrations, are accessible 2-categories with filtered colimits and flexible limits, finite flexible limits commuting with filtered colimits, and accesible retract equivalences [14]. Importantly, some of these examples go beyond the theory covered by 2-dimensional monad theory, since the categories of interest are not necessarily 2-monadic (or pseudo-monadic). Yet, the approach of [14] - which is somehow inspired by the theory of sketches - does not seem to be easily applicable to other 2-categories of interest, such as some of importance in categorical algebra, such as the 2-categories of Mal’cev, protomodular, and semiabelian categories, and categorical logic, such as the 2-categories of comprehension categories and of clans¹. In a different vein, taking a fully bicategorical approach, Di Liberti and Osmond have shown that \(\mathsf{Lex}\) is locally finitely bipresentable in a sense defined in [15]. Apart from the complex coherence conditions involved in the fully bicategorical point, this approach leads to bicategorical accessibility and completeness.

1.2 Main results↩︎

Here, we develop and apply an alternative approach. Our starting point is the observation that the definition of categories with finite limits involves axioms asserting the existence of some structure that is unique, up to unique isomorphism, when it exists. This form of quantification is somehow between unique existence (which is part of so-called finite limit theories) and ordinary existence (which is part of so-called regular theories) and hence has no counterpart in the 1-categorical setting.

We therefore introduce what we call isoregular theories, which are logical theories in which one can express this form of essentially unique existential quantification. We then introduce the notions of a model of an isoregular theory (now taking values in \(\mathsf{Cat}\) rather than \(\mathsf{Set})\) and prove 2-categorical counterparts of key results of categorical logic. First, we develop a functorial semantics for isoregular theories. This is done by isolating the fundamental properties of the syntactic 2-category \(\mathsf{Syn}({\mathbb{T}})\) of an isoregular theory \({\mathbb{T}}\), which we do introducing the notion of an isoregular 2-category (2). Then, we show (37) that models of \({\mathbb{T}}\) are the same thing as 2-functors \(M \colon\mathsf{Syn}({\mathbb{T}}) \to \mathsf{Cat}\) preserving the isoregular structure. With this in place, we prove that the 2-category of models of an isoregular theory is accessible with flexible limits and that the forgetful 2-functor to \(\mathsf{Cat}\) has a left biadjoint (41), therefore ensuring the existence of free models.

We then obtain several applications in a uniform manner. In particular, we obtain new proofs that \(\mathsf{Lex}\), \(\mathsf{Reg}\), \(\mathsf{GFib}\) are accessible with flexible limits, subsuming the core of Bourke’s results in [14]. Building on this, we show that the 2-categories \(\mathsf{Mal}\), \(\mathsf{Ptm}\), \(\mathsf{SmAb}\) of Malt’sev, protomodular and semiabelian categories (47 48 50), as well as the 2-categories \(\mathsf{Cmp}\) and \(\mathsf{Clan}\) of comprehension categories and clans (53 55), are accessible with flexible limits, which does not seem to be known. Additionally, a variety of forgetful functors are shown to admit left biadjoints, therefore establishing a number of new free constructions. In particular, we obtain a new proof of the existence of Joyal’s finite free bicompletions (45).

These results are a mere sample of the range of possible applications: as discussed in 6, the methods introduced here apply to several other 2-categories of interest, including those of pretoposes, multicategories, left adjoint functors, etc.

1.3 Technical aspects↩︎

We conclude this introduction with some comments on the more technical aspects of the paper.

First, when it comes to the formulation of the syntax of isoregular theories we combine ideas of enriched categorical logic [18], [19] and of type theory [25]. Isoregular theories have rules for forming terms, rules for forming propositions, and rules for logical entailment, corresponding to three forms of judgements: \[s \colon X \mathrlap{,} \qquad A \colon\mathsf{prop}\mathrlap{,} \qquad A_1, \ldots, A_n \colon A \mathrlap{.}\] These express that \(s\) is a well-formed term, that \(A\) is a well-formed proposition, that that \(A_1, \ldots, A_n\) entail \(A\), respectively, as in logic-enriched type theories [26]. In this setting, we can write a deduction rule asserting that, in order to be able to form existential quantification of the form \((\exists y \colon Y) B(x,y)\) only when, for \(x \colon X\), there exists at most a unique, up to unique isomorphism, \(y \colon Y\) such that \(B(x,y)\) holds. Thus, the formation rules for propositions depend on the deduction rules for logical entailment. This is in contrast with first-order logic, where one first defines the set of well-formed formulas and then, separately, defines the set of theorems of a theory by giving the deduction rules for logical entailment. It also differs from the approach in [27], as we avoid introducing 2-dimensional regular theories and carving out isoregular theories out of them. Building on [18], [19], it will also be essential to have at our disposal propositions of the form \(A^{[1]}\), where \(A\) is a proposition, which enable us to express properties of morphisms, rather than just objects, in the intended models. We do not make use of dependent sorts, so as to be able to build directly on [18], [19] and remain close to the presentation of [27], and leave this as a possible direction for future work.

When it comes to characterising the 2-categorical structure of the syntactic categories of isoregular theories, our notion of an isoregular 2-category (2) appears rather natural. Just as a regular 1-category is a 1-category with finite limits in which every kernel pair has a coequaliser and regular epimorphisms are stable under pullback, an isoregular 2-category is a 2-category with finite 2-limits in which every fully faithful kernel pair has a coequaliser and fully faithful regular epimorphisms are stable under pullback. In particular, isoregular 2-categories are ff-regular 2-categories in the sense of [28] (see 4 for details).

Just as in a regular category every morphism can be factored as a regular epimorphism followed by a monomorphism, in an isoregular 2-category every morphism with a fully faithful kernel pair can be factored as a fully faithful regular epimorphism followed by a monomorphism, which gives us exactly what is needed in order to characterise existence up to unique isomorphism. Indeed, morphisms with a fully faithful kernel pair admit several equivalent characterisations, including that of being the morphisms that are faithful and whose fibers are subcontractible (5), an aspect that brings out the connection with the notion of a homotopy proposition of Univalent Foundations and Homotopy Type Theory, as we discuss in 14. The factorisation of such morphisms then amounts to being able to existentially quantify over these fibers. Indeed, in the syntactic 2-category of an isoregular theory, the composite \[\begin{tikzcd} \{ x \colon X, y \colon Y \;| \;B(x,y) \} \ar[r, >->] & X \times Y \ar[r] & X \end{tikzcd}\] has a fully faithful kernel if and only if it is provable that it is faithful and, for \(x \colon X\), there exists at most a unique, up to unique isomorphism, \(y \colon Y\) such that \(B(x,y)\) holds. Existential quantification then corresponds to the factorisation \[\begin{tikzcd}[column sep = large] & \{ x \colon X \;| \;(\exists y \colon Y) B(x,y) \} \ar[dr, >->] & \\ \{ x \colon X, y \colon Y \;| \;B(x,y) \} \ar[ur, ->>] \ar[r, >->] & X \times Y \ar[r] & X \mathrlap{.} \end{tikzcd}\]

In order to prove that models of isoregular theories are accessible 2-categories with flexible limits, we first provide a functorial semantics (37), describing models as what we call isoregular functors, i.e. 2-functors preserving the structure of an isoregular 2-category: \[\mathsf{Mod}({\mathbb{T}})\;\cong \mathsf{IsoReg}[\mathsf{Syn}({\mathbb{T}}),\mathsf{Cat}] \mathrlap{,}\] and then, separately, establish that 2-categories of isoregular 2-functors are accessible with flexible limits (41), a result that provides additional evidence for the usefulness of the notion of an isoregular 2-category. Clearly, working in the 2-categorical (rather than bicategorical) setting offers significant simplifications throughout the development of the theory and does not prevent the intended applications.

1.4 Outline of the paper↩︎

2 introduces isoregular 2-categories and establishes some of their properties, including various equivalent characterisations of morphisms with fully faithful kernel. 3 introduces syntax and semantics of isoregular theories, including the soundness theorem. 4 establishes the functorial semantics for isoregular theories, by introducing syntactic 2-categories. Using the functorial semantics, 5 establishes the accessibility of models of isoregular theories. We conclude the paper in 6 with applications.

Acknowledgements.↩︎

Nicola Gambino is grateful to the Department of Mathematics and the School of Natural Sciences of The University of Manchester for granting sabbatical leave, during which this paper was written. Giacomo Tendas acknowledges with gratitude the support of the EPSRC postdoctoral fellowship via grant EP/X027139/1. We thank John Bourke, Richard Garner, Vít Jelínek, Marino Gran, and Jiří Rosický for helpful conversations.

2 Isoregular 2-categories↩︎

2.1 Preliminaries↩︎

We assume that the readers are familiar with the theory of 2-categories and confine ourselves to fix some notation and terminology. See [11] for the basics, [29] for 2-categorical limits in general and [12] for flexible 2-limits. Our development will focus on cartesian 2-categories, i.e. 2-categories with all finite 2-categorical limits, including a terminal object, products, pullbacks, equalisers.

We write \(\mathsf{Cat}\) for the 2-category of small categories, functors and natural transformations. For a 2-category \({\mathcal{K}}\), we write \({\mathcal{K}}(A,B)\) for the hom-category of morphisms from \(A\) to \(B\) and 2-cells between them. The composite of \(f \colon A \to B\) and \(g \colon B \to C\) will be denoted \(g \circ f\) or simply \(gf\). Similar conventions are adopted for composition of morphisms and 2-cells. We write \({\mathcal{K}}_0\) for the underlying 1-category of \({\mathcal{K}}\).

Let \({\mathcal{K}}\) be a 2-category. The power of an object \(A \in K\) by a small category \(\,\mathbb{c}\) is an object \(A^{\,\mathbb{c}} \in {\mathcal{K}}\) together with a functor, called evaluation, \(\mathrm{ev}_{\,\mathbb{c}} \colon{\,\mathbb{c}} \to {\mathcal{K}}(A^{\,\mathbb{c}}, A)\) which is universal, in the sense that for every \(X \in {\mathcal{K}}\), the induced functor \[{\mathcal{K}}(X, A^{\,\mathbb{c}}) \to {\mathcal{K}}(X,A)^{\,\mathbb{c}}\] is an isomorphism of categories. When \({\mathcal{K}}\) has powers by a small category \(\,\mathbb{c}\), these determine a 2-functor \((-)^{\,\mathbb{c}} \colon{\mathcal{K}}\to {\mathcal{K}}\). In the following, we shall be primarily interested in powers by finitely presentable categories. For a natural number \(n\), we write \([n]\) for the nerve of the poset \(0 < 1 \ldots < n\). In particular, \([1]\) is the category with two objects (\(0\) and \(1\)) and a single non-identity map (from \(0\) to \(1\)). In this case, the evaluation functor determines two maps \(\pi_0 \colon A^{[1]} \to A\), \(\pi_1 \colon A^{[1]} \to A\). When \({\mathcal{K}}\) has binary products, we write \(\pi_A \colon A^{[1]} \to A \times A\) for their pairing, i.e. \(\pi_A \equiv_{\mathrm{def}}(\pi_0, \pi_1)\).

Since we will not generally assume the ambient 2-category \({\mathcal{K}}\) to have all powers and copowers, the 2-dimensional universal property of a conical 2-limit in \({\mathcal{K}}\) will have to be checked explicitly, rather than inferred from its 1-dimensional one in \({\mathcal{K}}_0\). However, we have the following observation.

For an object \(X \in {\mathcal{K}}\), we write \({\mathcal{K}}(X, -) \colon{\mathcal{K}}\to \mathsf{Cat}\) for the induced representable 2-functor. These 2-functors allow us to extend to a general 2-category \({\mathcal{K}}\) many concepts that can be defined in \(\mathsf{Cat}\). For example, a morphism \(f\colon A\to B\) in \({\mathcal{K}}\) is called full if, for every \(X\in{\mathcal{K}}\), the functor \[\label{equ:representable-applied-to-f} {\mathcal{K}}(X,f)\colon {\mathcal{K}}(X,A)\to{\mathcal{K}}(X,B)\tag{1}\] is full. When the fullness condition is restricted to 2-cells in the codomain that are isomorphisms or equalities, we say that \(f\) is full on isomorphisms or full on identities, respectively. Explicitly, for \(f\) to be full on identities means that, given \(a \colon X \to A\) and \(a' \colon X \to A\), if \(fa = fa'\) there exists a 2-cell \(\alpha \colon a \Rightarrow a'\) such that \(f \alpha = 1_{fa}\). The notions of a faithful and a fully faithful morphism are defined analogously. Note that, if \(f\) is faithful and full on identities, then the 2-cell \(\alpha\) above is unique and an isomorphism.

If \({\mathcal{K}}\) has powers by \([1]\), \(f\) is fully faithful if and only if the following square is a pullback: \[\begin{tikzcd} A^{[1]} \ar[r, "f^{[1]}"] \ar[d, "\pi_A"'] & B^{[1]} \ar[d, "\pi_B"] \\ A \times A \ar[r, "f \times f"'] & B \times B \mathrlap{.} \end{tikzcd}\] In a 2-category \({\mathcal{K}}\) a morphism is said to be a monomorphism if it is representably so. Hence, every monomorphism is faithful. A morphism is a regular epimorphism if it is a coequalizer (in the 2-categorical sense) of a parallel pair of maps. If \({\mathcal{K}}\) has finite limits, a morphism is a monomorphism (a regular epimorphism) if and only if it is a monomorphism (a regular epimorphism, respectively) in the underlying category \({\mathcal{K}}_0\).

2.2 Isoregular 2-categories↩︎

Let \({\mathcal{K}}\) be a 2-category with finite 2-limits, to remain fixed for the rest of this section. Let \(f \colon A \to B\) be a morphism in \({\mathcal{K}}\). Recall that the kernel pair of \(f\) is the pullback \[\begin{tikzcd} \Delta_f \ar[d, "\pi_1"'] \ar[r, "\pi_2"] & A \ar[d, "f"] \\ A \ar[r, "f"'] & B \mathrlap{.} \end{tikzcd}\]

When the equivalent conditions of 1 hold, we say that \(f\) has a fully faithful kernel pair. In the 2-category \(\mathsf{Cat}\) of small categories, if a functor \(f \colon A \to B\) has a fully faithful kernel pair, then its coequaliser is again fully faithful and therefore is a fully faithful regular epimorphism. The essential properties of this situation are axiomatised in the notion of an isoregular 2-category, which we introduce next.

Morphisms with a fully faithful kernel pair, or ffk-morphisms for short, are fundamental for the definition of an isoregular 2-category and therefore it is useful to have some equivalent characterisations of them. We provide these in [fact-morph] below, but for this we need a definition and a preliminary lemma. In analogy with the definition of a subterminal object in a 1-category, we define a object \(C\) of a 2-category \({\mathcal{K}}\) to be subcontractible if for every \(X \in {\mathcal{K}}\) and \(f, g \colon X \to C\), there exists a unique (and hence necessarily invertible) \(\alpha \colon f \Rightarrow g\). Equivalently, for every \(X \in {\mathcal{K}}\), the category \({\mathcal{K}}(X,C)\) is either empty or contractible. In \(\mathsf{Cat}\), a subcontractible object is a category that is either empty or contractible. For example, consider a category \(D\) and define \(C\) to be the full subcategory of \(D\) spanned by the terminal objects of \(D\). Then \(C\) is subcontractible.

ffk-morphisms are not closed under composition. For example, let us work in \(\mathsf{Cat}\) and consider the composite functor \[\begin{tikzcd} \{0\} + \{1 \} \ar[r, "F"] & J \ar[r] & \{ \ast \} \mathrlap{,} \end{tikzcd}\] where \(J\) is the category with two objects and an isomorphism between them and the functor \(F\) is the inclusion of the endpoints. The composite is not an ffk-morphism, even if each of the composites. This fact could be understood recalling that, by part (vi) of 5, being an ffk-morphism involves a property of the fibers, which is not necessarily preserved by composition. However, the following closure properties with respect to fully faithful morphisms and monomorphisms hold.

Next, we give an example of an ffk-morphism that is neither fully faithful nor a monomorphism.

In a regular 1-category, every morphism can be factored as a regular epimorphism followed by a monomorphism. As 11 shows, in an isoregular 2-category, every ffk-morphism can be factored as a fully faithful regular epimorphism followed by a monomorphism. The factorisation can be understood as turning a ffk-morphism, whose fibers are subcontractible, into a monomorphism, whose fibers are subterminal (cf.14 for additional comments on this point). The proof is essentially the same as the one of the corresponding statement for regular 1-categories.

Let \({\mathcal{K}}\) and \({\mathcal{L}}\) be isoregular 2-categories. A 2-functor \(F \colon{\mathcal{K}}\to {\mathcal{L}}\) is said to be isoregular if it preserves finite 2-limits and coequalisers of fully faithful kernel pairs; equivalently, if it preserves finite limits and fully faithful regular epimorphisms. We write \(\mathsf{IsoReg}({\mathcal{C}},{\mathcal{K}})\) for the full sub-2-category of the functor 2-category \([{\mathcal{K}}, {\mathcal{L}}]\) spanned by isoregular 2-functors.

3 Isoregular theories: syntax and semantics↩︎

3.1 Languages↩︎

We follow the approach of [18], [19]. Languages are multi-sorted with arities being objects in the full sub-2-category of \(\mathsf{Cat}\) spanned by the finitely presentable categories, which we write \(\mathsf{Cat}_{\mathrm{fp}}\).

Let \({\mathbb{L}}\) be a finitary language as above. A sort is an expression of the form \(S^{\,\mathbb{c}}\) where \(S\) is a basic sort and \(\,\mathbb{c}\) is an arity. When \({\,\mathbb{c} } = [0]\), we write \(S\) instead of \(S^{[0]}\). If \(X = S^{\,\mathbb{c}}\) is a sort and \(\,\mathbb{d}\) is an arity, we define \[X^{\,\mathbb{d}} \equiv_{\mathrm{def}}S^{\,\mathbb{d} \times \,\mathbb{c}} \mathrlap{.}\]

A context is a sequence of variable declarations of the form \((\bar{x} \colon\bar{X}) = (x_1 \colon X_1, \ldots, x_n \colon X_n)\). For such a context, we define \[(\bar{x} \colon\bar{X})^{\,\mathbb{c}} \equiv_{\mathrm{def}}(u_1 \colon X_1^{\,\mathbb{c}}, \ldots, u_n \colon X_n^{\,\mathbb{c}}) \mathrlap{.}\] Here, the relabelling of variables has been made to improve readability, rather than for any essential reason. The deductive calculus for isoregular theories has three forms of judgement: \[\begin{gather} (\bar{x} \colon\bar{X}) \quad s \colon X \mathrlap{,} \tag{2} \\ (\bar{x} \colon\bar{X}) \quad A \colon\mathsf{prop} \mathrlap{,} \tag{3} \\ (\bar{x} \colon\bar{X}) \quad A_1, \ldots, A_m \vdash A \mathrlap{.} \tag{4} \end{gather}\] The judgements in 2 and 3 express that, relative to the variable declarations in the context, the expression \(s\) is a term of sort \(X\) and the expression \(A\) is a proposition, respectively. The judgement in 4 expresses that, relative to the variable declarations in the context and under the assumptions of the propositions \(A_1, \ldots, A_n\), the proposition \(A\) is true.

The notation introduced above will be simplified in many cases. When \(m = 0\), we write the judgement in 4 as \[(\bar{x} \colon\bar{X}) \; A\] and we do not mention the context when it is empty. The deduction rules of our calculus have the form \[\begin{prooftree} \mathcal{J}_1 \qquad \ldots \qquad \mathcal{J}_n \justifies \mathcal{J} \mathrlap{,} \end{prooftree}\] where \(\mathcal{J}_1\), …\(\mathcal{J}_m\), \(\mathcal{J}\) are judgements of one of the forms above. When \(n = 0\), we do not include the horizontal line. When stating rules, we do not mention a context that is common to all premisses and conclusions unless this causes confusion.

The deduction rules regarding terms are presented in ¿tbl:tab:terms?, making use of the conventions just introduced, and follow essentially [19]. Here, substitution is a primitive operation, rather than being defined by induction on terms, as this aligns well with our semantics of terms (cf.3.3). As we shall see, a judgement of the form \((\bar{x} \colon\bar{X}) \;t \colon Y\) will be interpreted in an isoregular 2-category as a morphism \(\llbracket{t}\rrbracket \colon\llbracket{\bar{X}}\rrbracket \to \llbracket{Y}\rrbracket\).

In the example below we will apply the restriction rule, taken along a functor \(f\colon\,\mathbb{d}\to\,\mathbb{c}\), to terms of the form \((\bar{x} \colon\bar{X}) \;s \colon X^{\,\mathbb{c}}\) where \(X\) may not be a basic sort as in [tbl:rule:restriction-def]. This should be understood as taking the restriction along \(f\times 1_{\,\mathbb{b}}\) where \(\,\mathbb{b}\in\mathsf{Cat}_{\mathrm{fp}}\) is such that \(X=S^{\,\mathbb{b}}\).

3.2 Isoregular theories↩︎

Let \({\mathbb{L}}\) be a fixed finitary language. The propositions of the calculus have the following six forms \[\top \mathrlap{,} \qquad R(s_1, \ldots, s_n) \mathrlap{,} \qquad s = t \mathrlap{,} \qquad A \land B \mathrlap{,} \qquad (\exists x \colon X) A \mathrlap{,} \qquad A^{[1]} \mathrlap{.}\] The first five forms of propositions are familiar from first-order logic, while the sixth is specific to our setting. For a proposition \(A\), we refer to \(A^{[1]}\) as the power of \(A\). Informally speaking, if a proposition \(A\) expresses properties of the objects of a category, the proposition \(A^{[1]}\) expresses properties of its morphisms. The deduction rules for isoregular logic are presented in three groups:

• rules for the formation of terms, in ¿tbl:tab:terms?,

• rules for the formation of propositions, in ¿tbl:tab:props?,

• rules for logical entailment, in 8.

One distinguishing aspect of this set of rules is that the deduction rules for forming new propositions depend on the deduction rules regarding logical entailment and viceversa. This is in contrast with first-order logic, where one first defines the set of well-formed formulas and then, separately, defines the set of theorems of a theory by giving the deduction rules for logical entailment, but is quite a natural adaptation of ideas from dependent type theory, where formation rules for types (which often can be seen as propositions, according to the propositions-as-types idea) can have premisses involving inhabitation of other types (which can be seen as derivability of propositions).

Let us explain the rules for formation of existentially quantified propositions, which allow us to form existential quantifiers only on propositions (provably) of a suitable kind. There are two such rules, given in [tbl:equ:exists-formation-mono] and [tbl:equ:exists-formation-eqfib], corresponding to ‘there exists a unique’ and ‘there exists a unique up to unique isomorphism’, respectively. The premiss \((x \colon X, y \colon Y) \;B(x,y) \colon\mathsf{prop}\) of these rules can be thought informally as giving rise to a morphism \[\label{equ:eqfib-informal} \{ x \colon X, y \colon Y \;| \;B(x,y) \} \rightarrowtail X \times Y \xrightarrow{ \pi_1} X \mathrlap{.}\tag{5}\] In [tbl:equ:exists-formation-mono], the judgement \(\mathcal{J}_{\textsf{mono}}(B)\) expresses that, for \(x \colon X\), there exists at most one \(y \colon Y\) such that \(B(x,y)\) holds, i.e. asserting that the morphism in 5 is a monomorphism. In [tbl:equ:exists-formation-eqfib], the judgements \(\mathcal{J}_{\textsf{faithful}}(B)\) and \(\mathcal{J}_{\textsf{full\text{-}id}}(B)\) express that, for \(x \colon X\), there exists at most one up to unique isomorphism \(y \colon Y\) such that \(B(x,y)\) holds, by asserting that the morphism in 5 is faithful and full on identities, and therefore an ffk-morphism by 5. Note that, using the rule in [equ:exists-formation-mono], the judgement \(\mathcal{J}_{\textsf{faithful}}(B)\) implies that the existential quantifier in \(\mathcal{J}_{\textsf{full\text{-}id}}(B)\) can actually be formed.

The deduction rule logical entailment for conjunction and existential quantification are the standard introduction and elimination rules, except that we need to include the so-called Frobenius rule (3), which ensures a good behaviour of the existential quantifier in contexts where implication is not part of the logical calculus. Note that, whenever an existential statement occurs in the conclusion of a deduction rule, the premisses ensure that, by the rules in [equ:exists-formation-mono] and [equ:exists-formation-eqfib] the existential quantifier can be formed. The other deduction rules for logical entailment express important properties of the intended models. For example, for a coequaliser of finite categories, \[\begin{tikzcd} \,\mathbb{a} \ar[r, shift left = 1, "f"] \ar[r, shift right = 1, "g"'] & \,\mathbb{c} \ar[r, "q"] & \,\mathbb{c} \mathrlap{,} \end{tikzcd}\] we have the deduction rule \[\begin{prooftree} s \colon S^{\,\mathbb{b}} \quad s \cdot f = s \cdot g \justifies (\exists x \colon S^{\,\mathbb{c}}) \big( x \cdot q = s \big) \mathrlap{.} \end{prooftree}\] Here, the existential quantifier can be formed according to our rules above since the judgement \[(x, x' \colon S^{\,\mathbb{c}}) \quad x \cdot q = s, x' \cdot q = s \vdash x = x'\] is provable using 6, as \(q\) is an epimorphism. The rules for powers of terms and propositions express functoriality of the operation of raising terms and propositions to a power and the preservation of conjunction and existential quantifiers by forming the power of a proposition.

3.3 Semantics↩︎

We shall be interested in interpreting formulas of these forms in an isoregular 2-category with a structure for \({\mathbb{L}}\). Importantly, not every raw proposition will admit an interpretation. Instead, we define simultaneously when a proposition is interpretable and, in that case, what its interpretation is. More precisely, if \(A\) is a proposition with free variables in the context \((x_1 \colon S_1^{\,\mathbb{c}_1},\ldots, x_n \colon S_n^{\,\mathbb{c}_n})\), we define when \(A\) is interpretable over \(L\) and, in that case, its interpretation as a subobject \[\llbracket{A}\rrbracket\rightarrowtail \llbracket{S_1}\rrbracket^{\,\mathbb{c}_1}\times\cdots\times \llbracket{S_n}\rrbracket^{\,\mathbb{c}_n}\] by recursion on the structure of the formula.

Below, we shall drop the subscript in the interpretation of sorts, function symbols and relation symbols whenever this does not cause confusion.

Assuming to have an \({\mathbb{L}}\)-structure \(M\) in \({\mathcal{K}}\) as in 24, we define the interpretation of sorts and contexts. For a sort \(X = S^{\,\mathbb{c}}\), we define \[\llbracket{ S^{\,\mathbb{c}}}\rrbracket \equiv_{\mathrm{def}}\llbracket{S}\rrbracket^{\,\mathbb{c} } \mathrlap{.}\] For a context \((\bar{x} \colon\bar{X}) = (x_1 \colon X_1, \ldots, x_n \colon X_n)\), we define \[\llbracket{ \bar{X} }\rrbracket \equiv_{\mathrm{def}}\llbracket{ X_1}\rrbracket \times \ldots \times \llbracket{X_n}\rrbracket \mathrlap{.}\] We then define the interpretation of the derivable judgements of the form 2 , so that a term \(s \colon Y\) in context \(\bar{x} \colon\bar{X}\) is interpreted as a morphism \[\llbracket{s}\rrbracket \colon\llbracket{\bar{X}}\rrbracket \to \llbracket{Y}\rrbracket \mathrlap{.}\] We do so by recursion on the derivation of the judgement, following the rules in ¿tbl:tab:terms?. First, for the variable rule, the interpretation of \((x_1 \colon X_1, \ldots, x_n \colon X_n) \;\mathsf{var}_i(\bar x) \colon X_i\), where \(1 \leq i \leq n\), is defined to be the \(i\)-th projection: \[\begin{tikzcd} \llbracket{ X_1}\rrbracket \times \ldots \times \llbracket{X_n}\rrbracket \ar[r, "\mathsf{pr}_i"] & \llbracket{X_i}\rrbracket \mathrlap{.} \end{tikzcd}\] For the function application rule, the interpretation of \(f(s_1, \ldots, s_n) \colon Y\) in context \(\bar{x} \colon\bar{X}\) is defined as the composite \[\begin{tikzcd}[column sep = huge] \llbracket{\bar{X}}\rrbracket \ar[r, "{(\llbracket{s_1}\rrbracket, \ldots, \llbracket{s_n}\rrbracket)}"] & \llbracket{Y_1}\rrbracket \times \ldots \times \llbracket{Y_n}\rrbracket \ar[r, "\llbracket{f}\rrbracket"] & \llbracket{Y}\rrbracket \mathrlap{,} \end{tikzcd}\] where, by the recursive hypothesis, we assumed that the interpretation of the judgements \((\bar{x} \colon\bar{X}) \;s_i \colon Y_i\) is defined. For the restriction rule, we define the interpretation of \(s \cdot f \colon S^{\,\mathbb{d}}\) to be the composite \[\begin{tikzcd} \llbracket{\bar{X}}\rrbracket \ar[r, "\llbracket{s}\rrbracket"] & \llbracket{S}\rrbracket^{\,\mathbb{c}} \ar[r, "\llbracket{S}\rrbracket^f"] & \llbracket{S}\rrbracket^{\,\mathbb{d}} \mathrlap{.} \end{tikzcd}\] For the power rule, assuming we have defined \(\llbracket{s}\rrbracket \colon\llbracket{\bar{X}}\rrbracket \to \llbracket{Y}\rrbracket\), we define the interpretation of \(s^{[1]} \colon X^{[1]}\) in context \(\bar{X}^{[1]}\) using the functoriality of powers, to be the composite \[\begin{tikzcd} \llbracket{ \bar{X}^{[1]} }\rrbracket \ar[r, "\cong"] & \llbracket{\bar{X}}\rrbracket^{[1]} \ar[r, "\llbracket{s}\rrbracket^{[1]}"] & \llbracket{Y}\rrbracket^{[1]} \ar[r, "\cong"] & \llbracket{Y^{[1]}}\rrbracket \mathrlap{,} \end{tikzcd}\] where, again, we assumed that the interpretation of \((\bar{x} \colon\bar{X}) \;s \colon Y\) is defined. Finally, for the substitution rule, the interpretation of \(t[s_1/y_i \ldots, s_n/y_n] \colon Y\) in context \(\bar{x} \colon\bar{X}\) is defined as the composite \[\begin{tikzcd}[column sep = huge] \llbracket{\bar{X}}\rrbracket \ar[r, "{(\llbracket{s_1}\rrbracket, \ldots, \llbracket{s_n}\rrbracket)}"] & \llbracket{Y_1}\rrbracket \times \ldots \times \llbracket{Y_n}\rrbracket \ar[r, "\llbracket{t}\rrbracket"] & \llbracket{Y}\rrbracket \mathrlap{.} \end{tikzcd}\]

Let \({M}\) be an \({\mathbb{L}}\)-structure in an isoregular 2-category \({\mathcal{K}}\). In order to extend the interpretation to the other forms of judgement, some additional care is required, since the derivability of judgements of one form is related to the derivability of the judgements of the other form, as familiar from dependent type theory. In particular, it is not possible to define the interpretation of propositions first and define what it means for a logical entailment to be valid separately. Instead, we start by defining a partial interpretation function mapping a judgement of the form \((\bar{x} \colon\bar{X}) \;A \colon\mathsf{prop}\) to a subobject \(\llbracket{A}\rrbracket \rightarrowtail \llbracket{\bar{X}}\rrbracket\) in \({\mathcal{K}}\) by recursion on the structure of the expression \(A\). This partial function will be proved to be total on the derivable judgements. To this end, we record when each clause is well-defined.

1. The interpretation of the judgement \((\bar{x} \colon\bar{X}) \;R(s_1, \ldots, s_n) \colon\mathsf{prop}\) is the pullback

   This is well-defined if we have \(m_R \colon\llbracket{R}\rrbracket \rightarrowtail \llbracket{\bar{Y}}\rrbracket\) and \(\llbracket{s_i}\rrbracket \colon\llbracket{\bar{X}}\rrbracket \to \llbracket{Y_i}\rrbracket\), for all \(1 \leq i \leq n\).

2. The interpretation of the judgement \((\bar{x} \colon\bar{X}) \;s=t \colon\mathsf{prop}\) is the equaliser of \(\llbracket{s}\rrbracket\) and \(\llbracket{t}\rrbracket\): \[\begin{tikzcd} \llbracket{s = t}\rrbracket \ar[r, >->] & \llbracket{\bar{X}}\rrbracket \ar[r, "\llbracket{s}\rrbracket", shift left = 1] \ar[r, "\llbracket{t}\rrbracket"', shift right = 1] & \llbracket{Y}\rrbracket \end{tikzcd}\] This is well-defined if we have \(\llbracket{s}\rrbracket \colon \llbracket{\bar{X}}\rrbracket \to \llbracket{Y}\rrbracket\) and \(\llbracket{t}\rrbracket \colon\llbracket{\bar{X}}\rrbracket \to \llbracket{Y}\rrbracket\).

3. The interpretation of the judgement \((\bar{x} \colon\bar{X}) \;A \wedge B \colon\mathsf{prop}\) is the pullback

   This is well-defined if the interpretations of the judgements \((\bar{x} \colon\bar{X}) \;A \colon\mathsf{prop}\) and \((\bar{x} \colon\bar{X}) \;B \colon\mathsf{prop}\) are so.

4. The interpretation of the judgement \((\bar{x} \colon\bar{X}^{[1]}) \vdash A^{[1]} \colon\mathsf{prop}\) is the pullback:

   This is well-defined if the interpretation of the judgement \((\bar{x} \colon\bar{X}) \;A \colon\mathsf{prop}\) is so.

5. The interpretation of the judgement \((\bar{x} \colon\bar{X}) \;(\exists y \colon Y) B(\bar{x}, y) \colon\mathsf{prop}\) is the (fully faithful regular epimorphism, monomorphism)-factorisation

   where \(p_1\) is the projection on the first factor. This is well-defined if the interpretation of the judgement \((\bar{x} \colon\bar{X}, y \colon Y) \;B(\bar{x}, y) \colon\mathsf{prop}\) is well-defined and \(m_B \circ p_1\) is an ffk-morphism in \({\mathcal{K}}\).

The next lemma can be understood as a form of definability.

We establish the soundness of the deduction rules of isoregular theories.

We are now ready to define the 2-categories of structures over a language, and of models over an isoregular theory.

Structures, morphisms of structures, and structure morphism 2-cells form an evident 2-category that we denote as \(\mathsf{Str}({\mathbb{L}},{\mathcal{K}})\). We then define the \(2\)-category of models of \({\mathbb{T}}\) in \({\mathcal{K}}\), written \(\mathsf{Mod}({\mathbb{T}},{\mathcal{K}})\), as the full subcategory of \(\mathsf{Str}({\mathbb{L}},{\mathcal{K}})\) spanned by the models of \({\mathbb{T}}\).

We conclude this section with two lemmas on the 2-categories of models which will be useful later.

4 Functorial semantics for isoregular theories↩︎

4.1 The syntactic 2-category of an isoregular theory↩︎

We construct the syntactic 2-category of an isoregular theory. For this, we introduce some definitions.

The next results introduce the syntactic 2-category of \({\mathbb{T}}\) (34) and establish that it is isoregular (36), by first showing that it it has finite 2-limits (7). For this, we put to work the deduction rules for isoregular theories. In order to simplify notation and make our arguments more readable, we work only with contexts of the form \((x \colon X)\), \((y \colon Y)\), \((x \colon X, y \colon Y)\). Of course, all arguments carry over to more general contexts.

The following lemma collects the stability properties of all our logic constructs, under powers by \([1]\); these will be essential in the proof of 37.

In order to state 10 11 12 below, for a morphism \([f]\colon \{ x\colon X|\;A( x)\}\to \{ y\colon Y|\;B( y)\}\) in \(\mathsf{Syn}({\mathbb{T}})\) we define the following judgements: \[\begin{align} & \mathsf{is\text{-}mono}(f) \equiv_{\mathrm{def}}\\ & \qquad (x, x' \colon X, y \colon Y)\; f(x,y), f(x', y) \vdash x' = x'' \mathrlap{,} \\ & \mathsf{is\text{-}faithful}(f) \equiv_{\mathrm{def}}\\ & \qquad (u, u' \colon X^{[1]}, v \colon Y^{[1]}) \;\mathsf{dom}(u) = \mathsf{dom}(u'), \mathsf{cod}(u) = \mathsf{cod}(u'), f^{[1]}(u,v), f^{[1]}(u',v) \vdash u = u' \mathrlap{,} \\ & \mathsf{is\text{-}full\text{-}identities}(f) \equiv_{\mathrm{def}}\\ & \qquad (x', x'' \colon X, y \colon Y) \;f(x',y), f(x'', y) \vdash (\exists u \colon X^{[1]}) f^{[1]}(u,\mathsf{id}_y) \land \mathsf{dom}(u) = x' \land \mathsf{cod}(u) = x'' \mathrlap{.} \end{align}\] For a proposition \((x \colon X, y \colon Y) B(x,y) \colon\mathsf{prop}\), we have a composite morphism \[m_B \colon\{x \colon X, y \colon Y \;| \;B(x,y) \} \rightarrowtail \{x \colon X \;| \;\top\} \times \{y \colon Y \;| \; \top\} \to \{y \colon Y \;| \; \top\}\] in \(\mathsf{Syn}({\mathbb{T}})\). Then, the judgement \(\mathcal{J}_{\mathsf{mono}}(B)\) of [tbl:equ:exists-formation-mono] is equivalent to the judgement \(\mathsf{is\text{-}mono}(m_B)\). A similar equivalence holds for the judgements in [tbl:equ:exists-formation-eqfib].

4.2 Functorial semantics↩︎

The next result is fundamental for our development, as it provides a counterpart of the cornerstones of functorial semantics in the 1-categorical setting by establishing the connection between 2-categories of models of isoregular theories and 2-categories of isoregular 2-functors.

5 Accessibility of 2-categories of models↩︎

5.1 Basics↩︎

The notion of accessible 2-category that we use is a specialization of one that has been considered for enriched categories, for the first time, in [16]. Another notion of accessibility (for enriched categories) had been introduced before in [34], but these coincide in the 2-categorical context by [35].

Given a 2-category \({\mathcal{K}}\) with \(\lambda\)-filtered colimits, an object \(X\in K\) is called \(\lambda\)-presentable if \({\mathcal{K}}(X,-)\colon {\mathcal{K}}\to\mathsf{Cat}\) preserves \(\lambda\)-filtered colimits. Then, by [36], a 2-category \({\mathcal{K}}\) with \(\lambda\)-filtered colimits is \(\lambda\)-accessible if and only if there is a set \({\mathcal{G}}\) of \(\lambda\)-presentable objects such that every objects of \({\mathcal{K}}\) can be written as a \(\lambda\)-filtered colimit of objects in \({\mathcal{G}}\).

The accessible 2-categories that we are interested in are those that admit all flexible limits; that is, have all small products, inserters, and equifiers. (Flexible limits also include splitting of idempotents, but these already exist in any accessible 2-category). Note that any 2-category with flexible limits has in particular also all (weighted) pseudolimits and (weighted) bilimits, see for instance [11].

Accessible 2-categories with flexible limits have been studied in [14], [16], [17]. We recall some of the key facts that will be used later.

5.2 Accessibility of models↩︎

We will now show that every 2-category of models of a isoregular theory is accessible with flexible limits.

We deduce the following result from 41 using 37.

6 Applications↩︎

6.1 Preliminaries↩︎

In this section we focus on models of isoregular theories in \(\mathsf{Cat}\), providing several applications of our general results, both proving new fact and giving new proofs of known ones in a uniform manner. We begin by considering categories with finite limits and colimits (6.2), move on to categories satisfying a variety of exactness conditions, as studied in categorical algebra (6.3), isofibrations and Grothendieck fibrations (6.4) and conclude with categories of interest in categorical logic, such as comprehension categories and clans (6.5).

Let us first make some general observations. If \({\mathbb{T}}\) is an isoregular theory over a language \({\mathbb{L}}\), and \(M\) is an \({\mathbb{L}}\)-structure in \(\mathsf{Cat}\) (or more generally in any isoregular \({\mathcal{K}}\) where the (strong epi, mono) factorization system exists), then the interpretation of any isoregular formula \((\bar X) \;A \colon\mathsf{prop}\), relative to \({\mathbb{T}}\), is well-defined as a subobject \(\llbracket{A}\rrbracket\rightarrowtail\llbracket{\bar X}\rrbracket\) since to interpret existential quantification we can take the (strong epi, mono) factorisation of the relevant arrow. Note that such interpretation coincides with the one we introduced since the (fully faithful regular epimorphism, monomorphism)-factorisation, when it exists, coincides with the (strong epimorphism, monomorphism)-factorisation.

Because of this the statement of 44 below is well-formed. This result will be essential in recognising the 2-categories of models of isoregular theories, as it allows us test the validity of the axioms at the level of the underlying sets (of objects), as with ordinary satisfaction.

Given this, it becomes quite easy to check when a given \({\mathbb{L}}\)-structure satisfies an entailment between isoregular formulas. Indeed, we are reduced to check that certain inclusions of sets hold, and at the level of object the interpretation of an isocartesian formula is what one expects it to be (remembering that we now have non-discrete arities):

• \(\mathsf{Ob}(\llbracket{S^{\,\mathbb{b}}}\rrbracket)=\{f\colon\,\mathbb{b}\to \llbracket{S}\rrbracket|\;f \text{ is a functor} \}\); that is, the set of diagrams of shape \(\,\mathbb{b}\) in \(\llbracket{S}\rrbracket\);

• \(\mathsf{Ob}(\llbracket{A^{[1]}}\rrbracket)=\mathsf{Mor}(\llbracket{A}\rrbracket)\) is the set of morphisms in \(\llbracket{A}\rrbracket\);

• \(\mathsf{Ob}(\llbracket{A\wedge B}\rrbracket)=\{ a\in \mathsf{Ob}(\llbracket{\bar X}\rrbracket) |\; a\in \mathsf{Ob}(\llbracket{A}\rrbracket)\text{ and } a\in \mathsf{Ob}(\llbracket{B}\rrbracket)\}\);

• \(\mathsf{Ob}(\llbracket{(\exists y\colon Y)A(\bar x,y)}\rrbracket)=\{ a\in \mathsf{Ob}(\llbracket{\bar X}\rrbracket) | \text{ there is } b\in \mathsf{Ob}(\llbracket{Y}\rrbracket)\text{ such that } (a,b)\in \mathsf{Ob}(\llbracket{A}\rrbracket)\}\);

For this reason, in the examples below we shall not dwell too much on trying to explain what it means for an \({\mathbb{L}}\)-structure to satisfy a given axiom (on object), as that simply amounts to translating into natural language what is written in symbols.

6.2 Limits and colimits↩︎

Fix a finite category \(\,\mathbb{b}\). Denote by \({\,\mathbb{b}}\)-\(\mathsf{lim}\) the 2-category of small categories with \(\,\mathbb{b}\)-limits, \(\,\mathbb{b}\)-limit preserving functors, and 2-natural transformations. We describe an isoregular theory \({\mathbb{T}}_{\,\mathbb{b}}\) whose models in \(\mathsf{Cat}\) are exactly small categories with limits of shape \(\,\mathbb{b}\); this follows the approach of [18].

Let us set some notation first. We denote by \(0*\,\mathbb{b}\) the category obtained by freely adding to \(\,\mathbb{b}\) an initial object \(0\); similarly, we let \([1]*\,\mathbb{b}\) be the category obtained by adding a further initial object to \(0*\,\mathbb{b}\) (or equivalently, adding an “initial arrow” to \(\,\mathbb{b}\)). Finally, we let \(\,\mathbb{I}*\,\mathbb{b}\) be the category obtained by adding an inverse to the new morphism of \([1]*\,\mathbb{b}\). To motivate the introduction of these notations, note that if \({\mathcal{C}}\in\mathsf{Cat}\), then an object of \({\mathcal{C}}^{0*\,\mathbb{b}}\) is the same as a functor \(\,\mathbb{b}\to {\mathcal{C}}\) together with a cone over it; while to give an object of \({\mathcal{C}}^{[1]*\,\mathbb{b}}\) is the same as giving a functor \(\,\mathbb{b}\to {\mathcal{C}}\), two cones over it, and a morphism in \({\mathcal{C}}\) between the two cones; in \({\mathcal{C}}^{\,\mathbb{I}*\,\mathbb{b}}\) such morphism of cones is equipped with an inverse.

Now, define the language \(\mathbb{L}_{\,\mathbb{b}}\) to have one sort \(S\) and just a relation symbol \(R_{\,\mathbb{b}}:S^{0*\,\mathbb{b}}\). The idea is that for each \(\mathbb{L}\)-structure \(\llbracket{-}\rrbracket\) in \(\mathsf{Cat}\), we shall think of \(\llbracket{R_{\,\mathbb{b}}}\rrbracket\) as the category of limiting cones over diagrams of shape \(\,\mathbb{b}\).

First, let us define the formula \((x,y\colon S^{0*\,\mathbb{b}}, z\colon S^{[1]*\,\mathbb{b}})\;A(x,y,z)\) as below \[(x,y\colon S^{0*\,\mathbb{b}}, z\colon S^{[1]*\,\mathbb{b}})\; R_{\,\mathbb{b}}(y)\wedge (z\cdot j_0=x) \wedge (z\cdot j_1=y) \mathrlap{,}\] where \(j_0,j_1\colon 0*\,\mathbb{b}\to [1]*\,\mathbb{b}\) sending \(\,\mathbb{b}\) to itself and picking out the domain and codomain of the freely added map respectively; below we will also use the inclusion \(\iota\colon\,\mathbb{b}\to 0*\,\mathbb{b}\). We now define the theory \({\mathbb{T}}_{\,\mathbb{b}}\) to consist of the following axioms:

1. \({\mathcal{J}}_{\mathsf{mono}}(A)\);

2. \((x,y\colon S^{0*\,\mathbb{b}})\;R_{\,\mathbb{b}}(y),\;(x\cdot \iota=y\cdot \iota) \vdash (\exists z\colon S^{[1]*\,\mathbb{b}})\;A(x,y,z)\);

3. \((z\colon S^{\,\mathbb{I}*\,\mathbb{b}})\;R_{\,\mathbb{b}}(z\cdot j_0)\vdash R_{\,\mathbb{b}}(z\cdot j_1)\);

4. \((z\colon S^{[1]\times 0*\,\mathbb{b}})\;R_{\,\mathbb{b}}(\mathsf{dom}(z)), R_{\,\mathbb{b}}(\mathsf{cod}(z))\vdash R_{\,\mathbb{b}}^{[1]}(z)\);

5. \((x\colon S^{\,\mathbb{b}})\;\vdash (\exists y\colon S^{0*\,\mathbb{b}})\;R_{\,\mathbb{b}}(y)\wedge (y\cdot \iota= x)\).

Alternatively, one can axiomatise the same class of models with axioms (i)–(iv) plus additional axioms that ensure that the existential quantifier in (v) is well-formed. However, this is unnecessary since this can be derived from axioms (i)–(iv), as we show in the proof of 13 below.

In a similar way we can construct a language \({\mathbb{L}}_{{\,\mathbb{b}}}'\) and an isoregular theory \({\mathbb{T}}'_{{\,\mathbb{b}}}\) such that \[\mathsf{Mod}({\mathbb{T}}'_{\,\mathbb{b}}, \mathsf{Cat}) \cong \,\mathbb{b}\text{-}{\mathsf{colim}}\] is isomorphic to the 2-category of small categories with \(\,\mathbb{b}\)-colimits, \(\,\mathbb{b}\)-colimit preserving functors, and 2-natural transformations. The difference from the previous case is that, instead of freely adding an initial object (or initial arrow/isomorphism) to \(\,\mathbb{b}\), we add a terminal object (or terminal arrow/isomorphism). So the language \({\mathbb{L}}_{\,\mathbb{b}}'\) will still have one sort \(S\), but a relation symbol \(R_{\,\mathbb{b}}'\colon S^{\,\mathbb{b}*0}\). The theory \({\mathbb{T}}_{\,\mathbb{b}}'\) will have essentially the same axioms of \({\mathbb{T}}_{\,\mathbb{b}}\), with properly modified arities.

Now we can allow \(\,\mathbb{b}\) to vary and define theories for the 2-categories: \(\mathsf{Lex}\) of small categories with finite limits, finite-limit preserving functors, and natural transformations; \(\mathsf{Rex}\) of small categories with finite colimits, finite-colimit preserving functors, and natural transformations; and \(\mathsf{RLex}\) of small categories with finite limits and finite colimits, finite-limit and finite-colimit preserving functors, and natural transformations.

More precisely, we define languages \[{\mathbb{L}}_{\mathsf{lex}}\equiv_{\mathrm{def}}\bigcup_{\,\mathbb{b}\in\mathsf{finCat}} {\mathbb{L}}_{\,\mathbb{b}}, \qquad {\mathbb{L}}_{\mathsf{rex}}'\equiv_{\mathrm{def}}\bigcup_{\,\mathbb{b}\in\mathsf{finCat}} {\mathbb{L}}_{\,\mathbb{b}}', \qquad {\mathbb{L}}_{\mathsf{rlex}}\equiv_{\mathrm{def}}{\mathbb{L}}_{\mathsf{lex}}\cup {\mathbb{L}}_{\mathsf{rex}}\] and corresponding isoregular theories \[{\mathbb{T}}_{\mathsf{lex}}\equiv_{\mathrm{def}}\bigcup_{\,\mathbb{b}\in\mathsf{finCat}} {\mathbb{T}}_{\,\mathbb{b}}, \qquad {\mathbb{T}}_{\mathsf{rex}}'\equiv_{\mathrm{def}}\bigcup_{\,\mathbb{b}\in\mathsf{finCat}} {\mathbb{T}}_{\,\mathbb{b}}', \qquad {\mathbb{T}}_{\mathsf{rlex}}\equiv_{\mathrm{def}}{\mathbb{T}}_{\mathsf{lex}}\cup {\mathbb{T}}_{\mathsf{rex}}\] respectively on \({\mathbb{L}}_{\mathsf{lex}}\), \({\mathbb{L}}_{\mathsf{rex}}\), and \({\mathbb{L}}_{\mathsf{rlex}}\).

It follows immediately by Lemma 13, its dual, and how models are defined that the following holds.

6.3 Exactness conditions↩︎

We now consider 2-categories of categories satisfying a variety of exactness conditions, namely regular, Mal’sev, exact, protomodular, and semiabelian categories (see [37]–[39] for details).

We begin by considering regular categories and write \(\mathsf{Reg}\) for the 2-category of regular categories, regular functors, and natural transformations. Let \({\mathbb{L}}_{\mathsf{reg}}\) be the language obtained by adding to \({\mathbb{L}}_{\mathsf{lex}}\) one relation symbol \(R_{\mathsf{ckp}}:S^{\,\mathbb{p}*0}\), where \(\,\mathbb{p}\) is the free-living pair of arrows. This new relation will be used to encode the coequalisers of kernel pairs. To define \({\mathbb{T}}_{\mathsf{reg}}\) we extend \({\mathbb{T}}_{\mathsf{lex}}\) by adding a few axioms. To begin with, we ask that every element of \(R_{\mathsf{ckp}}\) is a coequaliser; this is done by taking the dual of axioms (i)-(iv) of the theory \({\mathbb{T}}_{\,\mathbb{b}}\). In more detail, we first define the formula \((x,y\colon S^{\,\mathbb{p}*0}, z\colon S^{\,\mathbb{p}*[1]})\;A(x,y,z)\) as below \[(x,y\colon S^{\,\mathbb{p}*0}, z\colon S^{\,\mathbb{p}*[1]})\; R_{\mathsf{ckp}}(x)\wedge (z\cdot j_0=x) \wedge (z\cdot j_1=y)\] where \(j_0,j_1\colon \,\mathbb{p}*0\to \,\mathbb{p}*[1]\) pick out the domain and codomain of the freely added map respectively. Then add to \({\mathbb{T}}_{\mathsf{lex}}\) the axioms:

1. \({\mathcal{J}}_{\mathsf{mono}}(A)\);

2. \((x,y\colon S^{\,\mathbb{p}*0})\;R_{\mathsf{ckp}}(x),\;(x\cdot \iota=y\cdot \iota) \vdash (\exists z\colon S^{\,\mathbb{p}*[1]})\;A(x,y,z)\);

3. \((z\colon S^{\,\mathbb{p}*\,\mathbb{I}})\;R_{\mathsf{ckp}}(z\cdot j_0)\vdash R_{\mathsf{ckp}}(z\cdot j_1)\);

4. \((z\colon S^{[1]\times \,\mathbb{p}*0})\;R_{\mathsf{ckp}}(\mathsf{dom}(z)), R_{\mathsf{ckp}}(\mathsf{cod}(z))\vdash R_{\mathsf{ckp}}^{[1]}(z)\).

The next step is to ask that every kernel pair has a coequaliser. To that end, we use that kernel pairs are just a specific kind of pullback. For simplicity denote by \(R_{\mathsf{pb}}\equiv_{\mathrm{def}}R_{\,\mathbb{c}}\), where \(\,\mathbb{c}\) is the free cospan, the relation of \({\mathbb{L}}_{\mathsf{reg}}\) containing the pullback squares. This has sort \(S^{0*\,\mathbb{c}}\) which, since \(0*\,\mathbb{c}\cong [1]\times [1]\), by substitution we can replace with \(S^{[1]\times [1]}\). Consider the formula \((x\colon S^{\,\mathbb{p}*0})\;A_{\mathsf{kp}}(x)\) as below \[(\exists y\colon S^{[1]\times [1]})\;R_{\mathsf{pb}}(y)\wedge (\mathsf{pr}_d(y)=\mathsf{pr}_q(x)) \wedge (\mathsf{pr}_r(y)=\mathsf{pr}_q(x))\wedge (\mathsf{pr}_u(y)=\mathsf{pr}_f(x)) \wedge (\mathsf{pr}_l(y)=\mathsf{pr}_g(x)),\] where \(f,g\) denote the parallel arrows in \(\,\mathbb{p}*0\) and \(q\) the coequalising one.

We now add the axiom stating that every kernel pair has a coequaliser:

1. \((x\colon S^{\,\mathbb{p}*0})\;A_{\mathsf{kp}}(x)\vdash (\exists y:S^{\,\mathbb{p}*0})\;R_{\mathsf{ckp}}(y)\wedge (\mathsf{pr}_f(y)=\mathsf{pr}_f(x))\wedge (\mathsf{pr}_g(y)=\mathsf{pr}_g(x)).\)

Finally, we add an axiom saying that coequalisers of kernel pairs are stable under pullback. For that consider the finite category \(\,\mathbb{d}\) generated by the commutative diagram below.

Denote by \(\iota_t,\iota_b\colon \,\mathbb{p}*0\to \,\mathbb{d}\) the inclusion of the top and bottom co-forks respectively, and by \(\iota_{sq}\colon [1]\times [1]\to \,\mathbb{d}\) the inclusion of the square on the right. Then pullback stability of coequalisers of kernel pairs is expressed by the following axiom:

1. \((x\colon S^{\,\mathbb{d}})\;R_{\mathsf{pb}}(x\cdot \iota_{sq}),\;R_{\mathsf{ckp}}(x\cdot \iota_t),\;A_{\mathsf{kp}}(x\cdot \iota_b) \vdash R_{\mathsf{ckp}}(x\cdot \iota_b).\)

Recall that a Mal’cev category is a lex category where every reflexive relation is an equivalence relation [38]. Define \(\mathsf{Mal}\) to be the full subcategory of \(\mathsf{Lex}\) spanned by the Mal’cev categories, and \(\mathsf{RMal}\) to be the full subcategory of \(\mathsf{Reg}\) spanned by the regular Mal’cev categories.

To define a theory whose models are Mal’cev categories, we first construct a theory that identifies all internal relations (that is, jointly monic pairs of arrows) in a category. Starting from the language and theory for lex categories, add a relation symbol \(R_{\mathsf{irel}}:S^{\,\mathbb{p}}\), where \(\,\mathbb{p}\) is the free-living pair, which will contain the internal relations; we call the new language \({\mathbb{L}}_{\mathsf{irel}}\). We expand \({\mathbb{T}}_{\mathsf{lex}}\) by adding the axioms:

1. \((x\colon S^{\,\mathbb{p}})\;R_{\mathsf{irel}}(x) \vdash(\exists y\colon S^{[1]\times [1]}) R_{\mathsf{pb}}(y)\wedge (\mathsf{pr}_d(y)=\mathsf{pr}_f(x)) \wedge (\mathsf{pr}_r(y)=\mathsf{pr}_g(x))\wedge\)
   \((\mathsf{pr}_u(y)=\mathsf{id}_{\mathsf{dom}(\mathsf{pr}_u(y))}) \wedge (\mathsf{pr}_l(y)=\mathsf{id}_{\mathsf{dom}( \mathsf{pr}_l(y))})\)

2. \((x\colon S^{\,\mathbb{p}})\; R_{\mathsf{pb}}(y)\wedge (\mathsf{pr}_d(y)=\mathsf{pr}_f(x)) \wedge (\mathsf{pr}_r(y)=\mathsf{pr}_g(x))\wedge (\mathsf{pr}_u(y)=\mathsf{id}_{\mathsf{dom}(\mathsf{pr}_u(y))}) \wedge\)
   \((\mathsf{pr}_l(y)=\mathsf{id}_{\mathsf{dom}( \mathsf{pr}_l(y))}) \vdash R_{\mathsf{irel}}(x);\)

3. \((z\colon S^{[1]\times \,\mathbb{p}})\;R_{\mathsf{irel}}(\mathsf{dom}(z)), R_{\mathsf{irel}}(\mathsf{cod}(z))\vdash R_{\mathsf{irel}}^{[1]}(z)\).

These three axioms together ensure that \(R_{\mathsf{irel}}\) is the full (axiom (iii)) subcategory of \(S^{\,\mathbb{p}}\) spanned by all the internal relations (axioms (i) and (ii)). At this point we still have \(\mathsf{Mod}({\mathbb{T}}_{\mathsf{irel}},\mathsf{Cat})\cong\mathsf{Lex}\), since we are not adding any new properties.

To construct the theory \({\mathbb{T}}_{\mathsf{Mal}}\) for Mal’cev categories we now need to introduce formulas expressing when a relation is reflexive, symmetric, or transitive. Within \({\mathbb{T}}_{\mathsf{irel}}\), the formula for reflexivity \((x\colon S^{\,\mathbb{p}})\;A_{\mathsf{refl}}(x)\) is defined by \[(x\colon S^{\,\mathbb{p}})\;(\exists y\colon S^{\,\mathbb{p}'})\;R_{\mathsf{irel}}(x)\wedge (y_f=x_f) \wedge (y_g=x_g),\] where \(\,\mathbb{p}'\) is the free split pair, obtained by adding a common splitting to the two arrows in \(\,\mathbb{p}\). Note that the \(y\colon S^{\,\mathbb{p}'}\) above is unique since \(x\) is an internal relation. The formulas \(A_{\mathsf{sym}}(x)\) and \(A_{\mathsf{tran}}(x)\) are constructed in a similar way.

Thus, we can define \({\mathbb{T}}_{\mathsf{mal}}\) by adding to \({\mathbb{T}}_{\mathsf{irel}}\) the axiom \[(x\colon S^{\,\mathbb{p}})\;A_{\mathsf{refl}}(x) \vdash A_{\mathsf{sym}}(x)\wedge A_{\mathsf{tran}}(x).\] Similarly, we can consider the isoregular theory \({\mathbb{T}}_{\mathsf{rmal}}\equiv_{\mathrm{def}}{\mathbb{T}}_{\mathsf{reg}}\cup {\mathbb{T}}_{\mathsf{mal}}\) which models regular Mal’cev categories.

A direct application of Corollary 43 and Theorem 40 then gives the result below, ensuring the existence of free Mal’cev categories.

Let us write \(\mathsf{Ex}\) for the 2-category of (Barr) exact categories, exact functors, and natural transformations. Extending \({\mathbb{T}}_{\mathsf{reg}}\) and \({\mathbb{T}}_{\mathsf{irel}}\), we can define an isoregular theory \({\mathbb{T}}_{\mathsf{ex}}\) such that \[\mathsf{Mod}({\mathbb{T}}_{\mathsf{ex}},\mathsf{Cat})\cong\mathsf{Ex}\mathrlap{.}\] To do this, start from the language \({\mathbb{L}}_{\mathsf{reg}}\cup {\mathbb{L}}_{\mathsf{irel}}\) and add to \({\mathbb{T}}_{\mathsf{reg}}\cup {\mathbb{T}}_{\mathsf{irel}}\) the axiom \[(x\colon S^{\,\mathbb{p}})\;A_{\mathsf{refl}}(x), A_{\mathsf{sym}}(x), A_{\mathsf{tran}}(x)\vdash (\exists y\colon S^{\,\mathbb{p}*0})\;A_{\mathsf{kp}}(y)\wedge (\mathsf{pr}_f(y)=\mathsf{pr}_f(x)) \wedge (\mathsf{pr}_g(y)=\mathsf{pr}_g(x)\] saying that every equivalence relation arises as a (unique up to isomorphism) kernel pair.

The next notion from categorical algebra that we examine is protomodularity. Recall that a category with pullbacks is called protomodular if for any commutative diagram

where \(t\circ s=1\), if (a) and (a+b) are pullback squares, then so is (b) (see [40]). We can express this property with an isoregular theory. We denote by \(\mathsf{Ptm}\) the 2-category of protomodular categories, pullback-preserving functors, and natural transformations between them.

We start from the theory \({\mathbb{T}}_{\mathsf{pb}}\) of categories with pullbacks. Denote by \(\,\mathbb{q}\) the category generated by the diagram above, and by \(\iota_a,\iota_b,\iota_{a+b}\colon[1]\times [1]\to \,\mathbb{q}\) the inclusions of the three squares. Then it is enough to add to \({\mathbb{T}}_{\mathsf{pb}}\) the axiom \[(x\colon S^{\,\mathbb{q}})\quad R_{\mathsf{pb}}(x\cdot \iota_a), R_{\mathsf{pb}}(x\cdot \iota_{a+b})\vdash R_{\mathsf{pb}}(x\cdot \iota_b).\] Call \({\mathbb{T}}_{\mathsf{ptm}}\) the new theory we obtain; it is then straightforward to show that

As a consequence, we can establish the existence of free protomodular categories over categories of pullbacks. Below, we write \(\mathsf{Pb}\) for the 2-category of small categories with pullbacks, pullback-preserving functors, and natural transformations.

Recall that a category is called semi-abelian if it is exact, protomodular, has finite coproducts, and has a zero object (see again see [40]). Denote by \(\mathsf{SmAb}\) the 2-category of semi-abelian categories, exact and finite coproduct-preserving functors, and natural transformations between them. To construct a theory for semi-abelian category then it is enough to define \({\mathbb{T}}_{\mathsf{smab}}\) as the union of:

• the theory \({\mathbb{T}}_{\mathsf{ex}}\) of exact categories (which contains in particular a relation \(R_\emptyset\colon S^{[0]}\) collecting all terminal objects),

• the theory \({\mathbb{T}}_{\mathsf{ptm}}\) of protomodular categories,

• the theory \({\mathbb{T}}_{\mathsf{fc}}\) of categories with finite coproducts (which contains a relation \(R'_\emptyset\colon S^{[0]}\) collecting all the initial objects);

• the single axiom \[(x\colon S^{[0]})\quad R_\emptyset(x)\vdash R'_\emptyset(x)\] expressing the fact that every terminal object is also initial.

Given this it is straightforward to show

As a consequence also free semi-abelian categories exist; below \(\mathsf{Fc}\) is the 2-category of small categories with finite coproducts, finite-coproduct preserving functors, and natural transformations.

6.4 Fibrations↩︎

We now consider isofibrations and Grothendieck fibrations. Recall that a functor \(p\colon {\mathcal{E}}\to {\mathcal{B}}\) is an isofibration if and only if for any \(x\in{\mathcal{E}}\) and any isomorphism \(u\colon px\to y\) in \({\mathcal{B}}\) there exists an isomorphism \(v\colon x\to x'\) in \({\mathcal{E}}\) with \(pv=u\). We denote by \(\mathsf{IsoFib}\) the full subcategory of \(\mathsf{Cat}^{[1]}\) spanned by the isofibrations.

Given this, it is straightforward to write down the language and theory for isofibrations. We let \({\mathbb{L}}_{\mathsf{isofib}}\) have two basic sorts \(E,B\) and one function symbol \(p\colon E\to B\); then \({\mathbb{T}}_{\mathsf{isofib}}\) consists of the single axiom \[(x\colon E, u\colon B^{\,\mathbb{I}})\;\mathsf{dom}(u_0)=p(x) \vdash (\exists v\colon E^{\,\mathbb{I}})\;\mathsf{dom}(v_0)=x \wedge p^{[1]}(v_0)=u_0.\] As before, we denoted by \(\,\mathbb{I}\) the category obtained by adding an inverse to the morphism in \([1]\); given \(u\colon S^{\,\mathbb{I}}\) we denote by \(u_0\colon S^{[1]}\) the restriction of \(u\) along the inclusion. Similarly, we denote by \(u_0^{-1}\colon S^{[1]}\) the restriction along the inclusion \([1]\to\,\mathbb{I}\) picking the added inverse.

Let us write \(\mathsf{GFib}\) for the locally full subcategory of \(\mathsf{Cat}^{[1]}\) spanned by the Grothendieck fibrations, and those commutative squares whose top functor preserves the cartesian arrows. The language \({\mathbb{L}}_{\mathsf{Gfib}}\) for the theory of Grothendieck fibrations consists of two basic sorts \(E,B\), a function symbol \(p\colon E\to B\), and a relation symbol \(\mathsf{Cart}\rightarrowtail E^{[1]}\) that will collect all cartesian arrows in \(E\). Before defining the theory, to set notation consider the finite categories below:

and denote by \(\iota_{\,\mathbb{e}}\colon\,\mathbb{e} \to [2]\) the inclusion.

Now we define \({\mathbb{T}}_{\mathsf{Gfib}}\) to consist of the following axioms:

1. \((z,w\colon E^{[2]})\quad \mathsf{Cart}(\mathsf{snd}(z)),\;z\cdot \iota_{\,\mathbb{e}}=w\cdot \iota_{\,\mathbb{e}},\;p^{[1]}(\mathsf{fst}(z))=p^{[1]}(\mathsf{fst}(w))\vdash z=w\);

2. \((x\colon E^{\,\mathbb{e}}, z\colon B^{[2]})\quad \mathsf{Cart}(\mathsf{snd}(x)),\;p^{[1]}(\mathsf{snd}(x))=\mathsf{snd}(z),\;p^{[1]}(\mathsf{comp}(x))=\mathsf{comp}(z)\quad\)
   \(\vdash (\exists w\colon E^{[2]})\quad w\cdot\iota_{\,\mathbb{e}}= x\wedge p^{[1]}(\mathsf{fst}(w))=\mathsf{fst}(z)\wedge \mathsf{Cart}(\mathsf{snd}(w))\);

3. \((y\colon E^{\,\mathbb{f}})\quad \mathsf{Cart}(\mathsf{snd}(y)) \vdash \mathsf{Cart}(\mathsf{comp}(y))\);

4. \((u\colon E^{[1]\times [1]})\quad \mathsf{Cart}(\mathsf{dom}(u)), \mathsf{Cart}(\mathsf{cod}(u))\vdash \mathsf{Cart}^{[1]}(u)\);

5. \((y\colon E, u\colon B^{[1]})\quad \mathsf{cod}(u)=p(y) \vdash (\exists v\colon E^{[1]})\;\mathsf{Cart}(v)\wedge \mathsf{cod}(v)=y \wedge p^{[1]}(v)=u\).

6.5 Categorical logic, adjoints, and multicategories↩︎

We conclude by applying our results to various 2-categories of interest in categorical logic, 2-categories of adjoint functors, and multicategories.

Recall [41] that a comprehension category is the data of a commutative triangle

in \(\mathsf{Cat}\), where \(\mathsf{cod}\) is the codomain functor, \(p\) is a Grothendieck fibration, and \(\Sigma\) sends cartesian arrows to pullback squares. Comprehension categories assemble into a 2-category \(\mathsf{Cmp}\) whose morphisms are of the form

where \(F\) preserves the cartesian arrows. The 2-cells of \(\mathsf{Cmp}\) are just 2-cells in \(\mathsf{Cat}^{[2]}\) (the 2-category of commutative triangles in \(\mathsf{Cat}\)).

To define as isoregular theory describing comprehension categories, consider the language \({\mathbb{L}}_{\mathsf{cmp}}\) consisting of two sorts \(E,B\), two function symbols \(p\colon E\to B\) and \(\Sigma\colon E\to B^{[1]}\), and a relation symbol \(\mathsf{Cart}\rightarrowtail E^{[1]}\). Then \({\mathbb{T}}_{\mathsf{comp}}\) is defined by:

1. the axiom \((x\colon E)\;\mathsf{cod}(\Sigma(x))=p(x) ;\)

2. all of the axioms in of \({\mathbb{T}}_{\mathsf{Gfib}}\), asserting that \(p\) is a Grothendieck fibration and \(\mathsf{Cart}\) collects all cartesian maps;

3. axioms asserting that if \(\mathsf{Cart}(u)\) holds, then \(\Sigma^{[1]}(u)\colon B^{[1]\times[1]}\) is a pullback square in \(B\); this is done as in Section 6.2.

Given what we have shown already about limits and Grothendieck fibrations, the next lemma follows easily.

Recall [43], [44] that a clan is a category \({\mathcal{C}}\) together with a set of morphisms \(\mathsf{Fib}\subseteq {\mathcal{C}}^{[1]}\) (which we see as a full subcategory) such that:

• \({\mathcal{C}}\) has a terminal object \(1\);

• pullbacks along maps in \(\mathsf{Fib}\) exist;

• every isomorphism and every map with codomain \(1\) lies in \(\mathsf{Fib}\);

• the elements of \(\mathsf{Fib}\) are closed under composition and stable under pullback.

Clans assemble in a 2-category \(\mathsf{Clan}\) whose morphisms are functors preserving the class of fibrations as well as the terminal object and pullbacks along fibrations; 2-cells are just natural transformations.

The language \({\mathbb{L}}_{\mathsf{clan}}\) for clans consists of a single sort \(S\), a relation symbol \(\mathsf{Fib}\rightarrowtail S^{[1]}\) for the set of fibrations, a relation symbol \(R_\emptyset\rightarrowtail S\) to collect the terminal objects, and a relation symbol \(R_{\mathsf{pb}}\rightarrowtail S^{[1]\times [1]}\) collecting all the pullbacks along maps in \(\mathsf{Fib}\). The isoregular theory \({\mathbb{T}}_{\mathsf{clan}}\) is then formed by:

1. the five axioms of Section 6.2 for \(\,\mathbb{b}=\emptyset\), saying that \(S\) has a terminal object and \(R_\emptyset\) collects all of them;

2. the first four axioms of Section 6.2 for \(\,\mathbb{b}\) the free cospan (with inclusion \(\iota\colon\,\mathbb{b}\to [1]\times [1]\)), saying that \(R_{\mathsf{pb}}\) consists of pullback squares, is closed under isomorphisms, and is a full subcategory of \(S^{[1]\times [1]}\);

3. the axiom (similar to (v) in Section 6.2) \[(x\colon S^{\,\mathbb{b}})\; \mathsf{Fib}(\mathsf{pr}_r(x))\vdash (\exists y\colon S^{[1]\times [1]})\;R_{\mathsf{pb}}(y)\wedge (y\cdot \iota= x)\] for \(\,\mathbb{b}\) the free co-span, saying that pullbacks along maps in \(\mathsf{Fib}\) exists and are in \(R_{\mathsf{pb}}\);

4. the axiom \[(z\colon S^{[1]\times [1]})\;\mathsf{Fib}(\mathsf{dom}(z)), \mathsf{Fib}(\mathsf{cod}(z))\vdash \mathsf{Fib}^{[1]}(z)\] saying that \(\mathsf{Fib}\) defines a full subcategory;

5. the axiom \[(u\colon S^{\,\mathbb{I}}) \vdash \mathsf{Fib}(u_0)\] saying that \(\mathsf{Fib}\) contains all isomorphism (we follow the notation used in Section [sec:isofib]);

6. the axiom \[(u\colon S^{[2]})\; \mathsf{Fib}(\mathsf{fst}(u)), \mathsf{Fib}(\mathsf{snd}(u))\vdash \mathsf{Fib}(\mathsf{comp}(u))\] saying that \(\mathsf{Fib}\) is closed under composition;

7. the axiom \[(z\colon S^{[1]\times [1]})\;R_{\mathsf{pb}}(z)\vdash \mathsf{Fib}(\mathsf{pr}_l(z))\wedge \mathsf{Fib}(\mathsf{pr}_r(z))\] saying that the vertical legs of every square in \(R_{\mathsf{pb}}\) lie in \(\mathsf{Fib}\). Together with (iii) this implies that \(\mathsf{Fib}\) is stable under pullbacks.

For an example of a slightly different nature, let us consider \(\mathsf{Radj}\), the locally full sub-2-category of \(\mathsf{Cat}^{[1]}\) whose objects are right adjoint functors \(R\colon{\mathcal{C}}\to{\mathcal{D}}\), and morphisms are squares

were \(F\) preserves universal arrows; that is, if \(\eta\) is a universal arrow from \(c\in {\mathcal{C}}\) to \(R\), then \(F\eta\) is a universal arrow from \(Fc\) to \(R'\). This is equivalent to requiring that \(F\) preserves the units of the adjunction up to isomorphism.

At this point the reader will probably guess how to construct an isoregular theory that models \(\mathsf{Radj}\). The idea is that, beside having a function symbol \(R\colon C\to D\) between two sorts, one also adds a relation symbol \(\mathsf{Univ}\rightarrowtail C^{[1]}\) to collect (via given axioms) all universal arrows; i.e. all units of the adjunction. Then we add an axiom stating that for any object of \(C\) there exists an element of \(\mathsf{Univ}\) (which is unique up to isomorphism) with domain the given object. When taking models in \(\mathsf{Cat}\) this is equivalent to asking the existence of a left adjoint to \(R\); since morphisms need to respect the relation symbol, the 2-category of models will be the same as \(\mathsf{Radj}\).

The same arguments apply for the 2-category \(\mathsf{Ladj}\) whose objects are left adjoint functors \(L\colon{\mathcal{C}}\to{\mathcal{D}}\), and where the morphism preserve universal arrows from \(L\) to \(d\in{\mathcal{D}}\).

As our final example consider the 2-category \(\mathsf{Mult}\) of multicategories, multifunctors, and multinatural transformations. To find an isoregular theory presenting \(\mathsf{Mult}\) we see the data of a multicategory \(M\) as:

• a category \(M_n\) of \(n\)-ary morphisms and multisquares between them, for any \(n\geq 0\), where \(0\)-ary morphisms are the objects;

• unit \(1\colon M_0\to M_1\), source \(s_n\colon M_n\to(M_0)^n\), and target \(t_n\colon M_n\to M_0\) functors (for any \(n> 0\));

• subcategories \(\mathsf{Comp}_{n}^{m_1,\cdots,m_n}\rightarrowtail M_n\times M_{m_1}\times\cdots\times M_{m_n}\times M_{m_1+\cdots m_n}\) to encode that
  \(\mathsf{Comp}_{n}^{m_1,\cdots,m_n}(f,g_1,\cdots,g_n,h)\) holds if and only if \(f\circ (g_1,\cdots,g_n)\) is well-typed and coincides with \(h\).

All of this data identifies a language \({\mathbb{L}}\). The existence of composites is expressed via unique existential quantification and is subject to axioms expressing associativity and unitality. Finally one also needs to add axioms saying that morphisms in \(M_n\) are just compatible \((n+1)\)-tuples of objects from \(M_1\). This suffices to decribe \(\mathsf{Mult}\).

From this, we can add relation symbols \(\mathsf{Rep_n}\rightarrowtail M_n\), for any \(n\geq 1\), collecting (via specific axioms) all strong universal arrows \(\eta:(x_1,\cdots, x_n)\to \hat{x}\) in the sense of [45]. If we further add an axiom saying that for any \(n\)-tuple of objects \((x_1,\cdots, x_n)\) there is a (unique up to isomorphism) strong universal arrow with source \((x_1,\cdots, x_n)\), we obtain an isoregular theory that present the 2-category \(\mathsf{RMult}\) of representable multicategories, multifunctors that preserve strong universal arrows, and multinatural transformations.

Since \(\mathsf{RMult}\) is 2-equivalent to the 2-category \(\mathsf{MonCat}\) of monoidal categories, strong monoidal functors, and monoidal natural transformations, we obtain a new proof that \(\mathsf{MonCat}\) is accessible with flexible limits, as shown in [14].

7 Directions for future work↩︎

The paper suggests several promising ideas, including possible generalisations of our results which we expect to be true, whose investigation we leave for future work.

Internal languages↩︎

Given a small isoregular 2-category \({\mathcal{C}}\), we expect to be possible do define an isoregular theory \({\mathbb{T}}_{\mathcal{C}}\) such that \[\mathsf{IsoReg}({\mathcal{C}},{\mathcal{K}})\simeq \mathsf{Mod}({\mathbb{T}}_{\mathcal{C}},{\mathcal{K}}) \mathrlap{,}\] for any isoregular 2-category \({\mathcal{K}}\). This would strengthen the view of isoregular 2-categories as the semantical counterpart of isoregular theories.

Barr’s embedding↩︎

Given a small isoregular 2-category \({\mathcal{C}}\), a natural question that arises is whether the evaluation 2-functor \[\mathsf{ev}\colon{\mathcal{C}}\longrightarrow [\mathsf{IsoReg}({\mathcal{C}},\mathsf{Cat}),\mathsf{Cat}]\] is fully faithful, generalising the ordinary embedding for regular categories proved by Barr [3]. We believe that an adaptation of the arguments in [46] could work in this context.

Such a theorem would be very important for at least two reasons. On one hand, it would imply a completeness theorem for isoregular logic relative to models in \(\mathsf{Cat}\). On the other, it would mean that isoregular categories could be captured in the context of lex-colimits [47], and all of the theory developed in that paper would apply.

Makkai’s conceptual completeness↩︎

Assuming to have proved an analogue of Barr’s embedding as above, then is easy to see that the evaluation 2-functor restricts to \[J\colon{\mathcal{C}}\longrightarrow \mathsf{FlexFilt}(\mathsf{IsoReg}({\mathcal{C}},\mathsf{Cat}),\mathsf{Cat})\] where the codomain is the full subcategory of \([\mathsf{IsoReg}({\mathcal{C}},\mathsf{Cat}),\mathsf{Cat}]\) spanned by those 2-functors that preserve flexible limits and filtered colimits. Is it possible to add exactness condition on \({\mathcal{C}}\) to enforce that \(J\) is a 2-equivalence? This would give a 2-dimensional version of Makkai’s theorem for Barr-exact categories [48].

Infinitary case↩︎

Let \(\lambda\) be a regular cardinal. One can then define “\(\lambda\)-isoregular” logic by allowing arities from \(\mathsf{Cat}_\lambda\) (the full subcategory of \(\mathsf{Cat}\) spanned by the \(\lambda\)-presentable objects) and \(\lambda\)-small conjunctions. Semantically this corresponds to asking an isoregular 2-category also to have all \(\lambda\)-small products (and hence all \(\lambda\)-small limits), plus the requirement that fully faithful regular epimorphisms are stable under \(\lambda\)-small products.

Then all the results of the paper, and possibly those envisaged in this section, should extend to the infinitary setting without major efforts. As a consequence, one would be able to characterise accessible 2-categories with flexible limits exactly as the 2-categories of models of infinitary isoregular theories in \(\mathsf{Cat}\).

8 Deduction rules for isoregular theories↩︎

As in 1-dimensional first-order logic, we assume the standard structural and equality rules (see for instance [27]). We also assume two rules expressing unitality and associativity of term substitution, which we do not spell out. All the other rules of isoregular logic are listed below.

Deduction rules for conjunction↩︎

Deduction rules for existential quantifiers↩︎

Terminal object rule↩︎

Deduction rules for restriction↩︎

Deduction rules for powers.↩︎

References↩︎

---

1. Pseudo-monadicity of 2-categories closely related to that of clans [24], is subject of ongoing work of Bourke and Jelínek.↩︎