Michael Shulman
2-categorical logic collated

The internal logic of a 2-topos (one-page version)

This page is a collected version that includes most of the sub-pages about 2-categorical logic, for ease of printing. Keep in mind that everything here is rough, much is missing, and not all of the pages were designed to be read sequentially, so you may have to skip around.

What is a 2-topos?

Of course, a 2-topos is the 2-categorical version of a topos. In other words, it is a (vertically) categorified topos. However, as we know, categorification, like quantization and groupoidification, is an art rather than a science; it depends on deciding what the crucial properties are of the thing we want to categorify.

The problem is especially acute for toposes, because of their many-faceted nature. To speak figuratively, which attributes of an elephant do we want to categorify? It isn’t even necessarily clear that there is a single beast which decategorifies to all the aspects of an elephant at once; perhaps we have 2-legs, 2-trunks, 2-ears, 2-tails, and so on but no actual 2-elephant.

According to WeberYS2T,

• a 2-topos is a finitely complete 2-category which is cartesian closed and has a duality involution and a classifying discrete opfibration.

This is evidently a categorification of a definition such as

• a topos is a finitely complete category which is cartesian closed and has a subobject classifier.

On the other hand, according to StreetCBS,

• a 2-topos is a 2-category which is equivalent to the 2-category of stacks (2-sheaves) on some 2-site.

This is evidently a categorification of a definition such as

• a topos is a category which is equivalent to the category of sheaves on some site.

The definition I propose to categorify is

• a topos is a locally cartesian closed, finitely complete and cocomplete Heyting pretopos with a subobject classifier.

Of course, this definition contains a good deal of redundancy, but not all of that was apparent in the early days of topos theory, and there seems less reason to believe that the redundancy will remain under categorification. Moreover, for the purposes of logic, having a Heyting pretopos is the most important part of the definition; it is what enables the internal interpretation of first-order logic. (Local cartesian closure and a subobject classifier then enable the interpretation of higher-order logic.) It may be simply an accident that in the 1-categorical case, the higher-order structure automatically implies the first-order structure.

Thus, in order to obtain an internal logic of a 2-category, it is natural to start with a notion of Heyting 2-pretopos. This is especially attractive because it is less clear how to categorify the “higher-order structure” of local cartesian closure and a subobject classifier. The 2-category Cat, which one expects to be the prototypical 2-topos just as Set is the prototypical topos, does not have a subobject classifier, nor is it locally cartesian closed (though it is cartesian closed). What is true is that fibrations are exponentiable, and that it has objects (namely, full subcategories of $\mathrm{Set}$) that classify some discrete opfibrations.

Another guiding desideratum for us will be that all the notions we consider should be stable under slicing, just like the corresponding 1-categorical notions. For instance, this demands the upgrading of ordinary cartesian closure to some sort of local cartesian closure. However, in the 2-categorical case it turns out that usually the correct notion to consider is not the slice 2-category but rather the fibrational slice.

Thus, the proposed definition we will arrive at will be something like:

• an (elementary) 2-topos is a finitely complete and cocomplete Heyting 2-pretopos with exponentials and (some sort of discrete opfibration classifier).

The goal, again, is to find a notion of 2-topos that has an internal logic in which we can reason about categories. Street’s “Grothendieck 2-toposes” turn out to have (almost) all of these properties of an “elementary 2-topos.” The intersection of this notion with Weber’s consists of finite limits, cartesian closure (strictly weaker than our notion of “exponentials”), and a discrete fibration classifier. While some of our 2-toposes admit duality involutions, others (perhaps surprisingly) do not.

On the meaning of ‘categorified logic’

In talking about 2-toposes and classifying discrete opfibrations it is common to hear people talk about “the category of sets being a generalized object of truth values,” or more loosely of “treating sets as truth values.” (See, for instance, the discussion at this post.) The idea, of course, is that just as the functor

$$X\mapsto \mathrm{Sub}(X)$$X\mapsto Sub(X)

from $\mathrm{Set}$ (or any topos) to posets is representable by the set $\Omega$ of truth values, the functor

$$X\mapsto \mathrm{DOpf}(X)$$X\mapsto DOpf(X)

from $\mathrm{Cat}$ (or, hypothetically, any 2-topos) to categories is representable by the category $\mathrm{Set}$ of sets. Here $\mathrm{DOpf}(X)$ means the category of discrete opfibrations over $X$.

My current opinion is that there already exists a “logic which treats sets as truth values,” without the need for any categorification, namely type theory (more precisely, dependent type theory). It is central to categorical logic (although not always presented in this way) that the internal logic of a category $C$ actually takes place in the fibration $X\mapsto \mathrm{Sub}(X)$ of subobjects of objects of $C$. In particular:

• The Heyting algebra operations in each poset $\mathrm{Sub}(X)$ correspond to the logical connectives $\wedge ,\vee ,\top ,\perp ,\Rightarrow ,\neg$.
• The reindexing functors $f^{*}:\mathrm{Sub}(Y)\to \mathrm{Sub}(X)$ correspond to logical substitution, weakening, and contraction.
• Left adjoints to reindexing functors correspond to existential quantification.
• Right adjoints to reindexing functors correspond to universal quantification.

The fact that the resulting logic is a “logic of truth values,” or as I would say a “logic of (-1,0)-categories,” depends on each $\mathrm{Sub}(X)$ being a poset; that is, a (0,1)-category. However, for an ordinary category $C$ we also have a fundamental fibration $X\mapsto C/X$ of 1-categories, which has a corresponding “logic of 0-categories,” that is, sets. If $C$ is (for instance) a locally cartesian closed category with finite colimits, then each $C/X$ is a cartesian closed category with finite colimits (the 1-categorical analogue of a Heyting algebra) and the reindexing functors have left and right adjoints.

Now, instead of interpreting these operations as acting on logical statements that are either true or false, we interpret them as acting on types which can be inhabited or empty, but if inhabited can contain many different elements. For instance, instead of constructing a new proposition $\phi \wedge \psi$ from propositions $\phi$ and $\psi$, we construct a new type $A\times B$ from types $A$ and $B$. And instead of constructing a new proposition $(\forall x\in A)\phi (x)$ from a proposition $\phi$ that depends on a variable $x$, we construct a new type ${\Pi }_{x\in A}B(x)$ (a “dependent product”) from a type $B(x)$ that depends on $x$.

There are several different ways of thinking about this. From one perspective, we can think of these types as merely “souped up” versions of propositions that record not only whether something is true, but all the “ways” in which it can be true or all the “proofs” that it is true. Thus, our real interest is in whether a given type is inhabited or not, which is a close generalization of whether a given proposition is true. I believe this is often called the propositions as types paradigm.

On the other hand, we can treat the types as sets whose different elements we may care about, and it is from this perspective that I want to view it. In this case, we may also want to say things about the elements of those sets, which is to say, we also need a logic (of propositions) on top of our type theory (the “logic of sets”). This construction of a “logic over a type theory” is very common in type theory, and seems to be the generally accepted way to develop the internal logic of a $\Pi$-pretopos. From an $n$-categorical point of view, what we have is a 1-category in which we have both a “logic of 0-categories” (type theory) that takes place in the slice categories $C/X$ and a “logic of (-1,0)-categories” (ordinary logic) that takes place in the slice posets ${\mathrm{Sub}}_C(X)$.

It is now clear how to categorify this: in a 2-category $K$ we will have a “logic of 1-categories” that takes place in the slice 2-categories $K/X$, a “logic of 0-categories” that takes place in the slice 1-categories $\mathrm{disc}(K/X)$, and a “logic of (-1,0)-categories” that takes place in the slice posets ${\mathrm{Sub}}_K(X)$. (Actually, we could easily add logics of (1,0)-categories and (0,1)-categories taking place in $\mathrm{gpd}(K/X)$ and $\mathrm{pos}(K/X)$, respectively, but this doesn’t seem to be as useful.) The only possibly-unexpected wrinkle is that it turns out to be best to ues the fibrational slices ${\mathrm{Fib}}_K(X)$ and ${\mathrm{Opf}}_K(X)$ in place $K/X$ whenever possible.

From this perspective, it is evident that in “categorified logic” (at least as I conceive it) sets do not replace truth values. Rather, sets, and categories as well, have their own “logic” (aka “type theory”) which happens “underneath” the logic of truth values. The goal is that just as existing mathematical arguments involving sets can be formalized in the internal logic of a 1-topos, existing mathematical arguments involving categories should be formalizable in the internal logic of a 2-topos — and, empirically speaking, these arguments involving categories still use the same sort of (truth-valued) logic that arguments involving sets do. The only difference is that they involve categories (1-types) in addition to sets (0-types) and truth values ((-1)-types).

Something that would help me enormously (personally and convincing other philosophers) would be a concrete example to work with. It would be especially interesting if this could be in ‘natural language’, like my poodle example for 1-logic.

Perhaps an example from dependent type theory would do: During every month there exists a team for which there exists a day in that month on which every player on that team is fit.

It would be nicer though to have the meta-types be non-discrete categories.

You could try the following paper by Isar Stubbe: The canonical topology on a meet-semilattice which explicitly goes from Omega to Sets.

2-categorical conventions

In line with the rest of the nLab, 2-category means weak 2-category, or precisely bicategory. All notions such as limits, adjunctions, equivalences, and so on are understood in a suitably weak sense (without need for a prefix such as “bi-“). Note that without choice, even Cat is not a strict 2-category, since we must use anafunctors instead of functors; see regular 2-categories and choice.

If X has a meaning for 1-categories, then if X is used without a prefix for 2-categories it should include the existing notion for 1-categories as a special case (when 1-categories are considered as homwise-discrete 2-categories). If we consider a notion related to X but which is not a “conservative categorification” in this sense, we will call it 2-X; cf. subcategory. For instance, we say regular 2-category since a 1-category is regular as a 2-category iff it is regular as a 1-category, but 2-exact 2-category since an exact 1-category is almost never 2-exact as a 2-category.

$n$-categories for $n\le 2$

In many cases it turns out to be just as easy to develop the theory not just for 2-categories, but for $(s,r)$-categories for some $0\le s\le 2$ and $r>0$. We will say that $n\le 2$ and $n$ is directed to mean that $n=(s,r)$ for some such $s,r$. This includes the following cases:

2 = (2,2)

of course, a 2-category is just a 2-category

(2,1)

A (2,1)-category is a 2-category all of whose 2-cells are invertible, such as Gpd.

(1,2)

A (1,2)-category is a 2-category in which any two parallel 2-cells are equal, such as Pos.

1 = (1,1)

A 1-category is a 2-category in which any two parallel 2-cells are equal and invertible; that is, a 2-category which is both a (2,1)-category and a (1,2)-category. This means its hom-categories are equivalent to discrete sets, so it can be identified with a 1-category in the usual sense.

(0,1)

A (0,1)-category is a poset, or more precisely a preordered set.

The following values of $n=(s,r)$ are considered $\le 2$, but are not directed.

(2,0)

A (2,0)-category is a 2-groupoid: a 2-category in which all 2-cells are isomorphisms and all 1-cells are equivalences.

(1,0)

A (1,0)-category is a groupoid.

0=(0,0)

A 0-category is a set (or a category, or 2-category, that is equivalent to one).

-1 = (-1,0)

A (-1,0)-category is poset in which any two objects are isomorphic; thus it is a truth value (the truth value of “there exists an object”). Since there is no useful notion of (-1,-1)-category, (-1,0)-categories are often called (-1)-categories and we will sometimes use this convention.

-2 = (-2,-1)

A (-2,-1)-category is an inhabited (-1,0)-category; that is, it is the truth value “true.” As with (-1)-categories, (-2,-1)-categories are often called simply (-2)-categories.

These values of $n$ are also important, but for them one doesn’t expect a notion of $n$-topos, nor of regularity, exactness, extensivity, or an internal logic. For instance, a nontrivial groupoid has no limits, so it certainly cannot be regular.

Actually, I’ve been mildly surprised not to see you use these values of $n$. Sure, the concepts tend to be trivial then, but so they also tend to be when $n<0$.

And actually, I don't think it's appropriate to refer to $n<0$ as ‘directed’. Directedness is provided only by $r>0$.

—Toby

You’re right about directedness; I’ve fixed the page. What sort of “use” of nondirected $n$ were you expecting? They do come up, of course; for instance it’s important to talk about $n$-truncated objects when $n$ is not necessarily directed. The only point is that no nontrivial $n$-categories can be regular, exact, coherent, etc. unless $n$ is directed.

I guess it might be useful to distinguish $n$-truncated 2-toposes even when $n$ is not directed. For instance, 0-truncated (Grothendieck) 2-toposes are just powers of $\mathrm{Cat}$, and (1,0)-truncated 1-toposes are toposes of actions by a groupoid. But you can’t say any more that an $n$-truncated 2-topos is the category of 2-sheaves on an $n$-topos, since there is no longer any notion of $n$-topos.

I incorporated your other comments into the text. -Mike

By ‘use’ I meant at a minimum ‘mention’. That is, remark that no groupoid is regular, etc. Mind you, I've been only mildly surprised not to see this (and such surprise as I had came in part because you sometimes did mention $n\le 0$); I like to mention degenerate cases, but I know that others don't. Possibly we can regard the paragraph above as covering it now. —Toby

We adopt the natural convention that $(s,r)\pm 1=(s\pm 1,r\pm 1)$. Thus, for instance, saying that $n$-categories form an $(n+1)$-category includes the statements that:

• sets form a 1-category
• categories form a 2-category
• groupoids form a (2,1)-category
• posets form a (1,2)-category
• truth values form a poset

and so on. For this convention it is important to remember that (-1)-category is a shorthand for (-1,0)-category, so that $(-1)+1=(0,1)$, not (0,0). And of course, $(-2)+1=(-1)$. Note that $n$ is directed if and only if it is of the form $m+1$ for some $m\ge (-1,0)$.

Note that $(s,r)$-categories are the same as $(s,r\prime )$-categories whenever either $r,r\prime \ge s+1$ or $r,r\prime \le 0$. (Although for monoidal categories, $r=-1$ and $r=0$ can be distinguished.) Thus, to avoid duplication, usually one restricts to $0\le r\le s+1$. However, these requirements conflict when $s=-2$ (which is something of a special case in other ways as well). We choose -2 to mean (-2,-1) so that we obtain (-1,0) upon adding 1 to it, although (-2,0) would work just as well as long as we remember that (0,2) and (0,1) are the same. Thus, our general restriction on $r$ and $s$ is $\min (0,s+1)\le r\le s+1$.

Discussion

From a previous discussion at truncated object, which doesn't really belong there:

Yes, definitely. A so called ‘$-1$-category’ (a truth value) is really a $-1$-groupoid or a $0$-poset, that is a $(-1,0)$-category, not a $(-1,-1)$-category (which doesn't really make sense) at all. As you know. —Toby

Yeah. But (-1,0)-category is cumbersome to say when there is no different notion of (-1)-category that it needs to be distinguished from. (-: And it seems to break down at (-2) anyway; for the adding-one convention to continue to work we should write (-2,-1)-category instead of (-2)-category, but that doesn’t make sense in the general scheme of (n,r)-category. I suppose we could decide to write $(n,\mathrm{\infty })$ instead of $(n,n+1)$ in all cases… -Mike

Partly, this would work better if we said ‘$n$-poset’ all the time for various values of $n$. In general, an $(r,s)$-category is an $(r+1,s)$-poset. The bad part is that now these pages focus on $n\le (3,2)$, which is not so slick to say. But the general theory works better; we require $0\le s\le r$ (with the same exception as before, now when $r=-1$) and no glitch crossing from $-1$ to $-2$. —Toby

I suppose so, but I don’t think you’ll have much luck trying to get people to say “(3,2)-poset” instead of “2-category.” (-: -Mike

Nothing wrong with ‘$2$-category’, ‘$2$-groupoid’, etc as abbreviations, but we shouldn't lose sight of the fundamental concept. (Similarly, wasn't someone trying to come up with a general name for $(n,1)$-category?) —Toby

What are you claiming is the “fundamental concept?” The only candidates for a fundamental concept that I see are either full-blown $\omega$-categories or $(s,r)$-categories for arbitrary $s,r$. The only remaining question is terminology, and I think saying that “2-category” is an abbreviation for “(2,2)-category” is much more likely to catch on than saying that it is an abbreviation for “(3,2)-poset.” (In fact, it has already caught on.) In particular, there is a virtue to continuing to use the word “category,” which communicates the behavior of these things much better than “poset.” Already I think “(1,2)-category” is a more descriptive name than “2-poset.” -Mike

I agree with Toby that one should say ”$(r+1,s)$-order” (I don’t use “poset”, since this word suggests that they have a set of objects) rather than ”$(n,r)$-category” and even $V$-order instead of $V$-category, because the word “category” carries the further meaning that there is some groupoidality (the homs are groupoidal orders in a category). For this reason, I think that “order” conveys better the general behaviour than “category”. The most fundamental concepts, for me, are the $n$-orders, which are the most general $\omega$-orders of dimension $n$. The study of higher-dimensional toposes would perhaps be more natural if the reference cases were modelled on Ord and 2-Ord rather than Set and Cat. —Mathieu

I disagree that “category” carries the meaning of groupoidality in the homs. I suppose it can mean whatever you choose it to mean, like Humpty Dumpty, but there is nothing in the past usage of the word “category” to suggest such an implication. Just because $n$-categories, for natural numbers $n$, happen to have homs that are groupoidal at the top dimension for which they have unequal parallel morphisms doesn’t mean that “category” necessarily implies such groupoidality. If in addition to 2-categories we allow (2,1)-categories then (2,3)-categories are just as natural. The existing meaning of $V$-category includes categories enriched over orders (= (1,2)-categories) and categories enriched over truth values (= (0,1)-categories); why not allow “category” its existing, more inclusive, meaning?

Also, even in an $n$-order (= $(n-1,n)$-category) there is some groupoidality; it just doesn’t kick in until the $(n+1)$-cells. To me, a much stronger intuitive association is that “order” implies that parallel morphisms are equal. This is not true for $n$-orders for any $n>1$, except at the $n$-cells, and is not true for any dimension of cells in an $\omega$-order (= $\omega$-category). -Mike

My use of the phrase ‘fundamental concept’ was tongue in cheek, since (as you point out) it is the same concept. At best, one can say that the partial function from $Z\times Z$ to properties of $\mathrm{\infty }$-categories that maps $(s,r)$ to being an $(s,r)$-poset (or $(s,r)$-order) is simpler (hence should be regarded as more fundamental, with the other defined in terms of it) than the partial function that maps $(s,r)$ to being an $(s,r)$-category. Certainly the domain of the first partial function is nicer. So if we were inventing terminology afresh for the whole business, we would probably want to base it on that function. Even in the real world, where I titled an article (n,r)-category, one should talk about $(s,r)$-posets when that helps explain a pattern.

Also, we're not going to get anywhere talking about the limiting connotations that various words have. Of course ‘category’ has the connotation of being groupoidal at and above level $2$, since an ordinary category is groupoidal at and above level $2$; and ‘order’ and ‘poset’ have the connotation of being trivial at and above level $2$, since an ordinary order or poset is trivial at and above level $2$. (But I don't see what's wrong with the connotation that a poset has an underlying set, since even an $\mathrm{\infty }$-poset has an underlying set of equivalence classes of objects.) Any terminology that we choose to generalise will have limiting connotations from its previous use.

I think this is the last I'll say on the matter; it's not like I'm not trying to get Mike to renumber his work here.

—Toby

Regularity without choice

The 1-category $\mathrm{Set}$ is a 1-topos, and in particular regular, without any need for the axiom of choice, or indeed even any need for classical logic. Even predicativists generally agree that $\mathrm{Set}$ is a pretopos.

However, at first glance, the axiom of choice seems to be necessary in order for $\mathrm{Cat}$ to be a regular 2-category. Specifically, given a commutative square of functors

$$\begin{array}{ccc}A& \stackrel{f}{\to }& C\\ e\downarrow & & \downarrow m\\ B& \underset{g}{\to }& D\end{array}$$\array{A & \overset{f}{\to} & C\\ e \downarrow && \downarrow m\\ B& \underset{g}{\to} & D}

in which $m$ is full and faithful and $e$ is essentially surjective, in order to define a lift $h:B\to C$ we have to first choose, for each $b\in B$, an object $a_b\in A$ and an isomorphism $e(a_b)\cong b$, then defining $h(b)=f(a_b)$ with its action on morphisms determined by $g$ (since $m$ is ff).

Of course, there is a sense in which this is not a “real” use of choice, since $f(a_b)$ is determined by $b$ up to unique isomorphism. It is well-established that in the absence of choice, the usual notion of functor is too strict, and one should instead use anafunctors which determine their values only up to unique isomorphism. And it is not hard to check that if we define $\mathrm{Cat}$ to be the (no longer strict) 2-category of categories, anafunctors, and natural transformations, then it is regular, and in fact a 2-pretopos, without any need for choice.

Discussion on cartesian closure

Toby: Something to consider: In Makkai's paper on anafunctors, he needs a (fairly weak) form of the axiom of choice to conclude that the bicategory of categories, and anafunctors, and ananatural transformations is cartesian closed. Maybe the right notions of exponentials don’t require even this.

Mike: Interesting point! Of course, in the absence of choice, one has to use anafunctors in order for $\mathrm{Cat}$ to even be a regular 2-category, so this is an important question. However, it seems to me that his proof actually shows that without any choice at all, $\mathrm{Cat}$ (his $\mathrm{AnaCat}$) is cartesian closed in the sense that there is an anaequivalence $\mathrm{Cat}(A\times B,C)\simeq \mathrm{Cat}(A,C^B)$, and this is all one ought to need or want. Am I wrong?

Toby: But without that SCSA thing, I don't know what $C^B$ means in this context. That is, the category of small anafunctors from a small category $B$ to a small category $C$ is not itself small (at least not if $B$ is inhabited), and Makkai uses SCSA to prove the existence of an equivalent small category.

Now that I look at this stuff closely again, it seems unlikely to shed much light on the matter here. But there it is.

Mike: If you trace through his proof, it seems to me that what he really shows is that (without any choice) any anafunctor $X\to A$ is isomorphic to one whose set of specifications is of the form

$$\coprod _{(x,a)\in S}\mathrm{Iso}(a,a)$$\coprod_{(x,a)\in S} Iso(a,a)

for some $S\subset \mathrm{Ob}(X)\times \mathrm{Ob}(A)$. And there is clearly a set of these, so the full subcategory of $\mathrm{Cat}(X,A)$ on them should be an exponential $A^X$ in $\mathrm{Cat}$.

You only need choice if you want there to be a function assigning to each anafunctor $X\to A$ an isomorphism to one of the above form. And you can avoid using the full strength of choice by allowing yourself to replace $\mathrm{Iso}(a,a)$ by anything in some specified set of sets that are isomorphic to it.

Mike: No, what I said in the previous comment is wrong! What’s true is that for any saturated anafunctor $F$, the set $\mid F\mid (x,a)$ of specifications from $x$ to $a$ is, if inhabited, isomorphic to $\mathrm{Iso}(a,a)$. However, that isomorphism is non-canonical (to be precise, $\mid F\mid (x,a)$ is a torsor over $\mathrm{Iso}(a,a)$). Thus, in order to to replace your anafunctor by one whose set of specifications is of the above form, you need to choose simultaneously, for every $x$ and $a$ such that $\mid F\mid (x,a)$ is inhabited, an isomorphism $\mid F\mid (x,a)\stackrel{\cong }{\to }\mathrm{Iso}(a,a)$, and that requires some choice. Where SCSA is weaker than AC is that you don’t need to be able to choose isomorphisms to $\mathrm{Iso}(a,a)$, you just need to be able to choose isomorphisms to something such that there is at most a set of targets of the somethings, and that’s enough to make the category of anafunctors essentially small.

Right now I feel as though even in the absence of choice, $\mathrm{Cat}$ “ought” to have all these good properties, including cartesian closure. If anafunctors aren’t good enough to recover all of that without some form of choice, then maybe that just means that even with anafunctors, set-theoretic foundations just aren’t fully capable of mimicking truly categorial foundations.

David Roberts: Clearly WISC has some bearing here (and probably the kernel of the idea originated from this discussion). Is there a 2-categorical form of WISC? Is it useful? I suppose this depends on the analogue of what is considered 'small' in the 2-logic

Slice 2-categories

The slice 2-category of a 2-category $K$ over an object $X$ is the 2-category whose objects are morphisms $A\to X$ in $K$, whose morphisms are triangles in $K$ that commute up to a specified isomorphism, and whose 2-cells are 2-cells in $K$ forming a commutative 2-diagram with the specified isomorphisms in triangles.

In particular, any 2-cell in $K/X$ must become an isomorphism in $X$. This means that more information is lost when passing to slice 2-categories than for slice 1-categories, and slice 2-categories are not always well-behaved; they often fail to inherit useful properties of $K$. Frequently a better replacement is the fibrational slice.

Pullbacks and adjoints

If $K$ has pullbacks, then for any $f:X\to Y$ there is a pullback functor $f^{*}:K/Y\to K/X$. However, this does not make the assignation $X\mapsto K/X$ into a functor $K^{\mathrm{op}}\to \mathrm{Cat}$ or $K^{\mathrm{coop}}\to \mathrm{Cat}$, since there is no way to define it on 2-cells. This is one reason to use fibrational slices instead.

Just as in the 1-categorical case, the pullback functor $f^{*}:K/Y\to K/X$ always has a left adjoint ${\Sigma }_f:K/X\to K/Y$ given by composition with $f$. However, $f^{*}$ cannot be expected to have a right adjoint ${\Pi }_f$ for all maps $f$, since this fails even in $\mathrm{Cat}$. It is true in $\mathrm{Cat}$ when $f$ is a fibration or opfibration, however; see exponentials in a 2-category.

Fibrational slices

Definition

The fibrational slice of a 2-category $K$ over an object $X$ is the homwise-full sub-2-category $\mathrm{Fib}(X)$ of the slice 2-category $K/X$ whose objects are fibrations over $X$ and whose morphisms are morphisms of fibrations. Likewise, we have the opfibrational slice $\mathrm{Opf}(X)$ consisting of opfibrations.

The fibrational and opfibrational slices in a 2-category often play the role of the ordinary slice categories of a 1-category, replacing the ordinary slice 2-category. On this whole page we assume that $K$ has finite limits.

Basic properties

The 2-category $\mathrm{Opf}(X)$ is monadic over $K/X$. The relevant monad on $K/X$ takes $p:A\to X$ to the comma object $(p/1_X)$, or equivalently the pullback $A{\times }_X{X}^2$. It is lax-idempotent, so a morphism $p:A\to X$ is an opfibration if and only if $A\to (p/1_X)$ has a left adjoint with invertible counit in $K/X$. Likewise, $p$ is a fibration iff $A\to (1_X/p)$ has a right adjoint with invertible unit in $K/X$.

Since the fibrational slices are monadic over $K/X$, they inherit all limits from it. It follows that a fibration is a discrete object in $\mathrm{Fib}(X)$ iff it is discrete in $K/X$. These are unsurprisingly called discrete fibrations; we write $\mathrm{DFib}(X)$ for the category of such. Every morphism in $K/X$ between discrete fibrations is a morphism of fibrations; thus $\mathrm{DFib}(X)$ is a full subcategory of both $\mathrm{Fib}(X)$ and $K/X$.

Any pullback of an (op)fibration is again an (op)fibration. Therefore, any morphism $f:Y\to X$ induces a pullback functor $f^{*}:\mathrm{Fib}(X)\to \mathrm{Fib}(Y)$, which restricts to a functor $f^{*}:\mathrm{DFib}(X)\to \mathrm{DFib}(Y)$, and dually. Regarding the existence of adjoints to these functors, see comprehensive factorization and exponentials in a 2-category.

Any morphism with groupoidal codomain is a fibration and opfibration. Therefore, if $X$ is groupoidal, $\mathrm{Fib}(X)\simeq K/X\simeq \mathrm{Opf}(X)$. In particular, for (2,1)-categories and thus also for 1-categories, the fibrational slices are no different from the ordinary slices.

Subobjects

Central for us is the following fact, which would be false if we replaced $\mathrm{Opf}(X)$ by $K/X$. It underlies the inheritance of all sorts of structure by fibrational slices, such as regularity, coherency, extensivity, and exactness.

Theorem

A morphism in $\mathrm{Opf}(X)$ is ff in $\mathrm{Opf}(X$) iff its underlying morphism in $K$ is ff.

Proof

Suppose that $a:A\to X$ and $b:B\to X$ are opfibrations, and that $fmapsA\to B$ is a morphism in $\mathrm{Opf}(X)$ which is ff in $K$. Then since $\mathrm{Opf}(X)\to K$ is homwise faithful, $f$ is clearly faithful in $\mathrm{Opf}(X)$. And given a 2-cell $\alpha :h\to k:T\rightrightarrows B$ in $\mathrm{Opf}(X)$, since $f$ is ff in $K$, we must have $\alpha =f\beta$ for some 2-cell $\beta :j\to l:T\rightrightarrows A$. But then $a\beta \cong bf\beta =b\alpha$, so $\beta$ must also be a 2-cell in $\mathrm{Opf}(X)$.

Conversely, suppose that $f$ is ff in $\mathrm{Opf}(X)$, and that we have 2-cells $\alpha ,\beta :x\rightrightarrows y:T\rightrightarrows A$ in $K$ such that $f\alpha =f\beta$. Then since $bf\cong a$ we have $aalph=a\beta$; call this 2-cell $\xi :ax\to ay$. Since $a$ and $b$ are opfibrations and $f$ is a map of opfibrations, we have an opcartesian 2-cell $x\to {\xi }_{!}(x)$ lying over $\xi$ such that $fx\to f{\xi }_{!}(x)$ is also opcartesian. Then $\alpha$ and $\beta$ both factor through $x\to {\xi }_{!}(x)$ to give 2-cells $\gamma ,\delta :{\xi }_{!}(x)\rightrightarrows y$ in $\mathrm{Opf}(X)$ whose images under $f$ are equal. Since $f$ is faithful in $\mathrm{Opf}(X)$, we have $\gamma =\delta$, and hence $\alpha =\beta$. Thus, $f$ is faithful in $K$. The proof of fullness is analogous.

Therefore, if $A\to X$ is an (op)fibration in $K$, we have ${\mathrm{Sub}}_{\mathrm{Opf}(K)}(A)\subset {\mathrm{Sub}}_K(A)$, although in general the inclusion is proper. Of course, the dual result about $\mathrm{Fib}(X)$ is also true.

Iterated fibrations

It is well-known that a composite of fibrations is a fibration. Moreover:

Theorem

A morphism in $\mathrm{Fib}(X)$ is a fibration in the 2-category $\mathrm{Fib}(X)$ iff its underlying morphism in $K$ is a fibration.

This is a standard result, at least in the case $K=\mathrm{Cat}$, and is apparently due to Benabou. References include:

• J. Benabou, “Fibered categories and the foundations of naive category theory”
• B. Jacobs, Categorical Logic and Type Theory, Chapter 9
• C. Hermida, “Some properties of Fib as a fibred 2-category”

Therefore, for any fibration $A\to X$ in $K$ we have ${\mathrm{Fib}}_K(A)\simeq {\mathrm{Fib}}_{{\mathrm{Fib}}_K(X)}(A\to X)$, and similarly for opfibrations. This is a fibrational analogue of the standard equivalence $K/A\simeq (K/X)/(A\to X)$ for ordinary slice categories. It also implies that any morphism between discrete fibrations over $X$ is itself a (discrete) fibration in $K$, since in $\mathrm{Fib}(X)$ it has a discrete (hence groupoidal) target and thus is a fibration there.

We will also need the corresponding result for mixed-variance iterated fibrations, which seems to be less well-known. First we recall:

Definition

A span $A\stackrel{p}{\leftarrow }E\stackrel{q}{\to }B$ is called a (two-sided) fibration from $B$ to $A$ if

1. $q$ is an opfibration and $p$ takes $q$-opcartesian 2-cells to isomorphisms,

2. $p$ is a fibration and $q$ takes $p$-cartesian 2-cells to isomorphisms, and

3. for any $e:X\to E$, and any square

   $$\begin{array}{ccccc}& & {\alpha }^{*}e& \stackrel{p-\mathrm{cartesian}}{\to }& e\\ {}^{q-\mathrm{opcartesian}}& \swarrow & & & \downarrow & {}^{q-\mathrm{opcartesian}}\\ ({\alpha }^{*}e){\beta }_{!}& \to & {\alpha }^{*}(e{\beta }_{!})& \stackrel{p-\mathrm{cartesian}}{\to }& e{\beta }_{!}\end{array}$$\array{&& \alpha^*e & \overset{p-cartesian}{\to} & e\\ ^{q-opcartesian} & \swarrow && & \downarrow & ^{q-opcartesian}\\ (\alpha^* e)\beta_! & \to & \alpha^* (e \beta_!) & \overset{p-cartesian}{\to} & e \beta_!}

   of 2-cells, $({\alpha }^{*}e){\beta }_{!}\to {\alpha }^{*}(e{\beta }_{!})$ is an isomorphism.

Such two-sided fibrations in $\mathrm{Cat}$ correspond to functors $B\times A^{\mathrm{op}}\to \mathrm{Cat}$. The third condition corresponds precisely to the “interchange” equality $(\beta ,1)(1,\alpha )=(1,\alpha )(\beta ,1)$ in $B\times A^{\mathrm{op}}$. We write $\mathrm{Fib}(B,A)$ for the 2-category of two-sided fibrations from $B$ to $A$.

Theorem

A span $A\stackrel{p}{\leftarrow }E\stackrel{q}{\to }B$ is a two-sided fibration from $B$ to $A$ if and only if

1. $p:E\to A$ is a fibration and
2. $(p,q):E\to A\times B$ is an opfibration in $\mathrm{Fib}(A)$.

Proof

Recall that the projection $A\times B\to A$ is a fibration (and also an opfibration, although that is irrelevant here), and the cartesian 2-cells are precisely those whose component in $B$ is an isomorphism. Therefore, saying that $(p,q)$ is a morphism in $\mathrm{Fib}(A)$, i.e. that it preserves cartesian 2-cells, says precisely that $q$ takes $p$-cartesian 2-cells to isomorphisms.

Now, by the remarks above, $q$ is an opfibration in $K$ iff $E\to (q/1_B)$ has a left adjoint with invertible counit in $K/B$, and $(p,q)$ is an opfibration in $\mathrm{Fib}(A)$ iff $E\to ((p,q)/1_{A\times B})$ has a left adjoint with invertible counit in $\mathrm{Fib}(A)/(A\times B)$. Of crucial importance is that here $((p,q)/1_{A\times B})$ denotes the comma object calculated in the 2-category $\mathrm{Fib}(A)$, or equivalently in $K/A$, and it is easy to check that this is in fact equivalent to the comma object $(q/1_B)$ calculated in $K$.

Therefore, $(p,q)$ is an opfibration in $\mathrm{Fib}(A)$ iff $q$ is an opfibration in $K$ and the left adjoint of $E\to (q/1_B)$ is a morphism in $\mathrm{Fib}(A)$. It is then easy to check that this left adjoint is a morphism in $K/A$ iff $p$ inverts $q$-opcartesian arrows, and that it is a morphism of fibrations iff the final condition in Definition 1 is satisfied.

In particular, we have $\mathrm{Fib}(B,A)\simeq {\mathrm{Opf}}_{\mathrm{Fib}(A)}(A\times B)$. By duality, $\mathrm{Fib}(B,A)\simeq {\mathrm{Fib}}_{\mathrm{Opf}(B)}(A\times B)$, and therefore ${\mathrm{Fib}}_{\mathrm{Opf}(B)}(A\times B)\simeq {\mathrm{Opf}}_{\mathrm{Fib}(A)}(A\times B)$, a commutation result that is not immediately obvious.

It follows that the 2-categories $\mathrm{Fib}(B,A)$ of two-sided fibrations also inherit any properties that can be shown to be inherited by the “one-sided” fibrational slices $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$. Thus, we will usually concentrate on the latter, although two-sided fibrations will make an appearance in our treatment of duality involutions.

2-congruences

Idea

The correct notions of regularity and exactness for 2-categories is one of the subtler parts of the theory of first-order structure. In particular, we need a suitable replacement for the 1-categorical notion of equivalence relation. The (almost) correct definition was probably first written down in StreetCBS.

One way to express the idea is that in an $n$-category, every object is internally a $(n-1)$-category; exactness says that conversely every “internal $(n-1)$-category” is represented by an object. When $n=1$, an “internal 0-category” means an internal equivalence relation; thus exactness for 1-categories says that every equivalence relation is a kernel (i.e. is represented by some object). Thus, we need to find a good notion of “internal 1-category” in a 2-category.

Of course, there is an obvious notion of an internal category in a 2-category, as a straightforward generalization of internal categories in a 1-category. But internal categories in Cat are double categories, so we need to somehow cut down the double categories to those that really represent honest 1-categories. These are the 2-congruences.

Definition

If $K$ is a finitely complete 2-category, a homwise-discrete category in $K$ consists of a discrete morphism $D_1\to D_0\times D_0$, together with composition and identity maps $D_0\to D_1$ and $D_1{\times }_{D_0}{D}_1\to D_1$ in $K/(D_0\times D_0)$, which satisfy the usual axioms of an internal category up to isomorphism. (Since $D_1\to D_0\times D_0$ is discrete, these isomorphisms will automatically satisfy any coherence axioms one might care to impose.)

The notions of functor and transformation between such categories are evident. The first point worth noting is that the transformations between functors $D\to E$ are a version of the notion for internal categories, thus given by a morphism $D_0\to E_1$ in $K$. The 2-cells in $K(D_0,E_0)$ play no explicit role, but we will recapture them below. The second point worth noting is that by homwise-discreteness, any “modification” between transformations is necessarily a unique isomorphism, so (after performing some quotienting, if we want to be pedantic) we really have a 2-category $\mathrm{HDC}(K)$ rather than a 3-category.

If $f:A\to B$ is any morphism in $K$, there is a canonical homwise-discrete category $(f/f)\to A\times A$, where $(f/f)$ is the comma object of $f$ with itself. We call this the kernel $\ker (f)$ of $f$. In particular, if $f=1_A$ then $(1_A/1_A)=A^2$, so we have a canonical homwise-discrete category $A^2\to A\times A$ called the kernel $\ker (A)$ of $A$. It is easy to check that taking kernels of objects defines a functor $\Phi :K\to \mathrm{HDC}(K)$; this might first have been noticed by Street.

Theorem

If $D_1\rightrightarrows D_0$ is a homwise-discrete category in $K$, the following are equivalent.

1. $D_0\leftarrow D_1\to D_0$ is a two-sided fibration in $K$.
2. There is a functor $\ker (D_0)\to D$ whose object-map $D_0\to D_0$ is the identity.

Actually, homwise-discreteness is not necessary for this result, but we include it to avoid worrying about coherence isomorphisms, and since that is the case we are most interested in here.

Proof

We consider the case $K=\mathrm{Cat}$; the general case follows because all the notions are defined representably. A homwise-discrete category in $\mathrm{Cat}$ is, essentially, a double category whose horizontal 2-category is homwise-discrete (hence equivalent to a 1-category). We say “essentially” because the pullbacks and diagrams only commute up to isomorphism, but up to equivalence we may replace $D_1\to D_0\times D_0$ by an isofibration, obtaining a (pseudo) double category in the usual sense. Now the key is to compare both properties to a third: the existence of a companion for any vertical arrow.

Suppose first that $D_0\leftarrow D_1\to D_0$ is a two-sided fibration. Then for any (vertical) arrow $f:x\to y$ in $D_0$ we have cartesian and opcartesian morphisms (squares) in $D_1$:

(1)$$\begin{array}{ccccccc}x& \stackrel{\mathrm{id}}{\to }& x& & x& \stackrel{f_1}{\to }& y\prime \\ \cong \downarrow & \mathrm{opcart}& \downarrow f& & f\downarrow & \mathrm{cart}& \downarrow \cong \\ x\prime & \stackrel{f_2}{\to }& y& & y& \stackrel{\mathrm{id}}{\to }& y\end{array}$$\array{x & \overset{id}{\to} & x & \qquad & x & \overset{f_1}{\to} & y' \\ \cong \downarrow & opcart & \downarrow f & \qquad & f \downarrow & cart & \downarrow \cong\\ x' & \overset{f_2}{\to} & y & \qquad & y & \overset{id}{\to} & y}

The vertical arrows marked as isomorphisms are so by one of the axioms for a two-sided fibration. Moreover, the final compatibility axiom for a 2-sided fibration says that the square

(2)$$\begin{array}{ccc}x& \stackrel{f_1}{\to }& y\prime \\ \cong \downarrow & & \downarrow \cong \\ x\prime & \stackrel{f_2}{\to }& y,\end{array}$$\array{ x & \overset{f_1}{\to} & y'\\ \cong \downarrow & & \downarrow\cong \\ x' & \overset{f_2}{\to} & y,}

induced by factoring the horizontal identity square of $f$ through these cartesian and opcartesian squares, must be an isomorphism. We can then show that $f_1$ (or equivalently $f_2$) is a companion for $f$ just as in Theorem 4.1 here. Conversely, from a companion pair we can show that $D_0\leftarrow D_1\to D_0$ is a two-sided fibration just as as in loc cit.

The equivalence between the existence of companions and the existence of a functor from the kernel of $D_0$ is essentially found in this paper, although stated only for the “edge-symmetric” case. In their language, a kernel $\ker (A)$ is the double category $\square A$ of commutative squares in $A$, and a functor $\ker (D_0)\to D$ which is the identity on $D_0$ is a thin structure on $D$. In one direction, clearly $\ker (D_0)$ has companions, and this property is preserved by any functor $\ker (D_0)\to D$. In the other direction, sending any vertical arrow to its horizontal companion is easily checked to define a functor $\ker (D_0)\to D$.

In particular, we conclude that up to isomorphism, there can be at most one functor $\ker (D_0)\to D$ which is the identity on objects.

Definition

A 2-congruence in a finitely complete 2-category $K$ is a homwise-discrete category in $K$ satisfying the equivalent conditions of Theorem 4.

Of course, the kernel $\ker (A)$ of any object is a 2-congruence. More generally it is easy to see that the kernel $\ker (f)$ of any morphism is also a 2-congruence.

2-Forks and Quotients

The idea of a 2-fork is to characterize the structure that relates a morphism $f$ to its kernel $\ker (f)$. The kernel then becomes the universal 2-fork on $f$, while the quotient of a 2-congruence is the couniversal 2-fork constructed from it.

Definition

A 2-fork in a 2-category consists of a 2-congruence $s,t:D_1\rightrightarrows D_0$, $i:D_0\to D_1$, $c:D_1{\times }_{D_0}{D}_1\to D_1$, and a morphism $f:D_0\to X$, together with a 2-cell $\varphi :fs\to ft$ such that $\varphi i=f$ and such that

$$\begin{array}{ccccc}{D}_1{\times }_{D_0}{D}_1& \to & D_1& =& D_1\\ \downarrow & & \downarrow & {\Downarrow }_{\varphi }& \downarrow \\ D_1& \to & D_0& & D_0\\ \mid \mid & {\Downarrow }_{\varphi }& & {\searrow }^f& \downarrow f\\ D_1& \to & D_0& \stackrel{f}{\to }& X\end{array}=\begin{array}{c}{D}_1{\times }_{D_0}{D}_1\\ & {\searrow }^c\\ & & D_1& \to & D_0\\ & & \downarrow & {\Downarrow }_{\varphi }& \downarrow f\\ & & D_1& \stackrel{f}{\to }& X.\end{array}$$\array{ D_1\times_{D_0} D_1 & \to & D_1 & = & D_1\\ \downarrow && \downarrow & \Downarrow_\phi & \downarrow\\ D_1 & \to & D_0 && D_0\\ || &\Downarrow_\phi && \searrow^f & \downarrow f\\ D_1 & \to & D_0 & \overset{f}{\to} & X } \qquad = \qquad \array{ D_1\times_{D_0} D_1 \\ & \searrow^c\\ && D_1 & \to & D_0\\ && \downarrow & \Downarrow_\phi & \downarrow f\\ && D_1 & \overset{f}{\to} & X. }

The comma square in the definition of the kernel of a morphism $f:A\to B$ gives a canonical 2-fork

$$(f/f)\rightrightarrows A\stackrel{f}{\to }B.$$(f/f) \;\rightrightarrows\; A \overset{f}{\to} B.

It is easy to see that any other 2-fork

$$D_1\rightrightarrows D_0=A\stackrel{f}{\to }B$$D_1 \;\rightrightarrows\; D_0 = A \overset{f}{\to} B

factors through the kernel by an essentially unique functor $D\to \ker (f)$ that is the identity on $A$.

If $D_1\rightrightarrows D_0\stackrel{f}{\to }X$ is a 2-fork, we say that it equips $f$ with an action by the 2-congruence $D$. If $g:D_0\to X$ also has an action by $D$, say $\psi :gs\to gt$, a 2-cell $\alpha :f\to g$ is called an action 2-cell if $(\alpha t).\varphi =\psi .(\alpha s)$. There is an evident category $\mathrm{Act}(D,X)$ of morphisms $D_0\to X$ equipped with actions.

Definition

A quotient for a 2-congruence $D_1\rightrightarrows D_0$ in a 2-category $K$ is a 2-fork $D_1\rightrightarrows D_0\stackrel{q}{\to }Q$ such that for any object $X$, composition with $q$ defines an equivalence of categories

$$K(Q,X)\simeq \mathrm{Act}(D,X).$$K(Q,X) \simeq Act(D,X).

A quotient can also, of course, be defined as a suitable 2-categorical limit.

Lemma

The quotient $q$ in any 2-congruence is eso.

Proof

If $m:A\to B$ is ff, then the square we must show to be a pullback is

$$\begin{array}{ccc}\mathrm{Act}(D,A)& \stackrel{}{\to }& \mathrm{Act}(D,B)\\ \downarrow & & \downarrow \\ K(D_0,A)& \underset{}{\to }& K(D_0,B)\end{array}$$\array{Act(D,A) & \overset{}{\to} & Act(D,B)\\ \downarrow && \downarrow\\ K(D_0,A)& \underset{}{\to} & K(D_0,B)}

But this just says that an action of $D$ on $A$ is the same as an action of $D$ on $B$ which happens to factor through $m$, and this follows directly from the assumption that $m$ is ff.

Definition

A 2-fork $D_1\rightrightarrows D_0\stackrel{f}{\to }X$ is called exact if $f$ is a quotient of $D$ and $D$ is a kernel of $f$.

This is the 2-categorical analogue of the notion of exact fork in a 1-category, and plays an analogous role in the definition of a regular 2-category and an exact 2-category.

Opposites

The opposite of a homwise-discrete category is again a homwise-discrete category. However, the opposite of a 2-congruence in $K$ is a 2-congruence in $K^{\mathrm{co}}$, since 2-cell duals interchange fibrations and opfibrations. Likewise, passage to opposites takes 2-forks in $K$ to 2-forks in $K^{\mathrm{co}}$, and preserves and reflects kernels, quotients, and exactness.

Regular 2-categories

Definition

A 2-category $K$ is called regular if

1. It is finitely complete,
2. esos are stable under pullback, and
3. Every 2-congruence which is a kernel can be completed to an exact 2-fork.

In particular, the last condition implies that every 2-congruence which is a kernel has a quotient.

Examples

• Cat is regular.

• A 1-category is regular as a 2-category iff it is regular as a 1-category, since the esos in a 1-category are precisely the strong epics.

• Every finitely complete (0,1)-category (that is, every meet-semilattice) is regular.

Factorizations

In StreetCBS the last condition is replaced by

• Every morphism $f$ factors as $f\cong me$ where $m$ is ff and $e$ is eso.

We now show that this follows from our definition. First we need:

Lemma

(Street’s Lemma) Let $K$ be a finitely complete 2-category where esos are stable under pullback, let $e:A\to B$ be eso, and let $n:B\to C$ be a map.

1. If the induced morphism $\ker (e)\to \ker (ne)$ is ff, then $n$ is faithful.
2. If $\ker (e)\to \ker (ne)$ is an equivalence, then $n$ is ff.

Proof

First note that $\ker (e)\to \ker (ne)$ being ff means that if $a_1,a_2:Y\rightrightarrows A$ and ${\delta }_1,{\delta }_2:e{a}_1\rightrightarrows e{a}_2$ are such that $n{\delta }_1=n{\delta }_2$, then ${\delta }_1={\delta }_2$. Likewise, $\ker (e)\to \ker (ne)$ being an equivalence means that given any $\alpha :ne{a}_1\to ne{a}_2$, there exists a unique $\delta :e{a}_1\to e{a}_2$ such that $n\delta =\alpha$.

We first show that $n$ is faithful under the first hypothesis. Suppose we have $b_1,b_2:X\rightrightarrows B$ and ${\beta }_1,{\beta }_2:b_1\to b_2$ with $n{\beta }_1=n{\beta }_2$. Take the pullback

$$\begin{array}{cccc}& Y& \stackrel{r}{\to }& X\\ (a_1,a_2)& \downarrow & & \downarrow & (b_1,b_2)\\ & A\times A& \stackrel{e\times e}{\to }& B\times B\end{array}$$\array{&Y & \overset{r}{\to} & X \\ (a_1,a_2) & \downarrow && \downarrow & (b_1,b_2)\\ & A\times A & \overset{e\times e}{\to} & B\times B}

Then we have two 2-cells

$${\beta }_{1}r,{\beta }_{2}r:b_{1}r\rightrightarrows b_{2}r$$\beta_1 r, \beta_2 r: b_1 r \;\rightrightarrows\; b_2 r

such that the composites

$$ne{a}_1\cong n{b}_{1}r\stackrel{n{\beta }_{1}r=n{\beta }_{2}r}{\to }n{b}_{2}r\cong ne{a}_2$$n e a_1 \cong n b_1 r \overset{n \beta_1 r = n \beta_2 r}{\to} n b_2 r \cong n e a_2

are equal. By the hypothesis, $n{\beta }_{1}r=n{\beta }_{2}r$ implies ${\beta }_{1}r={\beta }_{2}r$. But $r$ is eso, since it is a pullback of the eso $e\times e$, so this implies ${\beta }_1={\beta }_2$. Thus, $n$ is faithful.

Now suppose the (stronger) second hypothesis, and form the pair of pullbacks:

$$\begin{array}{ccccc}(ne/ne)& \stackrel{g}{\to }& n/n& \to & C^2\\ \downarrow & & \downarrow & & \downarrow \\ A\times A& \stackrel{e\times e}{\to }& B\times B& \stackrel{n\times n}{\to }& C\times C\end{array}$$\array{(n e / n e) & \overset{g}{\to} & n / n & \to & C^{\mathbf{2}}\\ \downarrow && \downarrow && \downarrow \\ A\times A & \overset{e\times e}{\to} & B\times B & \overset{n\times n}{\to} & C\times C}

Then $g$, being a pullback of $e\times e$, is eso. We also have a commutative square

$$\begin{array}{ccc}(e/e)& \to & (ne/ne)\\ \downarrow & & \downarrow g\\ B^2& \to & (n/n).\end{array}$$\array{(e/e) & \to & (n e / n e)\\ \downarrow && \downarrow g \\ B^{\mathbf{2}} & \to & (n/n).}

By assumption, $(e/e)\to (ne/ne)$ is an equivalence. Since we have shown that $n$ is faithful, the bottom map $B^2\to (n/n)$ is ff, so since the eso $g$ factors through it, it must be an equivalence as well. But this says precisely that $n$ is ff.

Theorem

A 2-category is regular if and only if

1. it has finite limits,
2. esos are stable under pullback,
3. every morphism $f$ factors as $f\cong me$ where $m$ is ff and $e$ is eso, and
4. every eso is the quotient of its kernel.

Proof

First suppose $K$ is regular; we must show the last two conditions. Let $f:A\to B$ be any morphism. By assumption, the kernel $\ker (f)$ can be completed to an exact 2-fork $\ker (f)\rightrightarrows A\stackrel{e}{\to }C$. Since $e$ is the quotient of the 2-congruence $\ker (f)$, it is eso, and since $f$ comes with an action by $\ker (f)$, we have an induced map $m:C\to B$ with $f\cong me$. But since the 2-fork is exact, we also have $\ker (f)\simeq \ker (e)$, so by Street’s Lemma, $m$ is ff.

Now suppose that in the previous paragraph $f$ were already eso. Then since it factors through the ff $m$, $m$ must be an equivalence; thus $f$ is equivalent to $e$ and hence is a quotient of its kernel.

Now suppose $K$ satisfies the conditions in the lemma. Let $f:A\to B$ be any morphism; we must show that $\ker (f)$ can be completed to an exact 2-fork. Factor $f=me$ where $m$ is ff and $e$ is eso. Since $m$ is ff, we have $\ker (f)\simeq \ker (e)$. But every eso is the quotient of its kernel, so the fork $\ker (f)\rightrightarrows A\stackrel{e}{\to }C$ is exact.

In StreetCBS it is claimed that the final condition in Theorem 5 follows from the other three, but there is a flaw in the proof.

Subobjects

In a regular 2-category $K$, we call a ff $m:A\to X$ with codomain $X$ a subobject of $X$. We write $\mathrm{Sub}(X)$ for the preorder of subobjects of $X$, as a full sub-2-category of the slice 2-category $K/X$. Since $K$ is finitely complete and pullbacks preserve ffs, we have pullback functors $f^{*}:\mathrm{Sub}(Y)\to \mathrm{Sub}(X)$ for any $f:X\to Y$.

If $g\cong me$ where $m$ is ff and $e$ is eso, we call $m$ the image of $g$. Taking images defines a left adjoint ${\exists }_f:\mathrm{Sub}(X)\to \mathrm{Sub}(Y)$ to $f^{*}$ in any regular 2-category, and the Beck-Chevalley condition is satisfied for any pullback square, because esos are stable under pullback.

Preservation

It is easy to check that if $K$ is regular, so are:

• its 2-cell dual $K^{\mathrm{co}}$ (by the remarks about opposite 2-congruences).
• the (2,1)-category $\mathrm{gpd}(K)$ of groupoidal objects in $K$.
• the (1,2)-category $\mathrm{pos}(K)$ of posetal objects in $K$.
• the 1-category $\mathrm{disc}(K)$ of discrete objects in $K$.
• and more generally the $n$-category ${\mathrm{trunc}}_n(K)$ of $n$-truncated objects in $K$.

The slice 2-category $K/X$ does not, in general, inherit regularity, but we have:

Theorem

If $K$ is regular, so are the fibrational slices $\mathrm{Opf}(X)$ and $\mathrm{Fib}(X)$.

Classification of congruences

In general, the idea is that an $n$-congruence in an $m$-category $K$, where $n\le m$, is an “internal $(n-1)$-category” in $K$. Of course, we only deal formally with the case $m\le 2$, although we allow $n$ and $m$ to be of the form $(r,s)$; see n-prefix.

Definition

Let $D$ be a 2-congruence in a 2-category $K$.

• $D$ is a (2,1)-congruence if it is an internal groupoid, i.e. there is a map $D_1\to D_1$ providing “inverses”.
• It is a (1,2)-congruence if $D_1\to D_0\times D_0$ is ff.
• It is a 1-congruence if it is both a (2,1)-congruence and a (1,2)-congruence.
• it is a (0,1)-congruence if $D_1\to D_0\times D_0$ is an equivalence.

Note that in a 1-category,

• a 2-congruence is just an internal category (a 1-category),
• a (2,1)-congruence is an internal groupoid (a (1,0)-category),
• a (1,2)-congruence is an internal poset (a (0,1)-category), and
• a 1-congruence is an internal equivalence relation (a 0-category).

Of course, a (0,1)-congruence in any 2-category is completely determined by any object $D_0$.

Theorem

Let $q:X\to Y$ be a morphism in $K$. If $Y$ is $n$-truncated for $n\ge -1$, then $\ker (q)$ is an $(n+1)$-congruence. This means that:

1. If $Y$ is groupoidal, then $\ker (q)$ is a (2,1)-congruence.
2. If $Y$ is posetal, then $\ker (q)$ is a (1,2)-congruence.
3. If $Y$ is discrete, then $\ker (q)$ is a 1-congruence.
4. If $Y$ is subterminal, then $\ker (q)$ is a (0,1)-congruence.

In all these cases the converse is true if $K$ is regular and $q$ is eso.

Proof

The forward directions are fairly obvious; it is the converses which take work. Suppose first that $\ker (q)$ is a (2,1)-congruence, and let $\alpha :f\to g:X\rightrightarrows Y$ be any 2-cell. Pulling back the eso $q$ along $f$ and $g$ gives $P_1\to T$ and $P_2\to T$; let $r:P\to T$ be the pullback $P_1{\times }_X{P}_2$. Since $K$ is regular, $r$ is eso. By definition of kernels, the 2-cell $\alpha r$ corresponds to a map $P\to (q/q)$. But $(q/q)\rightrightarrows C$ is a (2,1)-congruence, so composing this map with the “inverse” map $(q/q)\to (q/q)$ gives another map $P\to (q/q)$, and thereby another 2-cell $fr\to gr$ which is inverse to $\alpha r$. Finally, since $r$ is eso, precomposing with it reflects invertibility, so $\alpha$ must also be invertible. Thus $Y$ is groupoidal.

Now suppose that $\ker (q)$ is a (1,2)-congruence, and let $\alpha ,\beta :f\to g:T\to Y$ be two parallel 2-cells. With notation as in the previous paragraph, the 2-cells $\alpha r$ and $\beta r$ correspond to morphisms $P\rightrightarrows (q/q)$ which become isomorphic in $X$. But since $(q/q)\rightrightarrows X$ is a (1,2)-congruence, this implies that the two maps $P\rightrightarrows (q/q)$ are isomorphic, and hence $\alpha r=\beta r$. And since $r$ is eso, precomposing with it is faithful, so $\alpha =\beta$; thus $Y$ is posetal.

The discrete case follows by combining the posetal and groupoidal cases, so it remains to show that if $\ker (q)$ is a (0,1)-congruence then $Y$ is subterminal. We know it is discrete, so it suffices to show that given two $f,g:T\rightrightarrows Y$ we have a 2-cell $f\to g$. Continuing with the same notation, and letting $h,k:P\to X$ be the induced maps with $qh\cong fr$ and $qk\cong gr$, we have $(h,k):P\to X\times X=(q/q)$, and therefore the 2-cell defining the fork $(q/q)\rightrightarrows X\stackrel{q}{\to }Y$ gives us a 2-cell $qh\to qk$ and therefore $fr\to gr$. Now $r$ is the quotient of its kernel, so for this 2-cell to induce a 2-cell $f\to g$ it suffices for it to be an action 2-cell for the actions of $\ker (r)$ on $fr$ and $gr$; but this is automatic since we know $Y$ to be posetal. Thus we have a 2-cell $f\to g$ as desired, so $Y$ is subterminal.

Exact 2-categories

A regular 1-category is exact when every congruence has a kernel. The definition for 2-categories is analogous.

Definition

Let $-1<n\le 2$ be directed (see n-prefix). A 2-category is $n$-exact if it is regular and every n-congruence is a kernel.

Recall that a 1-category is regular as a 1-category iff it is regular as a homwise-discrete 2-category. However, a regular 1-category is exact as a 1-category precisely when it is 1-exact as a 2-category. Since general 2-congruences in a 1-category are internal categories, they will obviously not all be kernels. This is why we add a prefix to “exact:” the best notion for 2-categories, which we call “2-exact,” is not a conservative extension of the established meaning of “exact” for 1-categories.

Likewise, it is unreasonable to expect a (2,1)-category to be any more than (2,1)-exact, or a (1,2)-category to be any more than (1,2)-exact.

Examples

• Cat is 2-exact. Likewise, Gpd is (2,1)-exact, Pos is (1,2)-exact, and of course Set is 1-exact.

• Every regular (0,1)-category (that is, every meet-semilattice) is (0,1)-exact, and in fact even 2-exact, since there are no nontrivial congruences of any sort in a poset.

• If $K$ is 2-exact, then by the classification of congruences, $\mathrm{gpd}(K)$ is (2,1)-exact, $\mathrm{pos}(K)$ is (1,2)-exact, $\mathrm{disc}(K)$ is 1-exact, and $\mathrm{Sub}(1)$ is (0,1)-exact.

• If $K$ is $n$-exact, then so is $K^{\mathrm{co}}$, by the remarks about opposite 2-congruences. For 1-categories and (2,1)-categories, of course, this is contentless, but for 2-categories and (1,2)-categories it is contentful.

Coherent 2-categories

Definition

A 2-category is called coherent if

1. it has finite limits,
2. finite jointly-eso families are stable under pullback, and
3. every finitary 2-polycongruence which is a kernel can be completed to an exact 2-polyfork.

Here a family $\{f_i:A_i\to B\}$ is said to be jointly-eso if whenever $m:C\to B$ is ff and every $f_i$ factors through $m$ (up to isomorphism), then $m$ is an equivalence.

Likewise, we have infinitary coherent 2-categories in which “finite” in the second two conditions is replaced by “small.”

Examples

• $\mathrm{Cat}$ is coherent.

• A 1-category is coherent as a 2-category iff it is coherent as a 1-category.

• A (0,1)-category (= poset) is coherent iff it is a distributive lattice, and infinitary-coherent iff it is a frame.

Factorizations

The following are proven just like their unary analogues in a regular 2-category.

Lemma

(Street’s Lemma) In a finitely complete 2-category where finite jointly-eso families are stable under pullback, if $\{e_i:A_i\to B\}$ is finite and jointly-eso and $n:B\to C$ is such that the induced functor $\ker (e_i)\to \ker (n{e}_i)$ is an equivalence, then $n$ is ff.

Theorem

A 2-category is coherent if and only if

1. it has finite limits,
2. finite jointly-eso families are stable under pullback,
3. every finite family $\{f_i\}$ factors as $f_i=m{e}_i$ where $m$ is ff and $\{e_i\}$ is jointly-eso, and
4. every jointly-eso family is the quotient of its kernel.

Of course, there are infinitary versions. In particular, we conclude that in a coherent (resp. infinitary-coherent) 2-category, the posets $\mathrm{Sub}(X)$ have finite (resp. small) unions that are preserved by pullback.

Colimits

Lemma

A coherent 2-category has a strict initial object; that is an initial object $0$ such that any morphism $X\to 0$ is an equivalence.

Proof

The empty 2-congruence is the kernel of the empty family (over any object), so it must have a quotient $0$, which is clearly an initial object. The empty family over $0$ is jointly-eso, so for any $X\to 0$ the empty family over $X$ is also jointly-eso; but this clearly makes $X$ initial as well.

Two ffs $m:A\to X$ and $n:B\to X$ are said to be disjoint if the comma objects $(m/n)$ and $(n/m)$ are initial objects. If initial objects are strict, then this implies that the pullback $A{\times }_{X}B$ is also initial, but it is strictly stronger already in $\mathrm{Pos}$.

Lemma

In a coherent 2-category, if $A\to X$ and $B\to X$ are disjoint subobjects, then their union $A\cup B$ in $\mathrm{Sub}(X)$ is also their coproduct $A+B$.

Proof

If $A$ and $B$ are disjoint subobjects of $X$, then the kernel of $\{A\to X,B\to X\}$ is the disjoint union of $\ker (A)$ and $\ker (B)$. Therefore, a quotient of it (which is a union of $A$ and $B$ in $\mathrm{Sub}(X)$) will be a coproduct of $A$ and $B$.

A coproduct $A+B$ in a 2-category is disjoint if $A$ and $B$ are disjoint subobjects of $A+B$. We say a coherent 2-category is positive if any two objects have a disjoint coproduct. By Lemma 3, this is equivalent to saying that any two objects can be embedded as disjoint subobjects of some other object. Disjoint coproducts in a coherent 2-category are automatically stable under pullback, so a positive coherent 2-category is necessarily extensive. Conversely, we have:

Lemma

A regular and extensive 2-category is coherent (and positive).

In the presence of finite coproducts, a family $\{e_i:A_i\to B\}$ is jointly-eso iff ${\coprod }_i{A}_i\to B$ is eso; thus regularity and universal coproducts imply that finite jointly-eso families are stable under pullback. And assuming extensivity, any 2-polycongruence $\{C_{ij}\}\rightrightarrows \{C_i\}$ gives rise to an ordinary 2-congruence ${\coprod }_{ij}{C}_{ij}\rightrightarrows {\coprod }_i{C}_i$. Likewise, 2-polyforks $\{C_{ij}\}\rightrightarrows \{C_i\}\to X$ correspond to 2-forks ${\coprod }_{ij}{C}_{ij}\rightrightarrows {\coprod }_i{C}_i\to X$, and the property of being a kernel or a quotient is preserved; thus regularity implies coherency.

Preservation

If $K$ is coherent, then easily so are $K^{\mathrm{co}}$, $\mathrm{disc}(K)$, $\mathrm{gpd}(K)$, $\mathrm{pos}(K)$, and $\mathrm{Sub}(1)$. Moreover, we have:

Theorem

If $K$ is a coherent 2-category, so are the fibrational slices $\mathrm{Opf}(X)$ and $\mathrm{Fib}(X)$ for any $X\in K$.

Extensive 2-categories

A coproduct $A+B$ in a 2-category is said to be disjoint if we have comma squares

$$\begin{array}{ccccccccccccccc}{A}^2& \to & A& & B^2& \to & B& & 0& \to & A& & 0& \to & B\\ \downarrow & \Downarrow & \downarrow & & \downarrow & \Downarrow & \downarrow & & \downarrow & \Downarrow & \downarrow & & \downarrow & \Downarrow & \downarrow & \\ A& \to & A+B& & B& \to & A+B& & B& \to & A+B& & A& \to & A+B& \end{array}$$\array{ A^{\mathbf{2}} & \to & A & \quad & B^{\mathbf{2}} & \to & B & \quad & 0 & \to & A & \quad & 0 & \to & B \\ \downarrow & \Downarrow & \downarrow & \quad & \downarrow & \Downarrow & \downarrow & \quad & \downarrow & \Downarrow & \downarrow & \quad & \downarrow & \Downarrow & \downarrow & \quad\\ A & \to & A+B & \quad & B & \to & A+B & \quad & B & \to & A+B & \quad & A & \to & A+B & \quad}

The first two say that $A\to A+B$ and $B\to A+B$ are ff and the second two say that they are disjoint subobjects of $A+B$.

A coproduct $A+B$ is said to be universal if for any morphism $Z\to A+B$, the pullbacks

$$\begin{array}{ccccc}X& \to & Z& \leftarrow & Y\\ \downarrow & & \downarrow & & \downarrow \\ A& \to & A+B& \leftarrow & B\end{array}$$\array{X & \to & Z & \leftarrow & Y\\ \downarrow & & \downarrow & & \downarrow\\ A & \to & A+B & \leftarrow & B}

exist and exhibit $Z$ as a coproduct $X+Y$.

Finally, we say a 2-category is extensive if it has finite coproducts which are disjoint and universal. If it also has finite limits we say it is lextensive, and if it is also coherent we call it positive. (Note that disjoint coproducts in a coherent 2-category are always universal.)

An extensive 2-category does satisfy 2-categorical versions of the additional characterizations of an extensive 1-category, but unlike in the 1-categorical case, these alternate conditions do not seem to suffice to characterize extensivity. In particular, though, a 1-category is extensive as a 1-category iff it is so as a homwise-discrete 2-category.

Preservation

If $K$ is extensive, so is $K^{\mathrm{co}}$, obviously. Less obvious is:

Lemma

If $K$ is extensive, so are $\mathrm{gpd}(K)$, $\mathrm{pos}(K)$, and $\mathrm{disc}(K)$. In other words, if $K$ is extensive, so is its $(n+1)$-category ${\mathrm{trunc}}_n(K)$ of $n$-truncated objects for $0\le n$.

Proof

Since the three given categories are closed in $K$ under limits and strict initial objects, it suffices to show they are closed under coproducts. First suppose given two morphisms $f,g:Z\to A_1+A_2$. Then $f$ decomposes $Z=X_1+X_2$, and $g$ decomposes $Z=Y_1+Y_2$. Then the inclusions $X_i\to Z=Y_1+Y_2$ also decompose each $X_i=X_{i1}+X_{i2}$. Now if there exists a 2-cell $f\to g$, it induces a map from each $X_{ij}$ to the comma object of $A_1$ and $A_2$. Since coproducts are disjoint and initials are strict, this implies that $X_{12}=X_{21}=0$. Therefore, we have a decomposition $Z=X_{11}+X_{22}$ so that $f=f_1+f_2$ and $g=g_1+g_2$, where $f_i:X_{ii}\to A_i$ and $g_i:X_{ii}\to A_i$.

Now, by universality of the coproduct $X_{11}+X_{22}$, it follows that 2-cells $f\to g$ are determined uniquely by pairs of 2-cells $f_1\to g_1$ and $f_2\to g_2$. Therefore, if $A_1$ and $A_2$ are groupoidal, any 2-cells $f_1\to g_1$ and $f_2\to g_2$ are invertible, and thus so is any 2-cell $f\to g$; so $A_1+A_2$ is groupoidal. And if $A_1$ and $A_2$ are posetal, any parallel 2-cells $f_1\rightrightarrows g_1$ and $f_2\rightrightarrows g_2$ are equal, and thus so are any $f\rightrightarrows g$; so $A_1+A_2$ is posetal. And of course the discrete case follows by combining these.

However, the (0,1)-category (= poset) $\mathrm{Sub}(1)$ of (-1)-truncated objects (= subterminal objects) does not inherit extensivity, and in fact posets are almost never extensive: the only disjoint coproduct is $0+0$.

We also have:

Lemma

If $K$ is extensive, so are the fibrational slices $\mathrm{Opf}(X)$ and $\mathrm{Fib}(X)$ for any $X\in K$.

2-pretoposes

Definition

Let $n$ be 2, (2,1), (1,2), or 1. That is, $1\le n\le 2$ and $n$ is directed; see n-prefix.

Definition

An $n$-pretopos is an $n$-exact $n$-category which is also extensive. An infinitary $n$-pretopos is an $n$-pretopos which is infinitary-extensive.

As remarked here, regularity plus extensivity implies coherency. Thus an $n$-pretopos is, in particular, a coherent $n$-category. Conversely, we have:

Theorem

An $n$-category is an $n$-pretopos if and only if it is coherent and every (finitary) $n$-polycongruence is a kernel.

Examples

• $\mathrm{Cat}$ is a 2-pretopos. Likewise, $\mathrm{Gpd}$ is a (2,1)-pretopos and $\mathrm{Pos}$ is a (1,2)-pretopos.

• A 1-category is a 1-pretopos precisely when it is a pretopos in the usual sense. Note that, as remarked for exactness, a 1-category is unlikely to be an $n$-pretopos for any $n>1$.

• Since no nontrivial (0,1)-categories are extensive, the definition as phrased above is not reasonable for $n=(0,1)$. However, for some purposes (such as the n-Giraud theorem), it is convenient to define an (infinitary) (0,1)-pretopos to simply be an (infinitary) coherent (0,1)-category (exactness being automatic).

Colimits

An $n$-pretopos has coproducts and quotients of $n$-congruences, which are an important class of colimits. However, it can fail to admit all finite colimits, for essentially the same reason as when $n=1$: namely, some ostensibly “finite” colimits secretly involve infinitary processes. In a 1-category, this manifests in the construction of arbitrary coequalizers and pushouts, where we must first generate an equivalence relation by an infinitary process and then take its quotient.

For 2-categories it is even easier to find counterexamples: the 1-pretopos $\mathrm{FinSet}$ does in fact have all finite colimits, but the 2-pretopos $\mathrm{FinCat}$ of finite categories (that is, finitely many objects and finitely many morphisms) does not have coinserters, coinverters, or coequifiers. (The category $\mathrm{FPCat}$ of finitely presented categories does have finite colimits, but fails to have finite limits.)

However, I conjecture that just as in the case $n=1$, once an $n$-pretopos is also countably-coherent, it does become finitely cocomplete. See colimits in an n-pretopos.

Heyting 2-categories

Definition

Definition

A 2-category is Heyting if it is coherent and each pullback functor $f^{*}:\mathrm{Sub}(Y)\to \mathrm{Sub}(X)$ has a right adjoint ${\forall }_f$.

As in the 1-categorical case, this also ensures that each $\mathrm{Sub}(X)$ is a Heyting algebra and that each $f^{*}$ is a homomorphism of Heyting algebras. Moreover, the right adjoints ${\forall }_f$ satisfy the Beck-Chevalley condition for pullback squares, because the left adjoints ${\exists }_f$ do. This is just what is necessary for the internal interpretation of (finitary) first-order logic.

Examples

• $\mathrm{Cat}$ is Heyting.

• A 1-category is Heyting as a 2-category iff it is Heyting as a 1-category.

• A (0,1)-category is Heyting iff it is a Heyting algebra.

• Any well-powered infinitary-coherent 2-category is Heyting, by the adjoint functor theorem for posets. In particular, any Grothendieck 2-topos is Heyting.

• Unlike in the 1-categorical case, there seems no reason why a coherent 2-category with exponentials must be Heyting. It does, however have adjoints to pullback along fibrations and opfibrations, and in particular along product projections, which is enough for some uses of universal quantification in the internal logic.

Preservation

Clearly if $K$ is Heyting, so are $K^{\mathrm{co}}$, $\mathrm{gpd}(K)$, $\mathrm{pos}(K)$, $\mathrm{disc}(K)$, and $\mathrm{Sub}(1)$ (the Heyting algebra of subterminals).

Moreover, Heytingness is also preserved by fibrational slicing. First we show:

Theorem

If $K$ is Heyting, then for any $X$ and any $A\in \mathrm{Opf}(X)$, ${\mathrm{Sub}}_{\mathrm{Opf}(X)}(A)$ is a coreflective sub-poset of ${\mathrm{Sub}}_K(A)$.

Proof

As proven here, ${\mathrm{Sub}}_{\mathrm{Opf}(X)}(A)$ is a full sub-poset of ${\mathrm{Sub}}_K(A)$. Moreover, it is easy to see that a ff $B\to A$ is in ${\mathrm{Sub}}_{\mathrm{Opf}(X)}(A)$ precisely when

1. $B\to X$ is an opfibration and
2. $B\to A$ is a morphism of opfibrations.

In general, the first condition does not imply the second. It is also easy to check that these two conditions together are equivalent to saying that the composite

$$B{\times }_X{X}^2\to A{\times }_X{X}^2\stackrel{a}{\to }A$$B\times_X X ^{\mathbf{2}} \to A\times_X X ^{\mathbf{2}} \overset{a}{\to} A

factors through $B\to A$, where $a$ is the action making $A$ into a fibration. Note that $B{\times }_X{X}^2$ is alternately written as $p^{*}B$, where $p:A{\times }_X{X}^2\to A$ is the projection onto the first factor. Therefore, $B$ is in ${\mathrm{Sub}}_{\mathrm{Opf}(X)}(A)$ just when ${\exists }_p{a}^{*}B\le B$, or equivalently when $B\le {\forall }_a{p}^{*}B$.

We claim that $B\mapsto {\forall }_a{p}^{*}B$ coreflects $\mathrm{Sub}(A)$ into ${\mathrm{Sub}}_{\mathrm{Opf}(X)}(A)$, and given the above, it suffices to verify that it is a comonad. First, let $i:A\to A{\times }_X{X}^2$ be the inclusion of identities; then $ai\cong 1$ and $pi\cong 1$, so we have

$$\begin{array}{rl}{i}^{*}{a}^{*}B=& B\\ a^{*}B\le & {\forall }_{i}B\\ {\forall }_p{a}^{*}B\le & {\forall }_p{\forall }_{i}B=B.\end{array}$$\begin{aligned} i^*a^*B =& B\\ a^*B \le& \forall_i B\\ \forall_p a^* B \le& \forall_p \forall_i B = B. \end{aligned}

This gives the counit of the comonad. The comultiplication is a little more involved. First note that we have a pullback square

$$\begin{array}{ccc}A{\times }_X{X}^2{\times }_X{X}^2& \stackrel{q}{\to }& A{\times }_X{X}^2\\ {}^{a\times 1}\downarrow & & {\downarrow }^a\\ A{\times }_X{X}^2& \underset{p}{\to }& A\end{array}$$\array{ A\times_X X ^{\mathbf{2}} \times_X X ^{\mathbf{2}} & \overset{q}{\to} & A\times_X X ^{\mathbf{2}} \\ ^{a\times 1}\downarrow && \downarrow^a\\ A\times_X X ^{\mathbf{2}} & \underset{p}{\to} & A}

where $q$ denotes projection onto the first two factors. Thus, by the Beck-Chevalley condition, $a^{*}{\forall }_p={\forall }_q(a\times 1{)}^{*}$ and therefore

$${\forall }_p{a}^{*}{\forall }_p{a}^{*}B={\forall }_p{\forall }_q(a\times 1{)}^{*}{a}^{*}B={\forall }_p{\forall }_q(1\times m{)}^{*}{a}^{*}B$$\forall_p a^*\forall_p a^* B = \forall_p \forall_q (a\times 1)^* a^* B = \forall_p \forall_q (1\times m)^* a^* B

where $m:X^2{\times }_X{X}^2\to X^2$ is the “composition” morphism.

Let us write $X^{\to \to }$ for $X^2{\times }_X{X}^2$, the object of composable arrows in $X$, and write $X^{\stackrel{\nearrow }{\to }\to }$ for the power of $X$ with the category

$$\begin{array}{ccc}& & •\\ & \nearrow \\ •& \to & •& \to & •\end{array}$$\array{&& \bullet\\ & \nearrow\\ \bullet &\to & \bullet & \to &\bullet}

Let $r:X^{\stackrel{\nearrow }{\to }\to }\to X^{\to \to }$ forget the “lonely” arrow, and let $c:X^{\to \to }\to X^{\stackrel{\nearrow }{\to }\to }$ make the lonely arrow into the composite of the other two. Then $rc\cong 1$, and moreover $p\prime q\prime c\cong 1\times m$, where $p\prime$ and $q\prime$ are $p$ and $q$ applied to the non-lonely arrows. Thus, we have

$$\begin{array}{rl}{c}^{*}(q\prime {)}^{*}(p\prime {)}^{*}{a}^{*}B=& (1\times m{)}^{*}{a}^{*}B\\ (q\prime {)}^{*}(p\prime {)}^{*}{a}^{*}B\le & {\forall }_c(1\times m{)}^{*}{a}^{*}B\\ {\forall }_r(q\prime {)}^{*}(p\prime {)}^{*}{a}^{*}B\le & {\forall }_r{\forall }_c(1\times m{)}^{*}{a}^{*}B\\ {\forall }_r(q\prime {)}^{*}(p\prime {)}^{*}{a}^{*}B\le & (1\times m{)}^{*}{a}^{*}B\\ q^{*}{p}^{*}{\forall }_p{a}^{*}B\le & (1\times m{)}^{*}{a}^{*}B\\ {\forall }_p{a}^{*}B\le & {\forall }_p{\forall }_q(1\times m{)}^{*}{a}^{*}B\\ {\forall }_p{a}^{*}B\le & {\forall }_p{a}^{*}{\forall }_p{a}^{*}B.\end{array}$$\begin{aligned} c^* (q')^* (p')^* a^* B =& (1\times m)^* a^* B\\ (q')^* (p')^* a^* B \le& \forall_c (1\times m)^* a^* B\\ \forall_r (q')^* (p')^* a^* B \le& \forall_r \forall_c (1\times m)^* a^* B\\ \forall_r (q')^* (p')^* a^* B \le& (1\times m)^* a^* B\\ q^* p^* \forall_p a^* B \le& (1\times m)^* a^* B\\ \forall_p a^* B \le& \forall_p \forall_q (1\times m)^* a^* B\\ \forall_p a^* B \le& \forall_p a^*\forall_p a^* B. \end{aligned}

as desired. (Here we have used another Beck-Chevalley condition to move $r$ past $q\prime$ and $p\prime$, turning them into $p$ and $q$ and it into $p$.)

Corollary

If $K$ is Heyting, so is each fibrational slice $\mathrm{Opf}(X)$ and $\mathrm{Fib}(X)$.

Proof

This follows from the adjoint lifting theorem for posets: for any $f:A\to B$ in $\mathrm{Opf}(X)$ we have a commutative square

$$\begin{array}{ccc}{\mathrm{Sub}}_{\mathrm{Opf}(X)}(B)& \stackrel{f^{*}}{\to }& {\mathrm{Sub}}_{\mathrm{Opf}(X)}(A)\\ \downarrow & & \downarrow \\ {\mathrm{Sub}}_K(B)& \underset{f^{*}}{\to }& {\mathrm{Sub}}_K(A)\end{array}$$\array{Sub_{Opf(X)}(B) & \overset{f^*}{\to} & Sub_{Opf(X)}(A)\\ \downarrow && \downarrow\\ Sub_K(B)& \underset{f^*}{\to} & Sub_K(A)}

where the vertical arrows are comonadic (inclusions of coreflective sub-posets) and the bottom horizontal arrow has a right adjoint; hence so does the top horizontal arrow.

Booleanness

We may naturally say that a coherent 2-category $K$ is Boolean if each $\mathrm{Sub}(X)$ is a Boolean algebra. As usual, this implies that $K$ is Heyting; we have ${\forall }_f=\neg {\exists }_f\neg$.

Note that a subobject and its complement in $\mathrm{Sub}(X)$ need not be “disjoint” in the sense introduced here; only their pullback, not their comma object, need be initial. Note also that unlike in the 1-categorical case, Booleanness is not stable under slicing; this fails already in the (1,2)-category $\mathrm{Pos}$ (though it holds in any (2,1)-category).

Cores

Cores

The core of a category $A$ is the maximal subcategory of $A$ that is a groupoid, consisting of all its objects and all isomorphisms between them. The core is not a functor on the 2-category $\mathrm{Cat}$, but it is a functor on the (2,1)-category ${\mathrm{Cat}}_g$ of categories, functors, and natural isomorphisms. In fact, it is a coreflection of ${\mathrm{Cat}}_g$ into $\mathrm{Gpd}$.

In general, for any 2-category $K$ we write $K_g$ for its “homwise core:” the sub-2-category determined by all the objects and morphisms but only the iso 2-cells. Of course, $K_g$ is a (2,1)-category. Then $\mathrm{gpd}(K)$ is a full sub-2-category of $K_g$, and we can ask whether it is coreflective. In a regular 2-category, however, it turns out that there is a stronger and more useful notion which implies this coreflectivity.

Definition

A core of an object $A$ in a regular 2-category is a morphism $J\to A$ which is eso, pseudomonic, and where $J$ is groupoidal.

Lemma

In a regular 2-category $K$, any core $J\to A$ is a coreflection of $A$ from $K_g$ into $\mathrm{gpd}(K)$.

Proof

We must show that for any groupoidal $G$, the functor

$$\mathrm{gpd}(K)(G,J)=K_g(G,J)\to K_g(G,A)$$gpd(K)(G,J)=K_g(G,J)\to K_g(G,A)

is an equivalence. Since $J\to A$ is pseudomonic in $K$, it is ff in $K_g$, so this functor is full and faithful; thus it remains to show it is eso. Given any map $G\to A$, take the pullback

$$\begin{array}{ccc}P& \to & J\\ \downarrow & & \downarrow \\ G& \to & A\end{array}$$\array{P & \to & J\\ \downarrow && \downarrow \\ G & \to & A}

and let $P_1\rightrightarrows P$ be the kernel of $P\to G$. Since the composite $P\to A$ descends to $G$, it comes equipped with an action by this kernel. However, since $G$ is groupoidal, $P_1\rightrightarrows P$ is a (2,1)-congruence, so the 2-cell defining the action must be an isomorphism. Therefore, it must factor uniquely through the pseudomonic $J\to A$, so $P\to J$ has an action as well; thus it descends to a map $G\to J$, as desired.

In particular, cores in a regular 2-category are unique up to unique equivalence. We write $J(A)$ for the core of $A$, when it exists.

Lemma

An object $A$ of a (2,1)-exact 2-category has a core if and only if there is an eso $C\to A$ where $C$ is groupoidal.

Proof

“Only if” is clear, so suppose that $p:C\to A$ is eso and $C$ is groupoidal. Let $C_1=C{\times }_{A}C$ be the pullback. Then $C_1$ is also groupoidal and is a (2,1)-congruence on $C$, so by exactness it is the kernel of some eso $q:C\to J$. There is an evident induced map $m:J\to A$; we claim that this is a core of $A$.

Evidently $m:J\to A$ is eso, since the eso $C\to A$ factors through it. And since $C_1$ is a (2,1)-congruence, the classification of congruences implies that $J$ is groupoidal; thus it remains to show that $m$ is pseudomonic.

First suppose given $f,g:X\rightrightarrows J$. Pulling back $q$ along $f$ and $g$ gives esos $P_1\to X$ and $P_2\to X$, whose pullback $P=P_1{\times }_X{P}_2$ comes with an eso $r:P\to T$ and two morphisms $h,k:P\to C$ with $qh\cong fr$ and $qk\cong gr$. Then any pair of 2-cells $\alpha ,\beta :f\to g$ induce maps $P\rightrightarrows C_1$, since $C_1$ is the kernel $(q/q)$. But if $m\alpha =m\beta$, then these two maps must be equal, since $C_1$ is also the kernel $(p/p)$. Therefore, $\alpha r=\beta r$, and since $r$ is eso, $\alpha =\beta$; thus $m$ is faithful.

On the other hand, again given $f,g:X\rightrightarrows J$, any isomorphism $\alpha :mf\cong mg$ induces a map $P\to C_1$ and therefore a 2-cell $\beta :fr\to gr$ with $m\beta =\alpha r$. To show that $\beta$ descends to a 2-cell $f\to g$, we must verify that it is an action 2-cell for the actions of $P\rightrightarrows J$ on $fr$ and $gr$. But $m\beta$ is an action 2-cell, since $m\beta =\alpha r$, and we now know that $m$ is faithful, so it reflects the axiom for an action 2-cell. Therefore, $m$ is full-on-isomorphisms, and hence pseudomonic.

Enough groupoids

We say that a regular 2-category has enough groupoids if every object admits an eso from a groupoidal one. Thus, a (2,1)-exact 2-category has cores if and only if it has enough groupoids.

Likewise, we say that a regular 2-category has enough discretes if every object admits an eso from a discrete one. Clearly this is a stronger condition. Note, though, that if $K$ has enough groupoids, then $\mathrm{pos}(K)$ has enough discretes, since the core of any posetal object is discrete.

Having enough discretes, or at least enough groupoids, is a very familiar aspect of 2-categories such as $\mathrm{Cat}$. It also turns out to make the internal logic noticeably easier to work with. However, in a sense none of the really “new” 2-categories have enough groupoids or discretes.

• The 2-exact 2-categories having enough discretes are precisely the categories of internal categories and anafunctors in 1-exact 1-categories; see exact completion of a 2-category. Likewise, any 2-exact 2-categories having enough groupoids consists of certain internal categories in a (2,1)-category.

• Basically the only Grothendieck 2-toposes having enough discretes are the 2-categories of stacks on 1-sites, and the only ones having enough groupoids are the 2-categories of stacks on (2,1)-sites. The “honestly 2-dimensional” case of stacks on 2-sites (almost?) never have enough of either.

Subobjects

We also remark that cores, when they exist, “capture all the information about subobjects.”

Proposition

If $K$ is a regular 2-category and $A$ is an object having a core $j:J\to A$, then $j^{*}:\mathrm{Sub}(A)\to \mathrm{Sub}(J)$ is an equivalence.

Proof

It is a general fact in a regular 2-category that for any eso $f:X\to Y$, $f^{*}:\mathrm{Sub}(Y)\to \mathrm{Sub}(X)$ is full (and faithful, which of course is automatic for a functor between posets). For if $f^{*}U\le f^{*}V$, then we have a square

$$\begin{array}{ccccc}{f}^{*}U& \to & f^{*}V& \to & V\\ \downarrow & & & & \downarrow \\ U& & \to & & Y\end{array}$$\array{f^*U & \to & f^*V & \to & V\\ \downarrow &&&& \downarrow\\ U & & \to & & Y}

in which $f^{*}U\to U$ is eso and $V\to Y$ is ff, hence we have $U\to V$ over $Y$.

Thus, in our case, $j^{*}$ is full and faithful since $j$ is eso, so it suffices to show that for any ff $U\to J$ we have $j^{*}{\exists }_{j}U\le U$ in $\mathrm{Sub}(J)$. But we have a commutative square

$$\begin{array}{ccc}U& \to & {\exists }_{j}U\\ \downarrow & & \downarrow \\ J& \to & X\end{array}$$\array{U & \to & \exists_j U\\ \downarrow && \downarrow\\ J & \to & X}

where the vertical arrows are ff and the bottom arrow $J\to X$ is faithful and pseudomonic, from which it follows that $U\to {\exists }_{j}U$ is also faithful and pseudomonic. Since $U\to {\exists }_{j}U$ is eso by definition, $U$ is a core of ${\exists }_{j}U$, and since $j^{*}{\exists }_{j}U$ is a groupoid mapping to ${\exists }_{j}U$, it factors through $U$, as desired.

NNOs in a 2-category

If $K$ is a 2-category with finite limits, a successor algebra in $K$ is an object $X$ equipped with morphisms $o:1\to X$ and $s:X\to X$. A morphism of successor algebras is a morphism $f:X\to Y$ with isomorphisms $f{o}_X\cong o_Y$ and $f{s}_X\cong s_{Y}f$. Likewise a 2-cell of successor algebras is a 2-cell $\alpha :f\to g$ commuting with the above isomorphisms in an obvious way.

Finally, a natural numbers object in $K$ is an initial object $N$ in the 2-category $\mathrm{SuccAlg}(K)$ of successor algebras. This means that for any successor algebra $X$ there is a morphism $N\to X$ of successor algebras, unique up to unique isomorphism. Clearly any NNO in $K$ is also an NNO, in the usual sense, in $\mathrm{disc}(K)$.

If $K$ doesn’t have enough exponentials, then perhaps this definition should be augmented with some parametricity, as in the 1-categorical case.

As in a 1-category, we can prove that:

• If $K$ has coproducts, then $[o,s]:1+N\to N$ is an equivalence, since $N$ is an initial algebra for the endofunctor $1+(-)$.
• Therefore, if $K$ is extensive, then $o:1\to N$ and $s:N\to N$ are disjoint subobjects of $N$.
• $N$ satisfies the fifth Peano axiom: if $N\prime$ is a subobject of $N$ containing $o$ and closed under $s$, then $N\prime =N$.

This enables us to show the following, using the internal logic.

Theorem

If $K$ is a positive Heyting coherent 2-category with an NNO $N$, then $N$ is discrete.

Proof

First note that since $N\simeq 1+N$ and coproducts are disjoint, we have

$$\begin{array}{rl}x:N,f:{\mathrm{hom}}_N(o,x),g:{\mathrm{hom}}_N(x,o)& ⊢f=g\text{and is an isomorphism}\\ x:N,f:{\mathrm{hom}}_N(x,o),g:{\mathrm{hom}}_N(o,x)& ⊢f=g\text{and is an isomorphism}\end{array}$$\begin{aligned} x:N, f:hom_N(o,x), g:hom_N(x,o) &\vdash f=g\;\text{and is an isomorphism}\\ x:N, f:hom_N(x,o), g:hom_N(o,x) &\vdash f=g\;\text{and is an isomorphism} \end{aligned}

Now consider the subobject $S\hookrightarrow N$ described in the internal logic as determined by those $y:N$ for which the above sequents remain true when $o$ is replaced by $y$. (This requires universal quantification over $x,f,g$.) The above observation shows that $o\in S$. Suppose that $y\in S$, $x:N$, and $f:{\mathrm{hom}}_N(sy,x)$, $g:{\mathrm{hom}}_N(sy,x)$. If $x=o$ then $f=g$ and is an isomorphism; otherwise $x=sz$; but $s$ is ff, so we have $f\prime :{\mathrm{hom}}_N(y,z)$ and $g\prime :{\mathrm{hom}}_N(y,z)$ which are equal and isomorphisms; hence so are $f=s(f\prime )$ and $g=s(g\prime )$. Thus, $S$ is closed under $s$, so it is all of $N$. Therefore, $N$ is discrete.

Exponentials in a 2-category

Cat is not locally cartesian closed

The 2-category $\mathrm{Cat}$ is cartesian closed, in an appropriate 2-categorical sense; see also the discussion here. However, it is not locally cartesian closed. This failure is fundamental and has nothing to do with strictness or size issues; pullbacks just don’t preserve colimits. For example, let $X=(0\to 1\to 2)$ be the ordinal $3$; then there is a pushout

$$\begin{array}{ccc}(1)& \to & (1\to 2)\\ \downarrow & & \downarrow \\ (0\to 1)& \to & (0\to 1\to 2)\end{array}$$\array{(1) & \to & (1\to 2)\\ \downarrow && \downarrow\\ (0\to 1) & \to & (0\to 1\to 2)}

in $\mathrm{Cat}/X$ which pulls back along the inclusion $(0\to 2)\to X$ to

$$\begin{array}{ccc}\varnothing & \to & (2)\\ \downarrow & & \downarrow \\ (0)& \to & (0\to 2)\end{array}$$\array{\emptyset & \to & (2)\\ \downarrow && \downarrow\\ (0) & \to & (0\to 2)}

which is certainly not a pushout. Note that the same counterexample applies in $\mathrm{Pos}$.

It is similarly easy to write down examples of coinserters, coinverters, and coequifiers that are not preserved by pullbacks. Coproducts are preserved by pullback (in fact, $\mathrm{Cat}$ is extensive), as are quotients of 2-congruences (since $\mathrm{Cat}$ is regular), but these seem to be about it for pullback-stable colimits in $\mathrm{Cat}$.

2-categories with exponentials

However, there are a number of other useful exponentiability properties that do hold when $K=\mathrm{Cat}$.

1. Fibrations and opfibrations are exponentiable. That is, if $f:A\to X$ is an (op)fibration, then exponentials $(B\to X{)}^{(A\to X)}$ exist in the slice 2-category $K/X$. Equivalently, $f^{*}:K/X\to K/A$ has a right adjoint ${\Pi }_f$. (Fibrations and opfibrations are not the only exponentiable morphisms in $\mathrm{Cat}$, but they are certainly the most important and most commonly encountered ones.)

2. If $A\to X$ is an opfibration and $B\to X$ is a fibration, then the exponential $(B\to X{)}^{(A\to X)}$ in $K/X$ is a fibration, and dually.

3. For any $f:Y\to X$, the functor $f^{*}:\mathrm{Fib}(X)\to \mathrm{Fib}(Y)$ has a right adjoint ${\mathrm{Ran}}_f$, and likewise for $f^{*}:\mathrm{Opf}(X)\to \mathrm{Opf}(Y)$.

4. For any $f:Y\to X$, the functors $f^{*}:\mathrm{DFib}(X)\to \mathrm{DFib}(Y)$ and $f^{*}:\mathrm{DOpf}(X)\to \mathrm{DOpf}(Y)$ have right adjoints ${\mathrm{Ran}}_f$.

5. The 2-categories $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$ are all cartesian closed.

6. $K$ itself is cartesian closed.

7. The 2-categories $\mathrm{DFib}(X)$ and $\mathrm{DOpf}(X)$ are all locally cartesian closed.

Note that ${\mathrm{Ran}}_f$ and ${\Pi }_f$ are not the same even when both exist, and likewise the exponentials in $\mathrm{Fib}(X)$ are not the same as the exponentials in $K/X$ even when both exist. The latter are better-behaved in some ways, for instance they are stable under pullback (because they are “fiberwise”).

Perhaps surprisingly, it turns out that the first of these properties is sufficient to imply all the others. The goal of the rest of this page is to prove this claim. Therefore, we define:

Definition

A 2-category $K$ with finite limits is said to have exponentials if all fibrations and opfibrations in $K$ are exponentiable.

Note that a 1-category, and in fact any (2,1)-category, has exponentials if and only if it is locally cartesian closed, since every morphism is a fibration and opfibration.

Basic observations

We begin with a couple of easy observations.

Proposition

If either fibrations or opfibrations are exponentiable in $K$, then $K$ is cartesian closed.

Proof

Of course, $K$ is cartesian closed just when every morphism $A\to 1$ is exponentiable; but every such morphism is both a fibration and an opfibration.

Proposition

If $A\to X$ is an opfibration and $B\to X$ is a fibration, then the exponential $(B\to X{)}^{(A\to X)}$ in $K/X$ (if it exists) is a fibration, and dually.

Proof

We say briefly how to construct an action morphism

$$X^2{\times }_X(B\to X{)}^{(A\to X)}\to (B\to X{)}^{(A\to X)}.$$X ^{\mathbf{2}} \times_X(B\to X)^{(A\to X)} \to (B\to X)^{(A\to X)}.

Of course, by adjointness it suffices to construct a morphism

$$A{\times }_X{X}^2{\times }_X(B\to X{)}^{(A\to X)}\to B$$A\times_X X ^{\mathbf{2}} \times_X (B\to X)^{(A\to X)} \to B

over $X$. Now the left-hand side is a limit of the diagram

$$\begin{array}{ccccc}& & & & (B\to X{)}^{(A\to X)}\\ & & & & \downarrow \\ & & X^2& \to & X\\ & & \downarrow \\ A& \to & X.\end{array}$$\array{ &&&& (B\to X)^{(A\to X)}\\ &&&& \downarrow\\ && X ^{\mathbf{2}} &\to & X\\ && \downarrow\\ A & \to & X.}

We first map it via a diagonal to the limit of

$$\begin{array}{ccccc}& & & & (B\to X{)}^{(A\to X)}\\ & & & & \downarrow \\ & & X^2& \to & X\\ & & \downarrow & & \uparrow \\ A& \to & X& \leftarrow & X^2\end{array}$$\array{ &&&& (B\to X)^{(A\to X)}\\ &&&& \downarrow\\ && X ^{\mathbf{2}} &\to & X\\ && \downarrow && \uparrow\\ A & \to & X & \leftarrow & X ^{\mathbf{2}}}

then use the covariant action of $X$ on $A$ to map to the limit of

$$\begin{array}{ccc}& & (B\to X{)}^{(A\to X)}\\ & & \downarrow \\ A& \to & X\\ & & \uparrow \\ X& \leftarrow & X^2\end{array}$$\array{ && (B\to X)^{(A\to X)}\\ && \downarrow\\ A &\to & X\\ && \uparrow\\ X & \leftarrow & X ^{\mathbf{2}}}

then the evaluation $A{\times }_X(B\to X{)}^{(A\to X)}\to B$ to get to the limit of

$$\begin{array}{ccc}& & B\\ & & \downarrow \\ & & X\\ & & \uparrow \\ X& \leftarrow & X^2\end{array}$$\array{ && B\\ && \downarrow\\ && X\\ && \uparrow\\ X & \leftarrow & X ^{\mathbf{2}}}

and finally the contravariant action of $X$ on $B$ to get to

$$\begin{array}{c}B\\ \downarrow \\ X.\end{array}$$\array{ B\\ \downarrow \\ X.}

It is then straightforward to check that this action makes $(B\to X{)}^{(A\to X)}$ into a fibration.

Comonadicity

The key observation for many of the proofs below is the following.

Lemma

If $K$ has exponentials, then for any $X$, $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$ are comonadic, as well as monadic, over $K/X$.

Proof

The monad on $K/X$ whose category of algebras is $\mathrm{Fib}(X)$ takes $A\to X$ to $X^2{\times }_{X}A$, or equivalently ${\Sigma }_s{t}^{*}A$ where $(s,t):X^2\rightrightarrows X$ are the two projections. But $t$ is an opfibration, so ${\Sigma }_s{t}^{*}$ has a right adjoint ${\Pi }_t{s}^{*}$. And it is a standard result, valid for 2-categories as for 1-categories, that when the underlying functor of a monad has a right adjoint, its right adjoint becomes a comonad whose category of coalgebras is equivalent to the category of algebras for the original monad.

Corollary

If $K$ has exponentials, then $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$ inherit any colimits possessed by $K$.

Proof

The category of coalgebras for any comonad inherits colimits from the base category, and slice (2-)categories always inherit colimits.

For our main applications of comonadicity, we require the following observation.

Proposition

Given a commutative square

$$\begin{array}{ccc}{D}_1& \stackrel{\overline{G}}{\to }& D_2\\ {}^{U_1}\downarrow & & {\downarrow }^{U_2}\\ C_1& \underset{G}{\to }& C_2\end{array}$$\array{D_1 & \overset{\overline{G}}{\to} & D_2\\ ^{U_1}\downarrow && \downarrow ^{U_2}\\ C_1 & \underset{G}{\to} & C_2}

of functors between 2-categories, if $U_1$ and $U_2$ are monadic, $D_1$ has reflexive codescent objects, and $G$ has a left adjoint, then $\overline{G}$ also has a left adjoint. Dually, if $U_1$ and $U_2$ are comonadic, $D_1$ has reflexive descent objects, and $G$ has a right adjoint, then $\overline{G}$ also has a right adjoint.

Proof

The 1-categorical version of this, referring to reflexive (co)equalizers, is well-known; see for instance

• P. T. Johnstone, Adjoint lifting theorems for categories of algebras.

The idea is the same as that in Beck’s (co)monadicity theorem: we express any object of $D_2$ as a reflexive coequalizer of free algebras, then apply the left adjoint of $G$ to obtain a reflexive pair of free algebras in $D_1$ and take its coequalizer. The 2-categorical version is analogous, using the ideas of a 2-categorical monadicity theorem as found, for example, in

• Claudio Hermida, Descent on 2-fibrations and strongly 2-regular 2-categories.

The dual is, of course, obvious.

Slicing and cartesian closure

Using comonadicity, we can show that certain exponentials are stable under slicing. First we observe:

Lemma

If $Y\to X$ is a fibration, then $\mathrm{Fib}(X)/Y$ is monadic over $K/Y$. If additionally $K$ has exponentials, then $\mathrm{Fib}(X)/Y$ is also comonadic over $K/Y$.

Proof

The first statement is an instance of a general fact: if $T$ is a monad on a (2-)category $C$ and $Y$ is a $T$-algebra, then there is an induced monad $T_Y$ on $C/Y$ whose (2-)category of algebras is $T\mathrm{Alg}/Y$, defined by taking $A\to Y$ to the composite $TA\to TY\to Y$.

The second statement is also an instance of a general fact: if such a $T$ has a right adjoint $G$, then $T_Y$ also has a right adjoint $G_Y$ defined to take $A\to Y$ to the pullback

$$\begin{array}{ccc}{G}_{Y}A& \to & GA\\ \downarrow & & \downarrow \\ Y& \to & GY.\end{array}$$\array{G_Y A & \to & G A\\ \downarrow && \downarrow\\ Y & \to & G Y.}

Here the lower map $Y\to GY$ is the adjunct of the algebra structure map $TY\to Y$.

Proposition

If $K$ has exponentials, then a morphism in $\mathrm{Fib}(X)$ or $\mathrm{Opf}(X)$ is exponentiable if its underlying morphism in $K$ is so. In particular, if $K$ has exponentials, then for any $X$, fibrations are exponentiable in $\mathrm{Fib}(X)$ and opfibrations are exponentiable in $\mathrm{Opf}(X)$.

Proof

Suppose that $f:Z\to Y$ is a morphism in $\mathrm{Fib}(X)$ and that $f$ is exponentiable in $K$. Then we have a commutative square

$$\begin{array}{ccc}\mathrm{Fib}(X)/Y& \stackrel{f^{*}}{\to }& \mathrm{Fib}(X)/Z\\ \downarrow & & \downarrow \\ K/Y& \underset{f^{*}}{\to }& K/Z\end{array}$$\array{Fib(X)/Y & \overset{f^*}{\to} & Fib(X)/Z\\ \downarrow && \downarrow\\ K/Y& \underset{f^*}{\to} & K/Z}

in which the vertical functors are comonadic by Lemma 10, and the bottom functor $f^{*}$ has a right adjoint since $f$ is exponentiable in $K$. Therefore, by Proposition 4, the top functor $f^{*}$ has a right adjoint as well. The second statement follows because the underlying morphism in $K$ of any fibration in $\mathrm{Fib}(X)$ is a fibration in $K$, and dually (see the theorems on iterated fibrations).

Corollary

If $K$ has exponentials and a duality involution, then $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$ also have exponentials for any $X$.

Proof

After Proposition 5, it remains to show that opfibrations are exponentiable in $\mathrm{Fib}(X)$ (and dually, fibrations are exponentiable in $\mathrm{Opf}(X)$). Note that an opfibration in $\mathrm{Fib}(X)$ will not, in general, be an opfibration in $K$. But with a duality involution we have $\mathrm{Fib}(X)\simeq \mathrm{Opf}(X^o)$, and opfibrations are exponentiable in $\mathrm{Opf}(X^o)$, hence also in $\mathrm{Fib}(X)$.

We say that a 2-category $K$ has local exponentials if $K$ has exponentials and each 2-category $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$ also has local exponentials. Of course, the recursion in this definition is not well-founded, but we can reformulate it in explicit terms to say that

1. $K$ has exponentials,
2. Each $\mathrm{Opf}(X)$ and $\mathrm{Fib}(X)$ has exponentials,
3. Each ${\mathrm{Opf}}_{\mathrm{Fib}(X)}(A\to X)$ and ${\mathrm{Fib}}_{\mathrm{Opf}(X)}(A\to X)$ has exponentials,
4. and so on.

Since duality involutions are stable under fibrational slicing, Corollary 3 implies that if $K$ has exponentials and a duality involution, then it has local exponentials. It would be nice to have a finite list of axioms that implies local exponentials without invoking a duality involution (since not all Grothendieck 2-toposes have dualities).

Corollary

If $K$ has exponentials, then the 2-categories $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$ are all cartesian closed.

Proof

Combine Propositions 5 and 2.

Corollary

If $K$ has exponentials, then the categories $\mathrm{DFib}(X)$ and $\mathrm{DOpf}(X)$ are all locally cartesian closed.

Proof

Since right adjoints preserve discrete objects, Corollary 4 implies that $\mathrm{DFib}(X)$ and $\mathrm{DOpf}(X)$ are cartesian closed for any $X$. Now, given a discrete fibration $A\to X$, we have ${\mathrm{Fib}}_K(A)\simeq {\mathrm{Fib}}_{\mathrm{Fib}(X)}(A\to X)$ by the theorem on iterated fibrations, and so ${\mathrm{DFib}}_K(A)\simeq {\mathrm{DFib}}_{\mathrm{Fib}(X)}(A\to X)\simeq {\mathrm{DFib}}_K(X)/(A\to X)$. Thus, since ${\mathrm{DFib}}_K(A)$ is cartesian closed, so is ${\mathrm{DFib}}_K(X)/(A\to X)$, and thus ${\mathrm{DFib}}_K(X)$ is locally cartesian closed.

Left Kan extensions

We now turn to the existence of left and right adjoints to pullback functors. So far what we know is

• $f^{*}:K/Y\to K/X$ always has a left adjoint ${\Sigma }_f$ given by composition with $f$.
• If $K$ has exponentials and $f$ is a fibration or opfibration, then (by definition) $f^{*}:K/Y\to K/X$ has a right adjoint ${\Pi }_f$.
• If $K$ has a comprehensive factorization (such as when it is countably-coherent), then $f^{*}:\mathrm{DFib}(Y)\to \mathrm{DFib}(X)$ and $f^{*}:\mathrm{DOpf}(Y)\to \mathrm{DOpf}(X)$ have left adjoints ${\mathrm{Lan}}_f$, which satisfy the Beck-Chevalley condition for comma squares.

Note that even if $f$ is a fibration, so that ${\Sigma }_f$ maps $\mathrm{Fib}(Y)$ to $\mathrm{Fib}(X)$, it will not in general be a left adjoint to $f^{*}:\mathrm{Fib}(X)\to \mathrm{Fib}(Y)$. However, if $f$ is a discrete fibration, then ${\Sigma }_f:\mathrm{DFib}(Y)\to \mathrm{DFib}(X)$ is left adjoint to $f^{*}:\mathrm{DFib}(X)\to \mathrm{DFib}(Y)$, since $\mathrm{DFib}(X)$ is a full sub-2-category of $K/X$.

We now consider how to construct left adjoints for non-discrete fibrations.

Proposition

If $K$ has exponentials and reflexive codescent objects, then each pullback functor $f^{*}:\mathrm{Fib}(Y)\to \mathrm{Fib}(X)$ and $f^{*}:\mathrm{Opf}(Y)\to \mathrm{Opf}(X)$ has a left adjoint ${\mathrm{Lan}}_f$.

Proof

Because of the existence of ${\Sigma }_f$, by Proposition 4 it suffices to show that $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$ always have reflexive codescent objects; but this follows from Corollary 2.

The basic first-order structure we are interested in doesn’t imply the existence of such codescent objects, and a Heyting 2-pretopos, such as $\mathrm{FinCat}$, need not have them. But they can be constructed with some infinitary structure; see colimits in an n-pretopos.

I do not know whether these adjunctions always satisfy the Beck-Chevalley condition for comma squares (although they do in one important case; see below).

Right Kan extensions

We now consider the existence of right adjoints to pullback functors between fibrational slices.

Proposition

If $K$ has exponentials, then $f^{*}:\mathrm{Opf}(X)\to \mathrm{Opf}(Y)$ and $f^{*}:\mathrm{Fib}(X)\to \mathrm{Fib}(Y)$ have right adjoints ${\mathrm{Ran}}_f$ for any $f$.

Proof

If $f$ is exponentiable in $K$, this follows directly from Lemma 9 and Proposition 4. In particular, this applies when $f$ is a fibration or opfibration.

Now let $f:Y\to X$ be any morphism, and consider the comma square:

Suppose first that all the left adjoints ${\mathrm{Lan}}_g$ exist for opfibrational slices and satisfy the Beck-Chevalley condition for comma squares. Then this comma square gives us an equivalence $f^{*}\simeq {\mathrm{Lan}}_t{s}^{*}$, so that $f^{*}:\mathrm{Opf}(X)\to \mathrm{Opf}(Y)$ has the right adjoint ${\mathrm{Ran}}_f:={\mathrm{Ran}}_s{t}^{*}$.

We now show that regardless of the overall existence of left adjoints, the particular value ${\mathrm{Lan}}_t{s}^{*}(A)$ exists for any $A\in \mathrm{Opf}(X)$ and is given by $f^{*}A$. This clearly suffices to prove the result.

According to the proof of Proposition 6, ${\mathrm{Lan}}_t{s}^{*}(A)$ should be given by the codescent object of

where

$$\begin{array}{rl}T=& {\Sigma }_t{s}^{*}A{\times }_Y{Y}^2\\ S=& {\Sigma }_t(s^{*}A{\times }_{(1/f)}(1/f{)}^2){\times }_Y{Y}^2\\ R=& {\Sigma }_t(s^{*}A{\times }_{(1/f)}(1/f{)}^2{\times }_{(1/f)}(1/f{)}^2){\times }_Y{Y}^2.\end{array}$$\begin{aligned} T =& \Sigma_t s^* A \times_Y Y ^{\mathbf{2}}\\ S =& \Sigma_t \left(s^* A\times_{(1/f)} (1/f)^{\mathbf{2}}\right) \times_Y Y ^{\mathbf{2}}\\ R =& \Sigma_t \left(s^* A\times_{(1/f)} (1/f)^{\mathbf{2}} \times_{(1/f)} (1/f)^{\mathbf{2}}\right) \times_Y Y ^{\mathbf{2}}. \end{aligned}

Now we have a map

$$q:{\Sigma }_t{s}^{*}A{\times }_Y{Y}^2\to f^{*}A{\times }_Y{Y}^2\to f^{*}A;$$q:\Sigma_t s^* A \times_Y Y ^{\mathbf{2}} \to f^* A \times_Y Y ^{\mathbf{2}} \to f^*A;

the first map is a Beck-Chevalley morphism, and the second comes from the fact that $f^{*}A$ is an opfibration. We claim that $q$ is actually a codescent object of the above diagram, and in fact it is a split codescent object. Recall from

• Claudio Hermida, Descent on 2-fibrations and strongly 2-regular 2-categories.

that a split codescent object is a diagram

with isomorphisms $c\tau \cong \sigma q$, ${\pi }_{12}\mu \cong \tau c$, ${\pi }_{02}\mu \cong \tau d$, $1\cong {\pi }_{01}\mu$, $1\cong d\tau$, and $1\cong q\sigma$ satisfying certain axioms. In this situation, $q$ is necessarily the codescent object of the diagram composed of $d,c,{\pi }_{01},{\pi }_{02},{\pi }_{12}$.

Tracing through the definitions above, we see that our $T$ is the limit of the span $A\to X\leftarrow Y$ weighted by

$$(0)\to (0\to 1\to 2)\leftarrow (1\to 2).$$(0) \;\to\; (0\to 1\to 2) \;\leftarrow\; (1\to 2).

Likewise, $S$ is the limit of $A\to X\leftarrow Y$ weighted by

$$(0)\to \left(\begin{array}{ccc}0& \to & 1\\ \downarrow & & \downarrow \\ 2& \to & 3& \to & 4\end{array}\right)\leftarrow (2\to 3\to 4)$$(0) \;\to\; \left(\array{0&\to&1\\ \downarrow && \downarrow \\ 2 &\to & 3& \to & 4}\right) \;\leftarrow\; (2 \to 3\to 4)

and $R$ is the limit by an evident more complicated weight. Finally, $f^{*}A$ itself is the limit of the same span weighted by

$$(\cdot )\to (\cdot )\leftarrow (\cdot ).$$(\cdot) \;\to\; (\cdot) \;\leftarrow\; (\cdot).

The morphism $q$ is induced by the action of $X$ on the opfibration $A$, applied twice. The morphism $d$ is induced by the inclusion of the second arrow in a composable pair and the action of $X$ on $A$ applied once. The morphism $c$ is induced by the composition of a composable pair. We define the splitting $\sigma ,\tau ,\mu$ in terms of the limit weights by adding in identity morphisms in appropriate places. It is then straightforward to check that the axioms for a split codescent object are satisfied.

Corollary

If $K$ has exponentials, then $f^{*}:\mathrm{DOpf}(X)\to \mathrm{DOpf}(Y)$ and $f^{*}:\mathrm{DFib}(X)\to \mathrm{DFib}(Y)$ have right adjoints ${\mathrm{Ran}}_f$ for any $f$.

Proof

Right adjoints preserve discrete objects.

This completes the proof that exponentiability of fibrations and opfibrations implies all the other notable exponentiability properties we might want to require of a 2-category.

Enrichment

One further observation:

Proposition

If $K$ has exponentials, then each category $\mathrm{DFib}(X)$ is enriched over the cartesian closed category $\mathrm{disc}(K)$.

Proof

We define the hom-object $\mathrm{DFib}(X)(A,B)$ to be ${\mathrm{Ran}}_X{B}^A$, where $B^A$ is the exponential in $\mathrm{DFib}(X)$ and

$${\mathrm{Ran}}_X:\mathrm{DFib}(X)\to \mathrm{DFib}(1)\simeq \mathrm{disc}(K)$$Ran_X:DFib(X) \to DFib(1)\simeq disc(K)

is the right adjoint to $X^{*}$. A composition map is obtained by adjointness in the usual way. We also have

$$\begin{array}{rl}K(1,\mathrm{DFib}(X)(A,B))\cong & K(1,{\mathrm{Ran}}_X{B}^A)\\ \cong & \mathrm{DFib}(X)(1_X,B^A)\\ \cong & \mathrm{DFib}(X)(A,B)\end{array}$$\begin{aligned} K(1,\mathbf{DFib(X)}(A,B)) \cong& K(1, Ran_X B^A)\\ \cong& DFib(X)(1_X, B^A)\\ \cong& DFib(X)(A,B) \end{aligned}

so the underlying ordinary category of this $\mathrm{disc}(K)$-enriched category is the ordinary category $\mathrm{DFib}(X)$.

In fact, more is true: I believe $\mathrm{DFib}(X)$ can be made into a locally internal category, or equivalently a locally small fibration, over $\mathrm{disc}(K)$. Its fiber over a discrete object $Z\in K$ is the category $\mathrm{DFib}(X\times Z)$. This follows by localizing the previous lemma in the slices $\mathrm{Fib}(Z)\simeq K/Z$; one also has to check that a suitable Beck-Chevalley condition is satisfied by the right adjoints ${\mathrm{Ran}}_f$.

An important structure possessed by the 2-category $\mathrm{Cat}$ is the duality involution $(-{)}^{\mathrm{op}}:{\mathrm{Cat}}^{\mathrm{co}}\to \mathrm{Cat}$. Here we consider what the important properties of this involution are that should be generalized to other 2-categories.

Involutions

The most obvious property of $(-{)}^{\mathrm{op}}$ is that it is coherently self-inverse. To state this formally, let $J$ be the walking isomorphism $(0\stackrel{\cong }{\to }1)$, considered as a 3-category with only identity 2-cells and 3-cells. Thus, a (pseudo) functor from $J$ to any 3-category $T$ can be considered an “internal adjoint (bi)equivalence in $T$.” If $T$ is a 3-category, let $C^{3\mathrm{op}}$ denote the 3-cell dual of $T$; note that $J^{3\mathrm{op}}\cong J$ and that $(-{)}^{\mathrm{co}}$ is a functor $2\mathrm{Cat}\to 2{\mathrm{Cat}}^{3\mathrm{op}}$. Finally, let $\tau :J\to J\cong J^{3\mathrm{op}}$ be the evident involution that switches $0$ and $1$.

Definition

A 2-contravariant involution (hereafter merely an involution) on a 2-category $K$ is functor $W:J\to 2\mathrm{Cat}$ such that $W(0)=K$ and the square

$$\begin{array}{ccc}J& \stackrel{\tau }{\to }& J^{3\mathrm{op}}\\ {}^W\downarrow & & {\downarrow }^W\\ 2\mathrm{Cat}& \underset{(-{)}^{\mathrm{co}}}{\to }& 2{\mathrm{Cat}}^{3\mathrm{op}}\end{array}$$\array{J & \overset{\tau}{\to} & J^{3op}\\ ^W \downarrow && \downarrow^W\\ 2Cat & \underset{(-)^{co}}{\to} & 2Cat^{3op}}

commutes (on the nose).

We write $(-{)}^o:K\to K^{\mathrm{co}}$ (or equivalently $K^{\mathrm{co}}\to K$) for the functor $W(0\to 1)$; the rest of the data of $W$ simply says that $((-{)}^o{)}^o\cong \mathrm{Id}$ in a coherent way.

Example

Any (2,1)-category $K$ admits a canonical involution that is the identity on objects and morphisms and sends each 2-cell to its inverse.

Example

Let $C$ be a 2-category equipped with an involution and let $K=[C,\mathrm{Cat}]$. Then $K$ has a canonical induced involution defined by

$$[C,\mathrm{Cat}{]}^{\mathrm{co}}\stackrel{\simeq }{\to }[C^{\mathrm{co}},{\mathrm{Cat}}^{\mathrm{co}}]\stackrel{\simeq }{\to }[C,{\mathrm{Cat}}^{\mathrm{co}}]\stackrel{(-{)}^{\mathrm{op}}\circ -}{\to }[C,\mathrm{Cat}].$$[C,Cat]^{co} \overset{\simeq}{\to} [C^{co},Cat^{co}] \overset{\simeq}{\to} [C, Cat^{co}] \overset{(-)^{op}\circ -}{\to} [C,Cat].

Conversely, if $C$ is Cauchy-complete, then $C^{\mathrm{op}}$ can be identified with the full subcategory of indecomposable projectives in $K$, and thus an involution on $K$ induces an involution on $C$.

Thus, in particular, any (2,1)-truncated 2-presheaf 2-topos admits a canonical involution. However, in general a 2-category that admits an involution will admit many involutions.

Proposition

For any 2-category $K$, the 2-category $\mathrm{Inv}(K)$ of involutions on $K$, if nonempty, is a torsor for the 3-group $\mathrm{Aut}(K)$ of (covariant) automorphisms of $K$.

Proof

Easy.

In particular, any automorphism of a (2,1)-category $C$ induces an involution on $[C,\mathrm{Cat}]$.

Duality Involutions

As observed by WeberYS2T, experience suggests that the most important additional property of the involution $(-{)}^{\mathrm{op}}$ on $\mathrm{Cat}$ is that fibrations over $A$ can be identified with opfibrations over $A^{\mathrm{op}}$, since both are equivalent to functors $A^{\mathrm{op}}\to \mathrm{Cat}$. So it is reasonable to consider, together with an involution $(-{)}^o$ on a 2-category $K$, a family of equivalences $\mathrm{Fib}(X)\simeq \mathrm{Opf}(X^o)$.

The next question is what additional properties should be required of such a family. The following definition is provisional, but I believe whatever eventual definition we settle on should allow the construction of all the data given below.

Definition

A duality involution on a 2-category $K$ is an involution $(-{)}^o$ together with the following data.

1. Equivalences of 2-categories

   $$V_X:\mathrm{Fib}(X)\simeq \mathrm{Opf}(X^o)$$V_X:Fib(X) \simeq Opf(X^o)

   which are natural in $X$ (that is, $V$ is a natural equivalence between functors $K^{\mathrm{coop}}\to 2\mathrm{Cat}$),

2. An equivalence between $V_1:\mathrm{Fib}(1)\simeq \mathrm{Opf}(1^o)$ and the composite $\mathrm{Fib}(1)\simeq K\simeq \mathrm{Opf}(1)\simeq \mathrm{Opf}(1^o)$ (note $1^o\simeq 1$ since $(-{)}^o$ is an equivalence).

3. For any pullback square

   $$\begin{array}{ccc}P& \to & A\\ \downarrow & & \downarrow \\ B& \to & X\end{array}$$\array{P & \to & A\\ \downarrow && \downarrow\\ B & \to & X}

   in which all the displayed maps are fibrations, an invertible modification between the two composites

   $$\begin{array}{c}\mathrm{Fib}(P)\stackrel{V_P}{\to }\mathrm{Opf}(P^o)\simeq {\mathrm{Opf}}_{\mathrm{Opf}(A^o)}(P^o\to A^o)\stackrel{V_A^{-1}}{\to }{\mathrm{Opf}}_{\mathrm{Fib}(A)}(V_A{P}^o\to A)\\ \simeq {\mathrm{Opf}}_{{\mathrm{Fib}}_{\mathrm{Fib}(X)}(A\to X)}(V_A{P}^o\to A)\simeq {\mathrm{Fib}}_{\mathrm{Fib}(X)}(V_X^{-1}{B}^o,A)\end{array}$$\begin{gathered} Fib(P) \overset{V_P}{\to} Opf(P^o) \simeq Opf_{Opf(A^o)}(P^o\to A^o) \overset{V_A^{-1}}{\to} Opf_{Fib(A)}(V_A P^o \to A)\\ \simeq Opf_{Fib_{Fib(X)}(A\to X)}(V_A P^o\to A) \simeq Fib_{Fib(X)}(V_X^{-1} B^o, A) \end{gathered}

   and

   $$\begin{array}{c}\mathrm{Fib}(P)\simeq {\mathrm{Fib}}_{\mathrm{Fib}(B)}(P\to B)\stackrel{V_B}{\to }{\mathrm{Fib}}_{\mathrm{Opf}(B^o)}(V_{B}P\to B^o)\simeq {\mathrm{Fib}}_{{\mathrm{Opf}}_{\mathrm{Opf}(X^o)}(B^o\to X^o)}(V_{B}P\to B^o)\\ \stackrel{V_X^{-1}}{\to }{\mathrm{Fib}}_{{\mathrm{Opf}}_{\mathrm{Fib}(X)}(V_X^{-1}{B}^o\to X)}(V_X^{-1}{V}_{B}P\to V_X^{-1}{B}^o)\simeq {\mathrm{Fib}}_{\mathrm{Fib}(X)}(V_X^{-1}{B}^o,A).\end{array}$$\begin{gathered} Fib(P) \simeq Fib_{Fib(B)}(P\to B) \overset{V_B}{\to} Fib_{Opf(B^o)}(V_B P\to B^o) \simeq Fib_{Opf_{Opf(X^o)}(B^o\to X^o)}(V_B P\to B^o)\\ \overset{V_X^{-1}}{\to} Fib_{Opf_{Fib(X)}(V_X^{-1} B^o\to X)}(V_X^{-1} V_B P\to V_X^{-1} B^o) \simeq Fib_{Fib(X)}(V_X^{-1} B^o, A). \end{gathered}

4. An invertible modification filling the square

   $$\begin{array}{ccc}\mathrm{Fib}(X)& \stackrel{V_X}{\to }& \mathrm{Opf}(X^o)\\ (-{)}^o\downarrow & & \downarrow (-{)}^o\\ \mathrm{Opf}(X^o{)}^{\mathrm{co}}& \underset{V_X^{-1}}{\to }& \mathrm{Fib}(X{)}^{\mathrm{co}}.\end{array}$$\array{Fib(X) & \overset{V_X}{\to} & Opf(X^o)\\ (-)^o\downarrow && \downarrow (-)^o\\ Opf(X^o)^{co}& \underset{V_X^{-1}}{\to} & Fib(X)^{co}.}

   which commutes with the previous two equivalences.

Perhaps there should also be some coherence data and axioms relating these data to each other.

The first two data should be fairly self-explanatory, but the third datum may seem quite complicated. In fact, it requires some thought to see that the two displayed composites are even well-defined. Note first that since $P=A{\times }_{X}B$, by naturality of $V$ we have $V_{B}P\simeq B^o{\times }_{X^o}{V}_{X}A$, and thus $V_X^{-1}{V}_{B}P\simeq V_X^{-1}{B}^o{\times }_{X}A$. Also, $P^o\simeq B^o{\times }_{X^o}{A}^o$, so again by naturality $V_A^{-1}{P}^o\simeq V_X^{-1}{B}^o{\times }_{X}A$. Thus $V_X^{-1}{V}_{B}P\simeq V_A^{-1}{P}^o$, and the final two equivalences in each displayed composite are instances of the theorem on iterated fibrations. One way to think about this datum is as sort of an “inclusion-exclusion” property for reversal of arrows.

We call the final datum commutation of opposites. To explain it, observe that because $(-{)}^o$ is a 2-contravariant involution, we automatically have equivalences ${\mathrm{Fib}}_K(X)\simeq {\mathrm{Fib}}_{K^{\mathrm{co}}}(X^o)={\mathrm{Opf}}_K(X^o{)}^{\mathrm{co}}$ (these are the vertical maps in the displayed square). In $\mathrm{Cat}$, this equivalence corresponds to composing a functor $A^{\mathrm{op}}\to \mathrm{Cat}$ with $(-{)}^{\mathrm{op}}:\mathrm{Cat}\to \mathrm{Cat}$ as well as reinterpreting it as an opfibration. Commutation of opposites then says that this operation commutes with $V$.

One immediate application of commutation of opposites is to deduce a version of the third datum for a pullback square of opfibrations, by passage along the equivalences $\mathrm{Fib}(X)\simeq \mathrm{Opf}(X^o{)}^{\mathrm{co}}$. We will see others below.

Example

If $K$ is a (2,1)-category, then its canonical involution extends to a canonical duality involution, since $\mathrm{Fib}(X)\simeq K/X\simeq \mathrm{Opf}(X)$.

Example

If $C$ is a (2,1)-category, then the canonical involution on $K=[C,\mathrm{Cat}]$ extends in a natural way to a duality involution. This does not seem to be the case if $C$ is merely a 2-category equipped with an involution.

The 3-group $\mathrm{Aut}(K)$ also acts on the 2-category $\mathrm{DualInv}(K)$ of duality involutions on $K$; the action is free but (seemingly) no longer necessarily transitive. However, I do not know an example of two inequivalent duality involutions having the same underlying involution (as would be necessary for non-transitivity).

The differences between Definition 13 and the definition of WeberYS2T are threefold.

1. Our definition is less strict; $(-{)}^o$ is only required to be self-inverse in a 2-categorically non-evil way.
2. Our definition refers to arbitrary fibrations and opfibrations, rather than merely discrete ones.
3. Our definition refers only to one-sided fibrations, whereas WeberYS2T requires an equivalence $\mathrm{DFib}(A\times B,C)\simeq \mathrm{DFib}(A,B^o\times C)$.

Of course, since any equivalence of 2-categories preserves discrete objects, our definition implies an equivalence $\mathrm{DFib}(X)\simeq \mathrm{DOpf}(X^o)$. More surprisingly, it turns out that the seemingly stronger two-sided version is a consequence of our definition.

Theorem

If $K$ is equipped with a duality involution, then we have natural equivalences $\mathrm{Fib}(A\times B,C)\simeq \mathrm{Fib}(A,B^o\times C)$.

Proof

We first construct an equivalence $\mathrm{Opf}(A\times B)\simeq \mathrm{Fib}(A,B^o)$. Note that since $\mathrm{Fib}(1)\simeq \mathrm{Opf}(1^o)$ is the identity, naturality implies that $V_A(A\times B)\simeq A^o\times B$. Also, since $(-{)}^o$ is an equivalence, and products in $K$ are the same as products in $K^{\mathrm{co}}$, we have $(A\times B{)}^o\simeq A^o\times B^o$. Now we have the composite equivalence (using the theorem on iterated fibrations):

$$\mathrm{Opf}(A\times B)\simeq {\mathrm{Opf}}_{\mathrm{Opf}(B)}(A\times B\to B)\stackrel{V_B}{\to }{\mathrm{Opf}}_{\mathrm{Fib}(B^o)}(A\times B^o\to B^o)\simeq \mathrm{Fib}(A,B^o).$$Opf(A\times B) \simeq Opf_{Opf(B)}(A\times B \to B) \overset{V_B}{\to} Opf_{Fib(B^o)}(A\times B^o \to B^o) \simeq Fib(A,B^o).

Note that there is also another equivalence

$$\mathrm{Opf}(A\times B)\stackrel{V_{A\times B}}{\to }\mathrm{Fib}((A\times B{)}^o)\simeq {\mathrm{Fib}}_{\mathrm{Fib}(A^o)}(A^o\times B^o\to A^o)\stackrel{V_A}{\to }{\mathrm{Fib}}_{\mathrm{Opf}(A)}(A\times B^o\to A)\simeq \mathrm{Fib}(A,B^o),$$Opf(A\times B) \overset{V_{A\times B}}{\to} Fib((A\times B)^o) \simeq Fib_{Fib(A^o)}(A^o\times B^o\to A^o) \overset{V_A}{\to} Fib_{Opf(A)}(A\times B^o\to A) \simeq Fib(A,B^o),

but the second and third data in the definition of a duality involution supply a canonical equivalence between these composites, so it doesn’t matter which we use. Finally, for the general case, we simply apply this twice:

$$\mathrm{Fib}(A\times B,C)\simeq \mathrm{Opf}(A\times B\times C^o)\simeq \mathrm{Opf}(A\times (B^o\times C{)}^o)\simeq \mathrm{Fib}(A,B^o\times C).$$Fib(A\times B, C) \simeq Opf(A\times B\times C^o) \simeq Opf(A\times (B^o\times C)^o) \simeq Fib(A, B^o\times C).

This gives our desired equivalence.

Note, though, that this proof crucially requires that the duality involution come with an equivalence $\mathrm{Fib}(X)\simeq \mathrm{Opf}(X^o)$, and not merely $\mathrm{DFib}(X)\simeq \mathrm{DOpf}(X^o)$.

Commutation of opposites, which we have not yet used, is necessary for the following important, and perhaps also surprising, result: duality involutions are preserved by (fibrational) slicing.

Theorem

Any duality involution on $K$ induces a duality involution on each fibrational slice ${\mathrm{Fib}}_K(X)$ and ${\mathrm{Opf}}_K(X)$.

Proof

We define $(-{)}^{o_X}:\mathrm{Fib}(X{)}^{\mathrm{co}}\to \mathrm{Fib}(X)$ to be the composite

$$\mathrm{Fib}(X)\stackrel{(-{)}^o}{\to }\mathrm{Opf}(X^o{)}^{\mathrm{co}}\stackrel{V_X^{-1}}{\to }\mathrm{Fib}(X{)}^{\mathrm{co}}.$$Fib(X) \overset{(-)^o}{\to} Opf(X^o)^{co} \overset{V_{X}^{-1}}{\to} Fib(X)^{co}.

To show that $(-{)}^{o_X}$ is an involution, we verify

$$(A^{o_X}{)}^{o_X}=V_X^{-1}((V_X^{-1}(A^o){)}^o)\simeq V_X^{-1}(V_X((A^o{)}^o))\simeq (A^o{)}^o\simeq A.$$(A^{o_X})^{o_X} = V_X^{-1}((V_X^{-1}(A^o))^o) \simeq V_X^{-1}(V_X((A^o)^o)) \simeq (A^o)^o \simeq A.

Here we use commutation of opposites in $K$ to commute $(-{)}^o$ past $V_X$. We now define

$$V_A^X:{\mathrm{Fib}}_{\mathrm{Fib}(X)}(A)\simeq {\mathrm{Opf}}_{\mathrm{Fib}(X)}(A^{o_X})$$V^X_A: Fib_{Fib(X)}(A) \simeq Opf_{Fib(X)}(A^{o_X})

to be the composite

$${\mathrm{Fib}}_{\mathrm{Fib}(X)}(A)\simeq \mathrm{Fib}(A)\stackrel{V_A}{\to }\mathrm{Opf}(A^o)\simeq {\mathrm{Opf}}_{\mathrm{Opf}(X^o)}(A^o)\stackrel{V_X^{-1}}{\to }{\mathrm{Opf}}_{\mathrm{Fib}(X)}(V_X(A^o))={\mathrm{Opf}}_{\mathrm{Fib}(X)}(A^{o_X}).$$Fib_{Fib(X)}(A) \simeq Fib(A) \overset{V_A}{\to} Opf(A^o) \simeq Opf_{Opf(X^o)}(A^o) \overset{V_X^{-1}}{\to} Opf_{Fib(X)}(V_X(A^o)) = Opf_{Fib(X)}(A^{o_X}).

It is easy to see that $V_{1_X}^X\simeq V_X^{-1}\circ V_X\simeq 1$, and to construct the pullback-commutation equivalence. Finally, we construct commutation of opposites in $\mathrm{Fib}(X)$ as the composite

$$(V_A^X(B){)}^{o_X}\simeq V_X^{-1}((V_X^{-1}(V_A(B)){)}^o)\simeq V_X^{-1}(V_X((V_A(B){)}^o))\simeq (V_A(B){)}^o\simeq V_A^{-1}(B^o)\simeq V_A^{-1}(V_X(V_X^{-1}(B^o)))=(V_A^X{)}^{-1}(B^{o_X}).$$(V^X_A(B))^{o_X} \simeq V_X^{-1}((V_X^{-1}(V_A(B)))^o) \simeq V_X^{-1}(V_X((V_A(B))^o)) \simeq (V_A(B))^o\simeq V_A^{-1}(B^o)\simeq V_A^{-1}(V_X(V_X^{-1}(B^o))) = (V^X_A)^{-1}(B^{o_X}).

The case of $\mathrm{Opf}(X)$ is dual.

Fixing groupoids

We saw above that in general, a 2-category admitting an involution or duality involution will admit many. One way to get rid of some of these spurious involutions is to require that $(-{)}^o$ fix groupoidal objects, as is clearly the case for the involution of $\mathrm{Cat}$ and the “canonical” involutions of (2,1)-truncated 2-presheaf 2-toposes.

Note that any involution takes groupoidal objects to groupoidal objects.

Definition

An involution $(-{)}^o$ on $K$ fixes groupoids it it restricts to the canonical involution on $\mathrm{gpd}(K)$, i.e. if $X^o\simeq X$ coherently whenever $X$ is groupoidal.

Lemma

If $K$ is a regular $n$-category having enough groupoids, then it admits, up to equivalence, at most one involution that fixes groupoids. If $K$ is also $n$-exact, then it admits exactly one such involution.

Proof

Suppose that $(-{)}^o$ is an involution on $K$ that fixes groupoids. Then for any $A$ and any groupoidal $X$, we have

$$K(X,A^o)\cong K^{\mathrm{co}}(X^o,A)\cong K^{\mathrm{co}}(X,A)\cong K(X,A{)}^{\mathrm{op}}.$$K(X,A^o) \cong K^{co}(X^o,A) \cong K^{co}(X,A) \cong K(X,A)^{op}.

Now given $B$ as well, with an eso $p:X\to B$ where $X$ is groupoidal, any morphism $B\to A^o$ is determined by a map $X\to A^o$ with an action by $\ker (p)$. But $\ker (p)=(p/p)$ is also groupoidal, so morphisms $B\to A^o$ are completely determined by morphisms to $A$ out of groupoidal objects. Thus, by the Yoneda lemma, any two values of $A^o$ must be canonically isomorphic.

Now suppose $K$ is exact, and let $p:X\to A$ be an eso where $X$ is groupoidal. Then its kernel $(p/p)$ is also groupoidal, and so $\ker (p)$ is a homwise-discrete category in $\mathrm{gpd}(K)$. Thus we can consider its opposite, which is also a homwise-discrete category in $\mathrm{gpd}(K)$. In general, the opposite of a 2-congruence in a 2-category will not be a 2-congruence, since the condition of being a two-sided fibration is not preserved. But in a (2,1)-category such as $\mathrm{gpd}(K)$, this extra condition is automatic, so this opposite of is also a 2-congruence in $\mathrm{gpd}(K)$ (and, in fact, an $n$-congruence when $K$ is an $n$-category). Thus, since $K$ is $n$-exact, this opposite has a quotient, which we call $A^o$. It is straightforward to verify that this defines an involution on $K$ that fixes groupoids.

Of course, the only interesting values of $n$ in the above lemma are 2 and (1,2), since any groupoid-fixing involution on a (2,1)-category is equivalent to the canonical one. Of particular note is that any (2,1)-truncated Grothendieck 2-topos admits a unique groupoid-fixing involution.

In fact, this groupoid-fixing involution should also extend to a duality involution. For when $K$ is $n$-exact, the functor $\mathrm{Opf}:K^{\mathrm{op}}\to 2\mathrm{Cat}$ ought to be a 3-sheaf? (a 2-stack). This means that if $p:X\to A$ is an eso with $X$ groupoidal, then $\mathrm{Opf}(A)$ can be reconstructed from $\mathrm{Opf}(X)$ and $\mathrm{Opf}(p/p)$ with descent data. Similarly, $\mathrm{Fib}:K^{\mathrm{coop}}\to 2\mathrm{Cat}$ should also be a 3-sheaf, and so $\mathrm{Fib}(A)$ can be recovered from $\mathrm{Fib}(X)$ and $\mathrm{Fib}(p/p)$ with “op-descent data.” But since $X$ is groupoidal, $\mathrm{Opf}(X)\simeq \mathrm{Fib}(X)$, and likewise for $(p/p)$. Therefore, descent data for $\ker (p)$ over $\mathrm{Opf}(X)$, which determines an object of $\mathrm{Opf}(A)$, is the same as op-descent data for the opposite of $\ker (p)$ over $\mathrm{Fib}(X)$, which determines an object of $\mathrm{Fib}(A^o)$. This gives the equivalence $\mathrm{Opf}(A)\simeq \mathrm{Fib}(A^o)$.

Alternately, there is also a stronger theorem that if $K$ is 2-exact with enough groupoids, then it is equivalent to a particular 2-category of internal categories and anafunctors in the (2,1)-category $\mathrm{gpd}(K)$ (more precisely, it is the 2-exact completion of $\mathrm{gpd}(K)$). And it is fairly easy to see, by its construction, that this 2-category has a duality involution, just as the 2-category of internal categories in any 1-category does.

Modulo the action of automorphisms, these are the only examples of duality involutions that I know. I do not know an example of a duality involution on a 2-category that does not have enough groupoids.

Fixing groupoids locally

Now, since a duality involution on $K$ extends to a duality involution on ${\mathrm{Fib}}_K(X)$ and ${\mathrm{Opf}}_K(X)$, it is natural to strengthen the notion of groupoid-fixing so that it carries over to fibrational slices. We write $\mathrm{GFib}(X)=\mathrm{gpd}(\mathrm{Fib}(X))$ and similarly $\mathrm{GOpf}(X)$.

Definition

A duality involution $(-{)}^o$ on $K$ fixes groupoids locally if we have a equivalence modification between $V_X:\mathrm{GFib}(X)\to \mathrm{GOpf}(X^o)$ and the composite $\mathrm{GFib}(X)\stackrel{(-{)}^o}{\to }\mathrm{GOpf}(X^o{)}^{\mathrm{co}}\simeq \mathrm{GOpf}(X^o)$.

The latter equivalence $\mathrm{GOpf}(X^o{)}^{\mathrm{co}}\simeq \mathrm{GOpf}(X^o)$ is the canonical involution on the (2,1)-category $\mathrm{GOpf}(X^o)$. Taking $X=1$, together with the second condition in the definition of a duality involution, this implies that $(-{)}^o$ fixes groupoids in the previous sense. Moreover, we have:

Theorem

If $(-{)}^o$ is a duality involution that fixes groupoids locally, then the induced duality involutions on $\mathrm{Fib}(X)$ and $\mathrm{Opf}(X)$ also fix groupoids locally.

Proof

For a fibration $A\to X$, on ${\mathrm{Fib}}_{\mathrm{Fib}(X)}(A)$ we have $(-{)}^{o_X}=V_X^{-1}\circ (-{)}^o$ and $V_A^X=V_X^{-1}\circ V_A$, so the equivalence between $(-{)}^o$ and $V_A$ in $K$ induces one between $(-{)}^{o_X}$ and $V_A^X$ in $\mathrm{Fib}(X)$.

Now, suppose that $(-{)}^o$ is a duality involution that fixes groupoids locally. Then for any $A$ and $B$, the pullback-commutation datum shows that the composite equivalence

$$\mathrm{Fib}(A\times B^o)\simeq \mathrm{Fib}(B,A)\simeq \mathrm{Opf}(A^o\times B)\simeq \mathrm{Opf}((A\times B^o{)}^o)$$Fib(A\times B^o) \simeq Fib(B,A) \simeq Opf(A^o\times B)\simeq Opf((A\times B^o)^o)

derived from Theorem 12 is equivalent to $V_{A\times B^o}$. But if we restrict to groupoidal fibrations, then

$$V_{A\times B^o}:\mathrm{GFib}(A\times B^o)\simeq \mathrm{GOpf}(A^o\times B)$$V_{A\times B^o}:GFib(A\times B^o) \simeq GOpf(A^o\times B)

is equivalent to $(-{)}^o$. Together with commutation of opposites, this implies that the canonical equivalence

$$\mathrm{GFib}(B,A)\simeq \mathrm{GFib}(A^o,B^o)$$GFib(B,A)\simeq GFib(A^o,B^o)

is, up to equivalence, simply given by $(-{)}^o$. In particular, since $(-{)}^o$ preserves powers, the canonical equivalence

$$\mathrm{DFib}(A,A)\simeq \mathrm{DFib}(A^o,A^o)$$DFib(A,A)\simeq DFib(A^o,A^o)

takes $A^2$ to $(A^o{)}^2$. In the 2-internal logic, this corresponds to the statement that ”${\mathrm{hom}}_A(x,y)\cong {\mathrm{hom}}_{A^o}(y,x)$,” which is certainly an expected part of the behavior of opposite categories. Of course, for this it suffices that $(-{)}^o$ fix discretes locally, which has the evident definition.

Further axioms

Another natural requirement is that when $X$ is groupoidal, $V_X$ should be equivalent to the composite

$$\mathrm{Fib}(X)\simeq K/X\simeq \mathrm{Opf}(X)\simeq \mathrm{Opf}(X^o).$$Fib(X)\simeq K/X \simeq Opf(X)\simeq Opf(X^o).

Note that this includes the second datum in the definition of a duality involution as a special case, since $1$ is groupoidal. There seems no reason for this condition to be stable under slicing, but it could be stabilized.

Grothendieck 2-toposes

Definition

A Grothendieck 2-topos is a 2-category that is equivalent to the 2-category of 2-sheaves (aka stacks) on some 2-site. More generally, a Grothendieck $n$-topos is an $n$-category that is equivalent to the $n$-category of $n$-sheaves on some $n$-site (for $n\le 2$); see truncated 2-topos.

The 2-Giraud theorem due to StreetCBS characterizes Grothendieck $n$-toposes as the infinitary n-pretoposes having a small eso-generating set of objects.

Cores and opposites

The most familiar Grothendieck 2-toposes are those of 2-sheaves on a 1-site. Even 2-presheaves on a 2-category that is not a 1-category can exhibit unexpected behavior; for instance they do not in general have cores or opposites. (2-presheaves on a (2,1)-category do have cores and opposites, though.)

The 2-Giraud theorem implies that if $K$ is a Grothendieck 2-topos, so is $K^{\mathrm{co}}$. In the case of 2-presheaves, we can identify this as:

$$[C,\mathrm{Cat}{]}^{\mathrm{co}}\simeq [C^{\mathrm{co}},{\mathrm{Cat}}^{\mathrm{co}}]\simeq [C^{\mathrm{co}},\mathrm{Cat}]$$[C,Cat]^{co} \simeq [C^{co},Cat^{co}] \simeq [C^{co},Cat]

since we have $(-{)}^{\mathrm{op}}:{\mathrm{Cat}}^{\mathrm{co}}\simeq \mathrm{Cat}$. In other words, the “2-topos of presheaves” functor from 2-categories to 2-toposes preserves the 2-cell-dual involution. Another way to say this is that only for 2-sheaves on a (2,1)-category is “oppositization” an endofunctor; in other cases “passage to opposites” means passage to a different 2-topos.

2-sheaves (stacks) on a 2-site

Definition

A coverage on a 2-category $C$ consists of, for each object $U\in C$, a collection of families $(f_i:U_i\to U{)}_i$ of morphisms with codomain $U$, called covering families, such that

• If $(f_i:U_i\to U{)}_i$ is a covering family and $g:V\to U$ is a morphism, then there exists a covering family $(h_j:V_j\to V{)}_j$ such that each composite $g{h}_j$ factors through some $f_i$, up to isomorphism.

This is the 2-categorical analogue of the 1-categorical notion of coverage introduced in the Elephant.

A 2-category equipped with a coverage is called a 2-site.

Examples

• If $C$ is a regular 2-category, then the collection of all singleton families $(f:V\to U)$, where $f$ is eso, forms a coverage called the regular coverage.

• Likewise, if $C$ is a coherent 2-category, the collection of all finite jointly-eso families forms a coverage called the coherent coverage.

• On $\mathrm{Cat}$, the canonical coverage consists of all families that are jointly essentially surjective on objects.

2-sheaves

Let $C$ be a 2-site having finite limits (for convenience). For a covering family $(f_i:U_i\to U{)}_i$ we have the comma objects

We also have the double comma objects $(f_i/f_j/f_k)=(f_i/f_j){\times }_{U_j}(f_j/f_k)$ with projections $r_{ijk}:(f_i/f_j/f_k)\to (f_i/f_j)$, $s_{ijk}:(f_i/f_j/f_k)\to (f_j/f_k)$, and $t_{ijk}:(f_i/f_j/f_k)\to (f_i/f_k)$.

Now, a functor $X:C^{\mathrm{op}}\to \mathrm{Cat}$ is called a 2-presheaf. It is 1-separated if

• For any covering family $(f_i:U_i\to U{)}_i$ and any $x,y\in X(U)$ and $a,b:x\to y$, if $X(f_i)(a)=X(f_i)(b)$ for all $i$, then $a=b$.

It is 2-separated if it is 1-separated and

• For any covering family $(f_i:U_i\to U{)}_i$ and any $x,y\in X(U)$, given $b_i:X(f_i)(x)\to X(f_i)(y)$ such that ${\mu }_{ij}(y)\circ X(p_{ij})(b_i)=X(q_{ij})(b_i)\circ {\mu }_{ij}(x)$, there exists a (necessarily unique) $b:x\to y$ such that $b_i=X(f_i)(b)$.

It is a 2-sheaf if it is 2-separated and

• For any covering family $(f_i:U_i\to U{)}_i$ and any $x_i\in X(U_i)$ together with morphisms ${\zeta }_{ij}:X(p_{ij})(x_i)\to X(q_{ij})(x_j)$ such that the following diagram commutes:

  $$\begin{array}{ccccc}X(r_{ijk})X(p_{ij})(x_i)& \stackrel{X(r_{ijk})({\zeta }_{ij})}{\to }& X(r_{ijk})X(q_{ij})(x_j)& \stackrel{\cong }{\to }& X(s_{ijk})X(p_{jk})(x_j)\\ {}^{\cong }\downarrow & & & & {\downarrow }^{X(s_{ijk})({\zeta }_{jk})}\\ X(t_{ijk})X(p_{ik})(x_i)& \underset{X(t_{ijk})({\zeta }_{ik})}{\to }& X(t_{ijk})X(q_{ik})(x_k)& \underset{\cong }{\to }& X(s_{ijk})X(q_{jk})(x_k)\end{array}$$\array{X(r_{i j k})X(p_{i j})(x_i) & \overset{X(r_{i j k})(\zeta_{i j})}{\to} & X(r_{i j k})X(q_{i j})(x_j) & \overset{\cong}{\to} & X(s_{i j k})X(p_{j k})(x_j)\\ ^\cong \downarrow && && \downarrow ^{X(s_{i j k})(\zeta_{j k})}\\ X(t_{i j k}) X(p_{i k})(x_i) & \underset{X(t_{i j k})(\zeta_{i k})}{\to} & X(t_{i j k}) X(q_{i k})(x_k) & \underset{\cong}{\to} & X(s_{i j k}) X(q_{j k})(x_k)}

  there exists an object $x\in X(U)$ and isomorphisms $X(f_i)(x)\cong x_i$ such that for all $i,j$ the following square commutes:

  $$\begin{array}{ccc}X(p_{ij})X(f_i)(X)& \stackrel{\cong }{\to }& X(p_{ij})(x_i)\\ {}^{X({\mu }_{ij})}\downarrow & & {\downarrow }^{{\zeta }_{ij}}\\ X(q_{ij})X(f_j)(x)& \underset{\cong }{\to }& X(q_{ij})(x_j).\end{array}$$\array{ X(p_{i j})X(f_i)(X) & \overset{\cong}{\to} & X(p_{i j})(x_i)\\ ^{X(\mu_{i j})}\downarrow && \downarrow^{\zeta_{i j}}\\ X(q_{i j})X(f_j)(x) & \underset{\cong}{\to} & X(q_{i j})(x_j).}

A 2-sheaf, especially on a 1-site, is frequently called a stack. However, this has the unfortunate consequence that a 3-sheaf is then called a 2-stack, and so on with the numbering all offset by one. Also, it can be helpful to use a new term because of the notable differences between 2-sheaves on 2-sites and 2-sheaves on 1-sites. The main novelty is that ${\mu }_{ij}$ and ${\zeta }_{ij}$ need not be invertible.

Note, though, they must be invertible as soon as $C$ is (2,1)-site: ${\mu }_{ij}$ by definition and ${\zeta }_{ij}$ since an inverse is provided by ${\iota }_{ij}^{*}({\zeta }_{ij})$, where ${\iota }_{ij}maps(f_i/f_j)\to (f_j/f_i)$ is the symmetry equivalence.

If $C$ lacks finite limits, then in the definitions of “2-separated” and “2-sheaf” instead of the comma objects $(f_i/f_j)$, we need to use arbitrary objects $V$ equipped with maps $p:V\to U_i$, $q:V\to U_j$, and a 2-cell $f_{i}p\to f_{j}q$. We leave the precise definition to the reader.

A 2-site is said to be subcanonical if for any $U\in C$, the representable functor $C(-,U)$ is a 2-sheaf. When $C$ has finite limits, it is easy to verify that this is true precisely when every covering family is a (necessarily pullback-stable) quotient of its kernel 2-polycongruence. In particular, the regular coverage on a regular 2-category is subcanonical, as is the coherent coverage on a coherent 2-category.

The 2-category $2\mathrm{Sh}(C)$ of 2-sheaves on a small 2-site $C$ is, by definition, a Grothendieck 2-topos.

Saturation conditions

A pre-Grothendieck coverage on a 2-category is a coverage satisfying the following additional conditions:

• If $f:V\to U$ is an equivalence, then the one-element family $(f:V\to U)$ is a covering family.

• If $(f_i:U_i\to U{)}_{i\in I}$ is a covering family and for each $i$, so is $(h_{ij}:U_{ij}\to U_i{)}_{j\in J_i}$, then $(f_i{h}_{ij}:U_{ij}\to U{)}_{i\in I,j\in U_i}$ is also a covering family.

This is the 2-categorical version of a Grothendieck pretopology.

Now, a sieve on an object $U\in C$ is defined to be a functor $R:C^{\mathrm{op}}\to \mathrm{Cat}$ with a transformation $R\to C(-,U)$ which is objectwise fully faithful (equivalently, it is ff in $[C^{\mathrm{op}},\mathrm{Cat}]$). Every family $(f_i:U_i\to U{)}_i$ generates a sieve by defining $R(V)$ to be the full subcategory of $C(V,U)$ on those $g:V\to U$ such that $g\cong f_{i}h$ for some $i$ and some $h:V\to U_i$. The following observation is due to StreetCBS.

Lemma

A 2-presheaf $X:C^{\mathrm{op}}\to \mathrm{Cat}$ is a 2-sheaf for a covering family $(f_i:U_i\to U{)}_i$ if and only if

$$X(U)\simeq [C^{\mathrm{op}},\mathrm{Cat}](C(-,U),X)\to [C^{\mathrm{op}},\mathrm{Cat}](R,X)$$X(U) \simeq[C^{op},Cat](C(-,U),X) \to [C^{op},Cat](R,X)

is an equivalence, where $R$ is the sieve on $U$ generated by $(f_i:U_i\to U{)}_i$.

Therefore, just as in the 1-categorical case, it is natural to restrict attention to covering sieves. We define a Grothendieck coverage on a 2-category $C$ to consist of, for each object $U$, a collection of sieves on $U$ called covering sieves, such that

• If $R$ is a covering sieve on $U$ and $g:V\to U$ is any morphism, then $g^{*}(R)$ is a covering sieve on $V$.

• For each $U$ the sieve $M_U$ consisting of all morphisms into $U$ (the sieve generated by the singleton family $(1_U)$) is a covering sieve.

• If $R$ is a covering sieve on $U$ and $S$ is an arbitrary sieve on $U$ such that for each $f:V\to U$ in $R$, $f^{*}(S)$ is a covering sieve on $V$, then $S$ is also a covering sieve on $U$.

Here if $R$ is a sieve on $U$ and $g:V\to U$ is a morphism, $g^{*}(R)$ denotes the sieve on $V$ consisting of all morphisms $h$ into $V$ such that $gh$ factors, up to isomorphism, through some morphism in $R$.

As in the 1-categorical case, one can then show that every coverage generates a unique Grothendieck coverage having the same 2-sheaves.

Truncated 2-toposes

Definition

Let $K$ be a Grothendieck 2-topos. We say that $K$ is $n$-truncated if it has a small eso-generator consisting of $(n-1)$-truncated objects. It is easy to see that if a coproduct of $(n-1)$-truncated objects is $(n-1)$-truncated (as is the case for all $n\ge 1$), then this is equivalent to saying that $K$ has enough $(n-1)$-truncated objects (i.e. every object admits an eso from an $(n-1)$-truncated one). In particular:

• $K$ is always 2-truncated.
• $K$ is (2,1)-truncated if it has enough groupoids.
• $K$ is 1-truncated if it has enough discretes.
• $K$ is (0,1)-truncated if the subterminal objects are eso-generating.
• $K$ is (-1)-truncated if the terminal object is an eso-generator.

$n$-sites and $n$-sheaves

By the 2-Giraud theorem, small eso-generating sets of objects correspond to small 2-sites of definition for $K$. Thus, if we define an $n$-site to be a 2-site which is an $n$-category (where $n\le 2$ as usual), we have:

Theorem

A Grothendieck 2-topos is $n$-truncated iff it is equivalent to the 2-category of 2-sheaves on some $n$-site.

Note that a 1-site is the same as the usual notion of site, and a $(0,1)$-site is sometimes called a posite. In particular, any frame is a (0,1)-site with its canonical coverage (the covering families are given by unions).

Particular cases include:

• $K$ is 1-truncated iff it is equivalent to the 2-category of 2-sheaves (stacks) on an ordinary small (1-)site, and therefore to the 2-category of stacks for the canonical coverage on some Grothendieck 1-topos.

• $K$ is (0,1)-truncated iff it is equivalent to the 2-category of stacks on a posite, and therefore also to the 2-category of stacks on some locale. We call such a $K$ localic.

• If $K$ is (-1)-truncated, then it is in particular localic, and its terminal object is a (strong) generator. It is not hard to see that this is equivalent to saying that the corresponding locale $X$ is a sublocale of the terminal locale $1$. Thus, just as (-1)-categories are subsets of $1$, (-1)-toposes are sublocales of $1$. If $\mathrm{Cat}$ has classical logic, this implies that either $X\cong 0$ or $X\cong 1$; and hence that either $K\simeq 1$ or $K\simeq \mathrm{Cat}$. However, constructively there may be many other sublocales of $1$.

• It would be nice if the only (-2)-truncated Grothendieck 2-topos were $\mathrm{Cat}$. However, I don’t see a way to make this happen except by fiat.

Grothendieck $n$-toposes

Now, if $C$ is an $n$-site, it is also reasonable to consider $n$-sheaves on $C$, by which we mean 2-sheaves taking values in $(n-1)$-categories. Thus, a 1-sheaf on a 1-site is precisely the usual notion of sheaf on a site. And a (0,1)-sheaf on a (0,1)-site is easily seen to be a lower set that is an “ideal” for the coverage.

We define a Grothendieck $n$-topos to be an $n$-category equivalent to the $n$-category of $n$-sheaves on an $n$-site. The case $n=1$ gives classical Grothendieck toposes; the case $n=(0,1)$ gives locales. Note the distinction between a Grothendieck $n$-topos and an $n$-truncated Grothendieck 2-topos. The relationship is that

1. The 2-category of 2-sheaves for the canonical coverage on a Grothendieck $n$-topos is an $n$-truncated Grothendieck 2-topos, and
2. Any $n$-truncated Grothendieck 2-topos arises in this way from the Grothendieck $n$-topos which is its full subcategory of $(n-1)$-truncated objects.

This relationship is completely analogous to the classical relationship between locales and localic toposes. In fact, if $\mathrm{Gr}n\mathrm{Top}$ denotes the $(n+1)$-category of Grothendieck $n$-toposes (that is, $n$-categories of $n$-sheaves on an $n$-site), we have inclusions

$$\begin{array}{ccccccc}& & & & & & \mathrm{Gr}(1,2)\mathrm{Top}\\ & & & & & \nearrow & & \searrow \\ \mathrm{Gr}(-1)\mathrm{Top}& \to & \mathrm{Gr}(0,1)\mathrm{Top}& \to & \mathrm{Gr}1\mathrm{Top}& & & & \mathrm{Gr}2\mathrm{Top}\\ & & & & & \searrow & & \nearrow \\ & & & & & & \mathrm{Gr}(2,1)\mathrm{Top}\end{array}$$\array{ &&&&&& Gr(1,2)Top\\ &&&&& \nearrow && \searrow\\ Gr (-1) Top &\to& Gr(0,1)Top &\to & Gr1Top &&&& Gr2Top\\ &&&&& \searrow && \nearrow\\ &&&&&& Gr(2,1)Top }

where the inclusion from $\mathrm{Gr}n\mathrm{Top}$ to $\mathrm{Gr}(n+1)\mathrm{Top}$ is given by taking the $(n+1)$-category of $(n+1)$-sheaves for the canonical coverage. (See 2-geometric morphism for the morphisms in these categories.)

2-geometric morphisms

If $K$ and $L$ are Grothendieck n-toposes, an $n$-geometric morphism $f:K\to L$ consists of an adjoint pair $f^{*}⊣f_{*}$, where $f_{*}:K\to L$ is the direct image and $f^{*}:L\to K$ is the inverse image, such that $f^{*}$ preserves finite limits (in the $n$-categorical sense).

When $n=1$ this is, of course, the usual definition. When $n=(0,1)$ this reduces to a continuous map between locales.

In general, we expect that Grothendieck $n$-toposes satisfy an $n$-categorical version of the adjoint functor theorem, so that any functor $f^{*}:L\to K$ that preserves finite limits and small colimits is the inverse image of some $n$-geometric morphism.

We define transformations and modifications between $n$-geometric morphisms to be transformations and modifications between their inverse image functors. We then have an $(n+1)$-category $\mathrm{Gr}n\mathrm{Top}$ of Grothendieck $n$-toposes and $n$-geometric morphisms.

Truncation in an exact 2-category

In a suitably exact 2-category, we can construct truncations as quotients of suitable congruences.

(-1)-truncation

This case is easy and just like for 1-categories.

Theorem

In any regular 2-category $K$ the inclusion $\mathrm{Sub}(1)\hookrightarrow K$ of the subterminal objects has a left adjoint called the support or (-1)-truncation.

Proof

Define the support $\mathrm{supp}(A)=A_{\le -1}$ of an object $A$ to be the image of the unique morphism $A\to 1$. That, is $A\to \mathrm{supp}(A)\to 1$ is an eso-ff factorization. Since $\mathrm{supp}(A)\to 1$ is ff, $\mathrm{supp}(A)$ is subterminal, and since esos are orthogonal to ffs, it is a reflection into $\mathrm{Sub}(1)$.

(0,1)-truncation

Perhaps surprisingly, the next easiest case is the posetal reflection.

Theorem

In any (1,2)-exact 2-category $K$ the inclusion $\mathrm{pos}(K)\hookrightarrow K$ of the posetal objects has a left adjoint called the (0,1)-truncation.

Proof

Given $A$, define $A_1$ to be the (ff) image of $A^2\to A\times A$. Since esos are stable under pullback, $A_1\rightrightarrows A$ is a homwise-discrete category, and it clearly has a functor from $\ker (A)$, so it is a (1,2)-congruence. Let $A\to P$ be its quotient. By the classification of congruences, $P$ is posetal. And if we have any $f:A\to Q$ where $Q$ is posetal, then we have an induced functor $\ker (A)\to \ker (f)$. But $Q$ is posetal, so $\ker (f)$ is a (1,2)-congruence, and thus $\ker (A)\to \ker (f)$ factors through a functor $A_1\to \ker (f)$. This then equips $f$ with an action by the (1,2)-congruence $A_1\rightrightarrows A$, so that it descends to a map $P\to Q$. It is easy to check that 2-cells also descend, so $P$ is a reflection of $A$ into $\mathrm{pos}(K)$.

This is actually a special case of the (eso+full,faithful) factorization system?, since an object $A$ is posetal iff $A\to 1$ is faithful. The proof is also an evident specialization of that.

0-truncation

The discrete reflection, on the other hand, requires some additional structure.

Theorem

In any 1-exact and countably-coherent 2-category $K$, the inclusion $\mathrm{disc}(K)\hookrightarrow K$ of the discrete objects has a left adjoint called the 0-truncation or discretization.

Proof

Given $A$, define $A_1$ to be the equivalence relation generated by the image of $A^2\to A\times A$; this can be constructed with countable unions in the usual way. Then $A_1\rightrightarrows A$ is a 1-congruence, and as in the posetal case we can show that its quotient is a discrete reflection of $A$.

There are other sufficient conditions on $K$ for the discretization to exist; see for instance classifying cosieve. We can also derive it if we have groupoid reflections, since the discretization is the groupoid reflection of the posetal reflection.

(1,0)-truncation

The groupoid reflection is the hardest and also requires infinitary structure. Note that the 2-pretopos $\mathrm{FinCat}$ does not admit groupoid reflections (the groupoid reflection of the “walking parallel pair of arrows” is $BZ$).

Theorem

In any (2,1)-exact and countably-extensive 2-category $K$, the inclusion $\mathrm{gpd}(K)\hookrightarrow K$ of the groupoidal objects has a left adjoint called the (1,0)-truncation.

The comprehensive factorization system

In Cat there is a factorization system $(E,M)$ where $E$ is the class of initial functors and $M$ is the class of discrete opfibrations; see

• Street, Walters, The comprehensive factorization of a functor. Bull. Amer. Math. Soc. 79, 1973.

We can construct an analogous factorization system in any 1-exact and countably-coherent 2-category.

Definition

A morphism $f:A\to B$ in a 2-category $K$ is initial if it is left orthogonal to discrete opfibrations. That is, whenever $g:C\to D$ is a discrete opfibration, the following square is a pullback in $\mathrm{Cat}$:

$$\begin{array}{ccc}K(B,C)& \to & K(B,D)\\ \downarrow & & \downarrow \\ K(A,C)& \to & K(A,D)\end{array}$$\array{ K(B,C) & \to & K(B,D)\\ \downarrow & & \downarrow\\ K(A,C) & \to & K(A,D)}

Theorem

Every morphism in a 1-exact countably-coherent 2-category (in particular, in an $n$-pretopos for $n\ge 1$) factors, up to isomorphism, as an initial morphism followed by a discrete opfibration.

Proof

By the 2-categorical analogue of a standard theorem about factorization systems in 1-categories, it suffices to show that

1. discrete opfibrations are closed under composition, and
2. for every $X$, the discrete opfibrational slice $\mathrm{DOpf}(X)$ is a full reflective subcategory of the slice 2-category $K/X$.

The first point is true in any 2-category. For the second, we factor the inclusion as

$$\mathrm{DOpf}(X)\to \mathrm{Opf}(X)\to K/X$$DOpf(X) \to Opf(X) \to K/X

and observe that both forgetful functors have left adjoints. The left adjoint to $\mathrm{DOpf}(X)\to \mathrm{Opf}(X)$ is discretization in the 1-exact and countably-coherent 2-category $\mathrm{Opf}(X)$. The left adjoint to $\mathrm{Opf}(X)\to K/X$ constructs the “free opfibration” on a functor $f:A\to X$, which is given by $A{\times }_X{X}^2$.

Corollary

In any 1-exact countably-coherent 2-category, (initial, discrete opfibration) is a (2-categorical) factorization system.

Corollary

In any 1-exact countably-coherent 2-category, each pullback functor $f^{*}:\mathrm{DOpf}(Y)\to \mathrm{DOpf}(X)$ has a left adjoint ${\mathrm{Lan}}_f$.

Proof

${\mathrm{Lan}}_f$ is given by composing with $f$, then factoring into an initial morphism followed by a discrete opfibration.

Examples

• In a 1-category, every morphism is a discrete opfibration, so the only initial morphisms are isomorphisms. The factorization system (isomorphisms,all morphisms) is well-known.

• In a (2,1)-category, the discrete opfibrations are precisely the faithful morphisms. Thus, in this case the comprehensive factorization system coincides with the (eso+full, faithful) factorization system.

Beck-Chevalley conditions

The appropriate Beck-Chevalley condition for the adjunctions ${\mathrm{Lan}}_f⊣f^{*}$ refers not to pullback squares, but to comma squares. The easiest proof of this fact uses the internal logic. We start with an internal characterization of initial morphisms, analogous to the classical characterization in $\mathrm{Cat}$ as the functors $f:A\to B$ for which each comma category $(f/b)$, for $b\in B$, is nonempty and connected.

For the rest of this page we make the standing assumption that $K$ is a 1-exact and countably-coherent 2-category.

Lemma

A morphism $f:A\to B$ in $K$ is initial iff the following are internally valid:

$$\begin{array}{c}b:B\mid \top ⊢(\exists a:A)(\exists \alpha :{\mathrm{hom}}_B(f(a),b))\\ b:B,a_1:A,a_2:A,{\alpha }_1:{\mathrm{hom}}_B(f(a_1),b),{\alpha }_2:{\mathrm{hom}}_B(f(a_2),b)\mid \top ⊢\underset{i\in \mathbb{N}}{\bigvee }{\phi }_i\end{array}$$\begin{gathered} b:B | \top \vdash (\exists a:A)(\exists \alpha:hom_B(f(a),b))\\ b:B, a_1:A, a_2:A, \alpha_1:hom_B(f(a_1),b), \alpha_2:hom_B(f(a_2),b) | \top \vdash \bigvee_{i\in \mathbb{N}} \varphi_i \end{gathered}

where for each $i$, ${\phi }_i$ expresses “there is a zigzag of length $i$ connecting ${\alpha }_1$ and ${\alpha }_2$ over $b$.”

Thus, for instance, we have

$$\begin{array}{rl}{\phi }_1\equiv & (\exists \gamma :{\mathrm{hom}}_A(a_1,a_2))({\alpha }_2\circ f(\gamma )={\alpha }_1)\\ {\phi }_2\equiv & (\exists c:A)(\exists \beta :{\mathrm{hom}}_B(f(c),b))(\exists {\gamma }_1:{\mathrm{hom}}_A(a_1,c))(\exists {\gamma }_2:{\mathrm{hom}}_A(a_2,c))({\alpha }_1=\beta \circ f({\gamma }_1)\wedge {\alpha }_2=\beta \circ f({\gamma }_2))\end{array}$$\begin{aligned} \varphi_1 \equiv& (\exists \gamma:hom_A(a_1,a_2)) (\alpha_2 \circ f(\gamma) = \alpha_1)\\ \varphi_2 \equiv& (\exists c:A)(\exists \beta:hom_B(f(c),b))(\exists \gamma_1:hom_A(a_1,c))(\exists \gamma_2:hom_A(a_2,c)) (\alpha_1 = \beta \circ f(\gamma_1) \wedge \alpha_2 = \beta \circ f(\gamma_2)) \end{aligned}

and so on.

Proof

$f:A\to B$ will be initial iff the discrete-opfibration part of its factorization is an equivalence. By construction, this factorization is the discrete reflection of $X=A{\times }_B{B}^2\to B$ in $\mathrm{Opf}(B)$, which is constructed as the quotient of the equivalence relation $X_1$ generated by $X^2$ (the power taken in $\mathrm{Opf}(B)$). Therefore, this discrete reflection will be the terminal object $1_B$ iff

1. $X\to B$ is eso and
2. the kernel of $X\to B$ in $\mathrm{Opf}(B)$ is $X_1$.

It is fairly evident that $X\to B$ is eso iff the first displayed sequent holds in $K$. For the second, note that the kernel of $X\to B$ in $\mathrm{Opf}(B)$ (or equivalently, in $K/B$) is just the pullback $X{\times }_{B}X$, since $B$ is discrete as an object of $K/B$. By definition of $X$, this pullback can be computed as the lax limit

and therefore it is precisely the context of the second displayed sequent. Since $X_1$ is the equivalence relation generated by $X^2$, it is necessarily contained in this kernel, so it suffices to show the converse implication. But $X_1$ is defined as the symmetric transitive closure of the image of $X^2$, which makes it essentially a countable union of “zigzags” from $X^2$, and this translates directly into the conclusion of the second sequent.

Lemma

Initial morphisms in $K$ are stable under transfer across comma squares, in the sense that if

is a comma square with $f$ initial, then $q$ is also initial.

Proof

Given the characterization of initial morphisms in Lemma 13, we can simply observe that the usual proof of this fact in $\mathrm{Cat}$ takes place entirely in countably-coherent logic.

Theorem

The adjunctions ${\mathrm{Lan}}_f⊣f^{*}$ for discrete opfibrations in $K$ satisfy the Beck-Chevalley condition for comma squares. That is, if

is a comma square, then the canonical transformation ${\mathrm{Lan}}_q{p}^{*}\to g^{*}{\mathrm{Lan}}_f$ between functors $\mathrm{DOpf}(A)\to \mathrm{DOpf}(B)$ is an equivalence.

Note that unlike the case for a pullback square, there is no possible “handedness” ambiguity in saying that a comma square satisfies the Beck-Chevalley condition; there is no transformation ${\mathrm{Lan}}_p{q}^{*}\to f^{*}{\mathrm{Lan}}_g$ at all.

The existence of the transformation in the correct direction also depends on the fact that opfibrational slices are functorial at the level of 2-cells. In particular, for a comma square there is no transformation ${\Sigma }_q{p}^{*}\to g^{*}{\Sigma }_f$ between functors $K/A\to K/B$.

Proof

Given a discrete opfibration $X\to A$, let $X\to {\mathrm{Lan}}_{f}X\to C$ be the (initial,discrete-opfibration) factorization of the composite $X\to A\stackrel{f}{\to }C$. Now by properties of comma squares and pullbacks, the pasting composite

is also a comma square, and thus so is

where the upper 2-cell is opcartesian for the opfibration ${\mathrm{Lan}}_{f}X\to C$, and the map $p^{*}X\to g^{*}{\mathrm{Lan}}_{f}X$ is obtained from the universal property of the pullback square on the bottom. Again, it follows from general properties of pullbacks and comma squares that the top square in this latter diagram is also a comma square. Thus, by Lemma 14, its left-hand morphism is initial. But then the left-hand composite $p^{*}X\to g^{*}{\mathrm{Lan}}_{f}X\to B$ is an (initial, discrete-opfibration) factorization of $p^{*}X\to (f/g)\to B$, and hence it exhibits the desired equivalence ${\mathrm{Lan}}_q{p}^{*}X\simeq g^{*}{\mathrm{Lan}}_{f}X$.

Passing to 2-cell duals, we obtain:

Corollary

For a comma square as above, the canonical transformation ${\mathrm{Lan}}_p{q}^{*}\to f^{*}{\mathrm{Lan}}_g$ between functors $\mathrm{DFib}(B)\to \mathrm{DFib}(A)$ is an equivalence.

Full morphisms and (eso+full, faithful) factorization

In Cat and Gpd, in addition to the (eso, ff) factorization system that is enshrined in the notion of regular 2-category, there is also an (eso+full, faithful) factorization system. In Gpd, the (eso+full, faithful) factorization is the same as the comprehensive factorization, but in Cat they are different.

Mathieu Dupont has pointed out that given sufficient exactness, (eso+full, faithful) factorizations can be constructed from (eso,ff) factorizations. Here we give the argument.

eso+full and full morphisms

Recall that a morphism $m:C\to D$ is said to be faithful if $K(X,C)\to K(X,D)$ is faithful for any $X$.

Definition

A morphism $e:A\to B$ in a 2-category $K$ is eso+full if for any faithful $m:C\to D$, the following square is a pullback:

$$\begin{array}{ccc}K(B,C)& \to & K(B,D)\\ \downarrow & & \downarrow \\ K(A,C)& \to & K(A,D)\end{array}$$\array{K(B,C) & \to & K(B,D)\\ \downarrow & & \downarrow\\ K(A,C) & \to & K(A,D)}

Definition

A morphism $f$ is said to be full if we have $f\cong me$ where $m$ is ff and $e$ is eso+full.

Luckily, the terminology is consistent:

Lemma

In any 2-category,

1. $f$ is eso+full if and only if it is both eso and full.
2. $f$ is ff if and only if it is both faithful and full.

Proof

Since ffs are faithful, any eso+full is eso, and any eso+full clearly factors as an eso+full (itself) followed by an ff (the identity). Conversely, if $f$ is eso and $f\cong me$ where $e$ is eso+full and $m$ is ff, then $m$ is an equivalence, and hence $f$, like $e$, is eso+full.

Now, ffs are clearly faithful, and any ff clearly factors as an eso+full (the identity) followed by an ff (itself). Conversely, if $f$ is faithful and we have $f\cong me$ where $e$ is eso+full and $m$ is ff, then $e$ is also faithful, and hence an equivalence; thus $f$, like $m$, is ff.

Lemma

Any eso+full morphism is co-ff.

Proof

Let $f:A\to B$ be eso+full; we want to show that $K(B,C)\to K(A,C)$ is ff. It is faithful since $f$ is eso, so suppose that $g,h:B\rightrightarrows C$ and that $\alpha :gf\to hf$; we want to show $\alpha =\beta f$ for some $\beta :g\to h$. Let $p:E\to B$ with $\gamma :gp\to hp$ be the inserter of $g,h$. Then we have a $k:A\to E$ such that $pk\cong f$ and (modulo this isomorphism) $\gamma k=\alpha$. But since $p$, being an inserter, is faithful, and $f$ is eso+full, we have $q:B\to E$ with $k\cong qf$ and therefore $\alpha =\gamma k=\gamma qf$; thus $\beta =\gamma q$ is our desired 2-cell.

Factorizations

Lemma

If $A_1\rightrightarrows A$ is a 2-congruence such that $A^2\to A_1$ is eso, then its quotient $f:A\to B$ (if it has one) is eso+full.

Proof

Suppose that $m:C\to D$ is faithful and that $mg\cong hf$; we want to show there is a $k:B\to C$ with $g\cong kf$ and $h\cong mk$ (the rest follows by standard arguments). Since $mg$ comes with an action by $A_1\rightrightarrows A$, it suffices to lift this action to $g$ itself, and since $m$ is faithful it suffices to lift the 2-cell defining the action. This follows by the existence of a diagonal lift in the following rectangle:

$$\begin{array}{ccccc}{A}^2& & \to & & C^2\\ \downarrow & & & & \downarrow \\ A_1& \to & (f/f)& \to & (m/m)\end{array}$$\array{A^{\mathbf{2}} && \to && C^{\mathbf{2}} \\ \downarrow && && \downarrow\\ A_1 & \to & (f/f) & \to & (m/m)}

which exists since $A^2\to A_1$ is eso (by assumption) and $C^2\to (m/m)$ is ff (since $m$ is faithful).

Lemma

In a regular 2-category, if $f:A\to B$ is a map such that $A^2\to (f/f)$ is eso, then $f$ is full.

Proof

The (eso,ff) factorization of $f$ is constructed by taking the quotient of $\ker (f)$. But by assumption, this kernel has the property of Lemma 17, so the eso part of the (eso,ff) factorization of $f$ is eso+full. Hence $f$ is full, by definition.

For comparison, recall that

• $A^2\to (f/f)$ is always faithful,
• $A^2\to (f/f)$ is full (equivalently, ff) iff $f$ is faithful, and
• $A^2\to (f/f)$ is an equivalence iff $f$ is ff.

I do not know whether the converse of Lemma 18 is true in general, but it is at least true in an exact 2-category.

Theorem

Let $K$ be an $n$-exact $n$-category, where $n$ is 2, (2,1), (1,2), or 1. Then:

1. Every morphism $f$ factors as $f\cong me$ where $e$ is eso+full and $m$ is faithful. Thus, (eso+full, faithful) is a factorization system on $K$.
2. A morphism $f:A\to B$ is full iff $A^2\to (f/f)$ is eso.
3. Therefore, $f$ is eso+full iff it is the quotient of a 2-congruence $A_1\rightrightarrows A$ such that $A^2\to A_1$ is eso.

Of course, the cases $n=1$ and $(1,2)$ are fairly trivial, since in those cases every morphism in an $n$-category is faithful and thus the only eso+full morphisms are the equivalences. However, we include them for completeness.

Proof

For the first statement, let $f:A\to B$ be any morphism, and factor $A^2\to (f/f)$ as an eso followed by a ff to get $A^2\to A_1\to (f/f)$. Then $A_1$ inherits the structure of a 2-congruence, which is an $n$-congruence since $(f/f)$ is. Since $K$ is $n$-exact, this $n$-congruence has a quotient $e:A\to Q$, which is eso+full by Lemma 17, and clearly $f$ factors through $e$ as $f\cong me$. Finally, since $(e/e)=A_1\to (f/f)$ is ff by definition, Street's Lemma implies that $m$ is faithful.

The “if” direction of the second statement is Lemma 18. Conversely, if $f\cong me$ where $m$ is ff and $e$ is eso+full, then $e$ must be obtained, up to equivalence, as the quotient of the $n$-congruence $A_1\rightrightarrows A$ constructed above, for which $A^2\to A_1$ is eso. But since $m$ is ff, we have $(f/f)\simeq (e/e)=A_1$, so $A^2\to (f/f)$ is eso as desired.

One direction of the third statement is Lemma 17. For the other, if $f$ is eso+full, then by the second statement $A^2\to (f/f)$ is eso, and because $f$ is eso it is the quotient of its kernel, namely $(f/f)\rightrightarrows A$.

Inspecting the proof shows that we don’t need the full strength of exactness, either; all we need is that any sub-congruence of a kernel has a quotient. This is a property in between regularity and exactness. For instance, it is satisfied by $\mathrm{FinCat}$, which is not exact.

Corollary

In a (2,1)-exact (2,1)-category, eso+full morphisms are stable under pullback, and therefore so are full ones.

Proof

If $p:A\to B$ is eso+full, then it is the quotient of its kernel, which in a (2,1)-category is $A{\times }_{B}A\to A$. And since $p$ is eso+full, by Theorem 22, $A\to A{\times }_{B}A$ is eso. If

$$\begin{array}{ccc}D& \to & A\\ {}^q\downarrow & & {\downarrow }^p\\ C& \stackrel{f}{\to }& B\end{array}$$\array{D & \to & A \\ ^q\downarrow && \downarrow ^p\\ C & \overset{f}{\to} & B}

is a pullback square, then the kernel $D{\times }_{C}D$ is also the pullback of $A{\times }_{B}A$ along $f$. Thus, by properties of pullback squares, $D\to D{\times }_{C}D$ is a pullback of $A\to A{\times }_{B}A$, and hence also eso. But $q$, being eso (as a pullback of $p$), is also the quotient of its kernel, so by Lemma 17 $q$ is eso+full. The second statement follows since ffs are certainly stable under pullback.

Corollary

Let $K$ be an $n$-exact $n$-category. Then:

1. Full morphisms are stable under composition.
2. A morphism is full iff it is (isomorphic to) a composite of eso+full and ff morphisms.
3. If $gf$ is full and $f$ is eso, then $g$ is full.

Proof

Given $f:A\to B$ and $g:B\to C$, we have two pullback squares

$$\begin{array}{ccccc}(f/f)& \to & (gf/gf)& \to & A\times A\\ \downarrow & & \downarrow & & \downarrow \\ B^2& \to & (g/g)& \to & B\times B.\end{array}$$\array{ (f/f) & \to & (g f / g f) & \to & A\times A\\ \downarrow &&\downarrow && \downarrow\\ B ^{\mathbf{2}} & \to & (g/g) & \to & B\times B.}

Thus, if $f$ and $g$ are full, so that $A^2\to (f/f)$ and $B^2\to (g/g)$ are eso, then $(f/f)\to (gf/gf)$ is also eso, hence so is $A^2\to (gf/gf)$; thus $gf$ is full. This proves the first statement, from which the second follows. For the third, if $gf$ is full and $f$ is eso, then $A^2\to (gf/gf)$ is eso, and so is $(gf/gf)\to (g/g)$ since it is a pullback of $f\times f$. Thus the composite $A^2\to (g/g)$ is eso, and since it factors through $B^2$, it follows that $B^2\to (g/g)$ is also eso; hence $g$ is full.

The Cauchy factorization system

Definitions

A morphism $m:A\to B$ in a 2-category $K$ is called ff and retract-closed or rff if $K(X,A)\to K(X,B)$ is fully faithful and closed under retracts for all $X$. Explicitly this means that (in addition to being ff) if $b:X\to B$ is a retract of $ma$ for some $a:X\to A$, then $b\cong ma\prime$ for some $a\prime \in A$.

A morphism $e:A\to B$ is called Cauchy surjective or cso if it is left orthogonal to all rffs; that is, if

$$\begin{array}{ccc}K(B,C)& \to & K(B,D)\\ \downarrow & & \downarrow \\ K(A,C)& \to & K(A,D)\end{array}$$\array{K(B,C) & \to & K(B,D)\\ \downarrow & & \downarrow \\ K(A,C) & \to & K(A,D)}

is a pullback whenever $m:C\to D$ is rff.

Remarks

• Since rffs are stable under pullback, $e$ is cso if and only if whenever it factors through an rff $m:C\to B$, then $m$ is an equivalence.

• Every eso is cso, since every rff is ff. Conversely, in a (2,1)-category, every ff is rff, and thus every cso is eso.

• In $\mathrm{Cat}$, the Cauchy surjective functors are those for which every object of $B$ is a retract of an object of $A$.

• Every equifier or inverter is rff. Therefore, every Cauchy surjective morphism is cofaithful and coconservative. In “Modulated bicategories” by Carboni, Johnson, Street, and Verity it is shown that conversely, every coconservative functor in $\mathrm{Cat}$ is Cauchy surjective.

Factorization System

In $\mathrm{Cat}$, (cso,rff) is a factorization system. We now show that the same is true in any regular 2-category.

Given $f:A\to B$, let $R_f$ be its retractor. This is a 2-categorical finite limit which comes with projections $p:R_f\to A$ and $q:R_f\to B$ and 2-cells $\rho :fp\to q$ and $\sigma :q\to fp$ such that $\rho \sigma =1_q$, and which is universal with these properties.

Lemma

In any 2-category, if $q:R_f\to B$ is eso, then $f$ is Cauchy surjective.

Proof

Suppose that $q$ is eso and let $A\stackrel{g}{\to }C\stackrel{m}{\to }B$ be such that $f\cong mg$ and $m$ is rff; we want to show $m$ is an equivalence. But since $m$ is rff and $q$ is a retract of $fp\cong mgp$, it follows that $q$ factors through $m$; whence $m$ is an equivalence since $q$ is eso.

Now suppose that $K$ is regular, and for any $f:A\to B$, let $R_f\stackrel{j}{\to }{C}_f\stackrel{m}{\to }B$ be an (eso,ff) factorization of $q$. Since $f$ is a retract of $f{1}_A$, there is a canonical $s:A\to R_f$ with $ps\cong 1_A$ and $f\cong qs\cong mjs$.

Lemma

In a regular 2-category, if $f:A\to B$ is ff and $C_f\subset A$ (hence $C_f\simeq A$), then $f$ is rff.

Proof

Suppose $f$ is ff and $C_f\simeq A$, and let $b:X\to B$ and $a:X\to A$ be such that $b$ is a retract of $a$. Then $b\cong qc$ and $a\cong pc$ for some $c:X\to R_f$. Then we have $jc:X\to C_f$ with $mjc\cong b$. But since $C_f\simeq A$ in $\mathrm{Sub}(B)$, we have a $y:X\to A$ with $fy\cong b$ as well; hence $f$ is rff.

Theorem

In a regular 2-category $K$,

1. Every morphism $f$ factors as a Cauchy surjective morphism followed by an rff.
2. Therefore, (cso,rff) is a factorization system on $K$.
3. A morphism $f$ is cso if and only if $q:R_f\to B$ is eso.
4. Likewise, $f$ is rff if and only if it is ff and $C_f\simeq A$.

Proof

Given any $f:A\to B$, let $j$, $m$, and $s$ be as above, and define $e=js:A\to C_f$. Then $me\cong mjs\cong qs\cong f$. Is easy to check that $R_f\cong R_e$; thus $R_e\to C_f$ is eso, so by Lemma 19 $e$ is Cauchy surjective.

Now let $R_m$ be the retractor of $m$, with $p\prime :R_m\to C_f$, $q\prime :R_m\to B$, and corresponding factorization $R_m\stackrel{j\prime }{\to }{C}_m\stackrel{m\prime }{\to }B$. Let

$$\begin{array}{ccc}P& \stackrel{u}{\to }& R_f\\ {}^v\downarrow & & {\downarrow }^j\\ R_m& \underset{p\prime }{\to }& C_f\end{array}$$\array{P & \overset{u}{\to}& R_f\\ ^v \downarrow && \downarrow ^j\\ R_m & \underset{p'}{\to} & C_f}

be a pullback. Then $v$, like $j$, is eso, and thus so is $j\prime v:P\to C_m$. Now $m\prime j\prime v\cong q\prime v$ is a retract of $mp\prime v\cong mju\cong qu$, and $q$ is a retract of $fp$, so $qu$ is a retract of $fpu$. Therefore, $m\prime j\prime v:P\to B$ is also a retract of $fpu$, so there is a morphism $w:P\to R_f$ with $mjw\cong qw\cong m\prime j\prime v$ (and $pw\cong pu$). Now in the square

$$\begin{array}{ccc}P& \stackrel{jw}{\to }& C_f\\ {}^{j\prime v}\downarrow & & {\downarrow }^m\\ C_m& \underset{m\prime }{\to }& B,\end{array}$$\array{P & \overset{j w}{\to} & C_f\\ ^{j' v}\downarrow && \downarrow ^m\\ C_m & \underset{m'}{\to} & B,}

$m$ is ff and $j\prime v$ is eso, so we have $C_m\subset C_f$ in $\mathrm{Sub}(B)$; thus by Lemma 20 $m$ is rff.

Therefore, with $f\cong me$ we have factored $f$ as a cso followed by an rff; this shows the first two statements. Moreover, $e$ satisfies the condition of Lemma 19, so if $f$ is cso and hence equivalent to $e$, so does it. Likewise, $m$ satisfies the condition of Lemma 20, so if $f$ is rff and hence equivalent to $m$, so does it.

Internal logic

From the characterization of csos and rffs in Theorem 23, we can conclude that csos and rffs have the expected descriptions in the internal logic.

Corollary

In a regular 2-category, a morphism $f:A\to B$ is Cauchy surjective if and only if the following sequent is valid in the internal logic:

$$y:B\mid \top ⊢(\exists x:A)(\exists \rho :{\mathrm{hom}}_B(f(x),y))(\exists \sigma :{\mathrm{hom}}_B(y,f(x)))(\rho \sigma =1_y).$$y:B | \top \vdash (\exists x:A)(\exists \rho:hom_B(f(x),y))(\exists \sigma:hom_B(y,f(x)))(\rho \sigma = 1_y).

Proof

The context $y:B,x:A,\rho :{\mathrm{hom}}_B(f(x),y),\sigma :{\mathrm{hom}}_B(y,f(x))\mid \rho \sigma =1_y$ is easily seen to be precisely $R_f$.

Corollary

In a regular 2-category, a morphism $f:A\to B$ is rff if and only if it is ff and the following sequent is valid in the internal logic:

$$x:A,y:B,\rho :{\mathrm{hom}}_B(f(x),y),\sigma :{\mathrm{hom}}_B(y,f(x))\mid \rho \sigma =1_y⊢(\exists x\prime :A)(f(x\prime )\cong y)$$x:A,y:B,\rho:hom_B(f(x),y), \sigma:hom_B(y,f(x)) | \rho \sigma = 1_y \vdash (\exists x':A)(f(x')\cong y)

Proof

The validity of this sequent says that the pullback of $f:A\to B$ along $q:R_f\to B$ is eso. But since both $f$ and $q$ factor through the ff $m:C_f\to B$, this pullback is equivalent to the pullback of $e:A\to C_f$ along $j:R_f\to C_f$. Since $j$ is eso, this pullback being eso is equivalent to $e:A\to C_f$ being eso. And since $f$ is ff, so is $e$; thus this is equivalent to $e$ being an equivalence.

Colimits in 2-pretopoi

An $n$-pretopos has coproducts and quotients of $n$-congruences, which are important classes of colimits. From these we can construct some other colimits, such as the following.

Theorem

A 2-pretopos admits copowers with any finite category.

Proof

If $C$ is a finite category and $A\in K$ is an object, we build a finite 2-polycongruence with one copy of $A$ indexed by each object $c\in C$, and with the hom-object from $A_c$ to $A_d$ being ${\sum }_{C(c,d)}{A}^2$. It is easy to check that a quotient of this congruence is a copower $A•C$.

However, an $n$-pretopos can fail to admit all finite colimits, for essentially the same reason as when $n=1$: some ostensibly “finite” colimits secretly involve infinitary processes. In a 1-category, this manifests in the construction of arbitrary coequalizers and pushouts, where we must first generate an equivalence relation by an infinitary process and then take its quotient. Likewise, a 2-pretopos can fail to admit pushouts, coinserters, coinverters, and coequifiers.

For 2-categories it is even easier to find counterexamples. The 1-pretopos $\mathrm{FinSet}$ does in fact have all finite colimits, but the 2-pretopos $\mathrm{FinCat}$ of finite categories does not have coinserters or coinverters. (It does have coequifiers, for the same reason that $\mathrm{FinSet}$ has coequalizers). The category $\mathrm{FPCat}$ of finitely presented categories, on the other hand, does have finite colimits, but fails to have finite limits.

You can also generate the equivalence relation using a higher-order process. Thus a topos (where higher-order processes occur) has all coequalisers, even if it's not a $W$-pretopos (where countably infinitary processes occur).

Incidentally, this is the example that first made me agree that predicativity was a reasonable constructive restriction. I just asked myself which way of generating an equivalence relation seemed more ‘constructive’.

—Toby

Indeed so. I noted at classifying cosieve that you can do the same thing in a 2-category if you have only a poset of truth values rather than a set. All this work on 2-toposes is actually making me more sympathetic to predicativism as well, because in the 2-dimensional case there isn’t really a “higher-order” version you can recourse to; you have to do things the “more constructive” way. Put differently, why is it okay to have a set (or poset) of all truth values, but not a category of all sets?

(Mathieu Dupont and I have been speculating about whether there could actually be a category of all sets; i.e. whether there could be a 2-pretopos having (exponentials, duality, and) a classifying discrete opfibration that classifies all discrete opfibrations. This would have marvelous consequences like that Set has all (not just small) limits and colimits, and so the adjoint functor theorem can be just true without any messing around with generators. But it is inconsistent with there being enough groupoids, or with Set being a topos, and hence also inconsistent with classical logic. I don’t really have very high hopes that it is consistent at all. Having a (1,2)-category of all posets appears to be inconsistent with just exponentials and duality.)

BTW, I assume that by ”$\Pi$-pretopos” you meant ”$\Pi$-pretopos with a NNO?” In my limited experience ”$\Pi$-pretopos” means “locally cartesian closed pretopos” which certainly includes all toposes.

-Mike

Sorry, I removed the wrong letter from ’$\Pi$-$W$-pretopos’. I meant a $W$-pretopos, that is a pretopos in which every polynomial functor has pullback-stable initial algebras in every slice category (which may follow from simply a pullback-stable NNO, I forget).

In my experience, when you can't find an inconsistency but you're sure that one exists, then the Burali-Forti paradox always works. There may be a simpler one, but Burali-Forti is the surest.

—Toby

I think that Burali-Forti works in this case to get a contradiction from having enough groupoids. But I can’t make it do anything else, because without cores, all I can construct is a poset of ordinals, which isn’t itself an ordinal because an ordinal is a set equipped with a certain sort of relation.

Why are you changing my $\Pi$s to characters that I can’t type?

-Mike

Sorry, I started to fix the ‘Π’s (and ‘$\Pi$’s), then realised that I was fixing some inappropriately and so changed them back (but apparently not always to what they had been before). And you can type that character, as Π. Actually, since you're using Ubuntu like me, you can install SCIM and use that to type it directly (the TeX input method is pretty neat). That said, ‘$\Pi$’ (also ‘$W$’), in math mode, is probably more appropriate, as it refers to closure under a type operation with that name.

I'll try to think about it and see if I can make a paradox work. I don't quite understand how you construct these posets that don't have underlying sets. Although it reminds of me of Paul Taylor's Abstract Stone Duality, where there is a topological space of truth values (in fact one free on a poset) but no underlying set of such.

—Toby

I can type Π but when I view the source that you’ve typed, I don’t see Π but rather an actual Pi-character.

-Mike

It produces the same output in the displayed XHTML. If you want to get Π in your Markdown source, either cut and paste from the display of Π, or install SCIM (or something along those lines) like I did. —Toby

Also, see the new page category of all sets regarding posets and categories that don’t have underlying sets.

-Mike

Will do. —Toby

I don’t want to get a Pi-character in my Markdown source; my point was rather that I wished you wouldn’t put it in yours! I thought the whole point of things like HTML entities like Π and TeX code like $\Pi$ was so that we could produce nice-looking math just by inputting ordinary ASCII text that can be read and edited without installing any fancy fonts or software.

-Mike

OK, fair enough, it's your web, so all special characters will be implemented as XHTML or SGML character entities (unless available through Instiki, of course). —Toby

However, once we have some infinitary structure, this problem goes away.

Theorem

A countably-extensive $n$-pretopos has all countable colimits.

1-pretoposes are balanced

It is well-known that in a 1-pretopos,

1. every monic is regular, and as a consequence
2. a 1-pretopos is balanced (every monic epic is an isomorphism), and
3. every epic is regular.

2-pretoposes are not balanced

For a similar statement in an $n$-pretopos for $n>1$, the natural first guess is to replace “monic” by “ff” and “regular epic” by “eso.” However, there are (at least) two reasonable replacements for “epic” and “regular monic:”

1. We could replace “epic” by “cofaithful” and “regular monic” by “equifier,” or
2. we could replace “epic” by “coconservative” (aka “liberal”) and “regular monic” by “inverter.”

Since esos in Cat are cofaithful and liberal but not co-ff, it wouldn’t work to replace “epic” by “co-ff.” Unfortunately, both ideas fail in Cat, where equifiers and inverters are not just ff but are closed under retracts. Likewise, the map from a category to its Cauchy completion is full, faithful, cofaithful, and liberal, but generally not an equivalence.

There are two ways to deal with this problem. One is to restrict to smaller values of $n$, for which there are no nontrivial retracts. The other is to go back and change “ff” to “ff and closed under retracts” and change “eso” to “surjective up to retracts.”

(2,1)-pretoposes are balanced

Theorem

In a (2,1)-exact positive coherent 2-category, every ff with groupoidal codomain is an equifier (in fact, an identifier of an involution).

Recall that an identifier of a 2-cell $\alpha :f\to f:A\to B$ in a 2-category is the equifier of $\alpha$ and $1_f$. By an involution we mean an (invertible) 2-cell that is its own inverse.

Proof

Let $m:A\to B$ be ff with $B$ groupoidal, and consider first the (2,1)-congruence given by $B+B\rightrightarrows B$, where one copy of $B$ gives the identities, and the composition treats the other copy of $B$ as an involution. Its quotient is the copower of $B$ by the “walking involution.”

Now consider the following equivalence relation on $B+B$ in $\mathrm{disc}(K/B\times B)$. We have

$$(B+B){\times }_{B\times B}(B+B)\simeq (B{\times }_{B\times B}B)+(B{\times }_{B\times B}B)+(B{\times }_{B\times B}B)+(B{\times }_{B\times B}B)$$(B+B)\times_{B\times B}(B+B) \simeq (B\times_{B\times B} B)+(B\times_{B\times B} B)+(B\times_{B\times B} B)+(B\times_{B\times B} B)

and we define the relation to be given by

$$\begin{array}{c}B+A+A+B\\ \downarrow \\ (B{\times }_{B\times B}B)+(B{\times }_{B\times B}B)+(B{\times }_{B\times B}B)+(B{\times }_{B\times B}B).\end{array}$$\array{B+A+A+B \\ \downarrow\\ (B\times_{B\times B} B)+(B\times_{B\times B} B)+(B\times_{B\times B} B)+(B\times_{B\times B} B).}

Since $\mathrm{disc}(K/B\times B)\simeq \mathrm{disc}({\mathrm{Fib}}_K(B\times B))$ is a 1-pretopos, this relation has a quotient, say $[f,g]:B+B\to C$. It is easy to verify that $a,b:C\rightrightarrows B$ is then a (2,1)-congruence on $B$ with $af=ag=bf=bg=1_B$. (This depends on $B$ being groupoidal; otherwise it would be a homwise-discrete category but not necessarily a congruence.) Let $q:B\to D$ be the quotient in $K$ of this (2,1)-congruence. Then we have a 2-fork $\varphi :qa\to qb$ such that $\varphi f=1_q$ and $\varphi g$ is an involution of $q$.

We claim that $m$ is an identifier of $\varphi g$. By construction of $C$, we have $\varphi gm=1_{qm}$, so since $m$ is ff, it suffices to show that for any $x:X\to B$ with $\varphi gx=1_{qx}$, $x$ factors through $m$. But since $C$ with $\varphi$ is the kernel of $q$, the assumption $\varphi gx=1_{qx}=\varphi fx$ implies that in fact $fx=gx$. If we write $i,j:B\rightrightarrows B+B$ for the two inclusions, this means that $ix:X\to B+B$ and $jx:X\to B+B$ become equal in $C$, and therefore factor through the kernel pair of $[f,g]$, namely $B+A+A+B$. But this is evidently tantamount to saying that $x$ factors through $A$.

Corollary

In a (2,1)-pretopos,

1. every ff is an equifier,
2. every cofaithful ff is an equivalence, and
3. every cofaithful morphism is eso.

Proof

Theorem 26 shows the first statement. Then any ff $f:A\to B$ is an equifier of $\alpha ,\beta :g\rightrightarrows h:B\rightrightarrows C$, so in particular $\alpha f=\beta f$; but if $f$ is also cofaithful, this implies $\alpha =\beta$, and thus their equifier $f$ is an equivalence. Finally, if $f$ is just cofaithful, we factor it as $f=me$ where $m$ is ff and $e$ is eso; but then $m$ is also cofaithful, hence an equivalence, and so $f$, like $e$, is eso.

(1,2)-pretoposes are balanced

Theorem

In a (1,2)-exact positive coherent 2-category, every ff with posetal codomain is an inverter.

Proof

Let $m:A\to B$ be ff, and consider the 2-congruence on $B+B$ defined as follows. We have

$$(B_0+B_1)\times (B_0+B_1)=(B_0\times B_0)+(B_0\times B_1)+(B_1\times B_0)+(B_1\times B_1),$$(B_0+B_1)\times (B_0+B_1) = (B_0\times B_0)+(B_0\times B_1)+(B_1\times B_0)+(B_1\times B_1),

(adding subscripts to distinguish the two copies of $B$) and the congruence is given by

$$\begin{array}{ccccccc}{B}^2& +& B^2& +& Y& +& B^2\\ & & & \downarrow \\ (B_0\times B_0)& +& (B_0\times B_1)& +& (B_1\times B_0)& +& (B_1\times B_1).\end{array}$$\array{ B ^{\mathbf{2}} &+& B ^{\mathbf{2}} &+& Y &+& B ^{\mathbf{2}}\\ &&& \downarrow\\ (B_0\times B_0) &+& (B_0\times B_1) &+& (B_1\times B_0) &+& (B_1\times B_1).}

Here $Y\hookrightarrow B^2$ is defined to be the ff image of the “composition” morphism $(1_B/m/1_B)\to B^2$; in other words it is “the object of arrows in $B$ which factor through some element of $A$.” The composition is easy to define making this into a 2-congruence, and if $B$ is posetal, then it is a (1,2)-congruence.

Let $[p,q]:B+B\to C$ be the quotient of this congruence. Analogously to the proof of Theorem 26, the fork defining this quotient gives a 2-cell $\varphi :p\to q$ such that $\varphi m$ is an isomorphism. Thus, to show that $m$ is the inverter of $\varphi$, it suffices to show that for any $x:X\to B$ with $\varphi x$ invertible, $x$ factors through $m$. Now $\varphi x$ is induced by the fork defining $C$ together with the composite $X\to B\to B^2$. If $\varphi x$ is invertible, then its inverse is given by some map $y:X\to Y$, which must lie over the diagonal $X\to B\to B\times B$.

Now, pulling back the eso $(1/m/1)\to Y$ along $y$ we obtain an eso $r:Z\to X$ with a morphism $s:Z\to A$ such that the identity 2-cell of $xr$ is the composite of 2-cells $xr\to ms\to xr$; in other words, $xr$ is a retract of $ms$. But since $B$ is posetal, this means $xr\cong ms$, and then the fact that $r$ is eso implies that $x$ factors through $m$, as desired.

Corollary

In a (1,2)-pretopos,

1. every ff is an inverter,
2. every liberal ff is an equivalence, and
3. every liberal morphism is eso.

Proof

Just like Corollary 14 but using Theorem 27 instead.

2-pretoposes are Cauchy balanced

Now, in any regular 2-category, in addition to the (eso,ff) factorization system we also have a Cauchy factorization system consisting of the cso (Cauchy surjective) and rff (ff and retract-closed) morphisms. Moreover, every cso is cofaithful and liberal. In “Modulated bicategories” by Carboni, Johnson, Street, and Verity (CJSV), it is shown that the liberal functors in Cat are precisely the Cauchy surjective ones; we now show that the same is true in any 2-pretopos.

Corollary

In a 2-pretopos,

1. every rff is an inverter,
2. every liberal rff is an equivalence, and
3. every liberal morphism is Cauchy surjective.

In particular, every liberal morphism is cofaithful.

Proof

The first statement is proven exactly like Theorem 27, except that at the last step we use the assumption that $m$ is retract-closed rather than the assumption that $B$ is posetal. The other statements follow as before, recalling that Cauchy surjective morphisms are cofaithful.

In (CJSV) a 2-category is defined to be co-conservational (liberational?) if

• it has finite colimits,
• it has (liberal, strong conservative) factorizations,
• strong conservative morphisms are preserved by copowers with $2$, and
• strong conservative morphisms are stable under pushout,

and faithfully co-conservational if moreover

• every liberal morphism is cofaithful.

Here a strong conservative morphism is one that is right orthogonal to all liberals. Theorem 16 shows that in a 2-pretopos, strong conservatives coincide with rffs, since liberals coincide with csos; thus any 2-pretopos satisfies the second condition to be co-conservational. It need not have finite colimits, but this can be remedied with some infinitary structure. The construction of copowers in a 2-pretopos can be used to show that rffs are preserved by copowers with $2$. And we have also seen that since every liberal is cso, it is cofaithful.

However, even $\mathrm{Cat}$ fails the final condition, as shown in (CJSV, Prop. 3.4). This can be remedied by passing to the 2-category ${\mathrm{Cat}}_{\mathrm{cc}}$ of Cauchy-complete categories. I do not yet know whether a similar construction is possible in any 2-pretopos.

Regular completion

Recall that there is a 2-category $\mathrm{HDC}(K)$ of homwise-discrete categories in any finitely complete 2-category $K$. We write $n{\mathrm{Cong}}_s(K)$ for its full sub-2-category spanned by the $n$-congruences (always we take $n=$ 2, (2,1), (1,2), or 1). Recall that there is a functor $\Phi :K\to 2{\mathrm{Cong}}_s(K)$ sending each object to its kernel; if $K$ is an $n$-category then the image of $\Phi$ is contained in $n\mathrm{Cong}(K)$.

Lemma

Suppose that $K$ has finite limits. Then:

1. $\mathrm{HDC}(K)$ has finite limits.
2. $n{\mathrm{Cong}}_s(K)$ is closed under finite limits in $\mathrm{HDC}(K)$.
3. $\Phi$ is 2-fully-faithful (that is, an equivalence on hom-categories) and preserves finite limits.

Proof

It suffices to deal with finite products, inserters, and equifiers. Evidently $\Phi (1)$ is a terminal object. If $D$ and $E$ are homwise-discrete categories, define $P_0=D_0\times E_0$ and $P_1=D_1\times E_1$; it is easy to check that then $P_1\rightrightarrows P_0$ is a homwise-discrete category that is the product $D\times E$ in $\mathrm{HDC}(K)$. Since $(D_0\times E_0{)}^2\simeq (D_0{)}^2\times (E_0{)}^2$, and products preserve ffs, we see that $P$ is an $n$-congruence if $D$ and $E$ are and that $\Phi$ preserves products.

For inserters, let $f,g:C\rightrightarrows D$ be functors in $\mathrm{HDC}(K)$, define $i_0:I_0\to C_0$ by the pullback

$$\begin{array}{ccc}{I}_0& \to & D_1\\ i_0\downarrow & & \downarrow \\ C_0& \stackrel{(f_0,g_0)}{\to }& D_0\times D_0,\end{array}$$\array{I_0 & \to & D_1\\ i_0 \downarrow && \downarrow \\ C_0 & \overset{(f_0,g_0)}{\to} & D_0\times D_0,}

and define $i_1:I_1\to C_1$ by the pullback

$$\begin{array}{ccc}{I}_1& \to & X\\ i_1\downarrow & & \downarrow \\ C_1& \stackrel{(f_1,g_1)}{\to }& D_1\times D_1\end{array}$$\array{I_1 & \to & X\\ i_1\downarrow && \downarrow\\ C_1 & \overset{(f_1,g_1)}{\to} & D_1\times D_1}

where $X$ is the “object of commutative squares in $D$.” Then $I_1\rightrightarrows I_0$ is a homwise-discrete category and $i:I\to C$ is an inserter of $f,g$. Also, $I$ is an $n$-congruence if $C$ is, and $\Phi$ preserves inserters.

Finally, for equifiers, suppose we have functors $f,g:C\rightrightarrows D$ and 2-cells $\alpha ,\beta :f\rightrightarrows g$ in $\mathrm{HDC}(K)$, represented by morphisms $a,b:C_0\rightrightarrows D_1$ such that $(s,t)a\cong (f_0,g_0)\cong (s,t)b$. Let $e_0:E_0\to C_0$ be the universal morphism equipped with an isomorphism $\varphi :a{e}_0\cong b{e}_0$ such that $(s,t)\varphi$ is the given isomorphism $(s,t)a\cong (s,t)b$ (this is a finite limit in $K$.) Note that since $(s,t):D_1\to D_0\times D_0$ is discrete, $e_0$ is ff. Now let $E_1=(e_0\times e_0{)}^{*}{C}_1$; then $E_1\rightrightarrows E_0$ is a homwise-discrete category and $e:E\to C$ is an equifier of $\alpha$ and $\beta$ in $\mathrm{HDC}(K)$. Also $E$ is an $n$-congruence if $C$ is, and $\Phi$ preserves equifiers.

For any morphism $f:A\to B$ in $K$, $\Phi (f)$ is the functor $\ker (A)\to \ker (B)$ that consists of $f:A\to B$ and $f^2:A^2\to B^2$. A transformation between $\Phi (f)$ and $\Phi (g)$ is a morphism $A\to B^2$ whose composites $A\to B^2\rightrightarrows B$ are $f$ and $g$; but this is just a transformation $f\to g$ in $K$. Thus, $\Phi$ is homwise fully faithful. And homwise essential-surjectivity follows from the essential uniqueness of thin structures, or equivalently a version of Prop 6.4 in FBMF.

Moreover, we have:

Theorem

If $K$ is an $n$-category with finite limits, then $n{\mathrm{Cong}}_s(K)$ is regular.

Proof

It is easy to see that a functor $f:C\to D$ between $n$-congruences is ff in $n{\mathrm{Cong}}_s(K)$ iff the square

$$\begin{array}{ccc}{C}_1& \to & D_1\\ \downarrow & & \downarrow \\ C_0\times C_0& \to & D_0\times D_0\end{array}$$\array{C_1 & \to & D_1\\ \downarrow && \downarrow\\ C_0\times C_0 & \to & D_0\times D_0}

is a pullback in $K$.

We claim that if $e:E\to D$ is a functor such that $e_0:E_0\to D_0$ is split (that is, $e_{0}s\cong 1_{D_0}$ for some $s:D_0\to E_0$), then $e$ is eso in $n{\mathrm{Cong}}_s(K)$. For if $e\cong fg$ for some ff $f:C\to D$ as above, then we have $g_{0}s:D_0\to C_0$ with $f_0{g}_{0}s\cong e_{0}s\cong 1_{D_0}$, and so the fact that $C_1$ is a pullback induces a functor $h:D\to C$ with $h_0=g_{0}s$ and $fh\cong 1_D$. But this implies $f$ is an equivalence; thus $e$ is eso.

Moreover, if $e_0:E_0\to D_0$ is split, then the same is true for any pullback of $e$. For the pullback of $e:E\to D$ along some $k:C\to D$ is given by a $P$ where $P_0=E_0{\times }_{D_0}{D}_{\mathrm{iso}}{\times }_{D_0}{C}_0$; here $D_{\mathrm{iso}}\hookrightarrow D_1$ is the “object of isomorphisms” in $D$. What matters is that the projection $P_0\to C_0$ has a splitting given by combining the splitting of $e_0$ with the “identities” morphism $D_0\to D_{\mathrm{iso}}$.

Now suppose that $f:D\to E$ is any functor in $n{\mathrm{Cong}}_s(K)$. It is easy to see that if we define $Q_0=D_0$ and let $Q_1$ be the pullback

$$\begin{array}{ccc}{Q}_1& \to & E_1\\ \downarrow & & \downarrow \\ Q_0\times Q_0& \stackrel{f_0\times f_0}{\to }& E_0\times E_0\end{array}$$\array{ Q_1 & \to & E_1 \\ \downarrow && \downarrow\\ Q_0 \times Q_0 & \overset{f_0\times f_0}{\to} & E_0\times E_0}

then $f\cong me$ where $e:D\to Q$ and $m:Q\to E$ are the obvious functors. Moreover, clearly $m$ is ff, and $e$ satisfies the condition above, so any pullback of it is eso. It follows that if $f$ itself were eso, then it would be equivalent to $e$, and thus any pullback of it would also be eso; hence esos are stable under pullback.

Since $m$ is ff, the kernel of $f$ is the same as the kernel of $e$, so to prove $K$ regular it remains only to show that $e$ is a quotient of that kernel. If $C\rightrightarrows D$ denotes $\ker (f)$, then $C$ is the comma object $(f/f)$ and thus we can calculate

$$C_0=D_0{\times }_{E_0}{E}_1{\times }_{E_0}{D}_0\cong Q_1.$$C_0 = D_0\times_{E_0} E_1 \times_{E_0} D_0 \cong Q_1.

Therefore, if $g:D\to X$ is equipped with an action by $\ker (f)$, then the action 2-cell is given by a morphism $Q_1=C_0\to X_1$, and the action axioms evidently make this into a functor $Q\to X$. Thus, $Q$ is a quotient of $\ker (f)$, as desired.

However, there are three problems with the 2-category $n{\mathrm{Cong}}_s(K)$.

1. It is too big. It is not necessary to include every $n$-congruence in order to get a regular category containing $K$, only those that occur as kernels of morphisms in $K$.
2. It is too small. While it is regular, it is not exact.
3. It doesn’t remember information about $K$. If $K$ is already regular, then passing to $n{\mathrm{Cong}}_s(K)$ destroys most of the esos and quotients already present in $K$.

The solution to the first problem is straightforward. If $K$ is a 2-category with finite limits, define $K_{\mathrm{reg}/\mathrm{lex}}$ to be the sub-2-category of $2{\mathrm{Cong}}_s(K)$ spanned by the 2-congruences which occur as kernels of morphisms in $K$. If $K$ is an $n$-category then any such kernel is an $n$-congruence, so in this case $K_{\mathrm{reg}/\mathrm{lex}}$ is contained in $n{\mathrm{Cong}}_s(K)$ and is an $n$-category. Also, clearly $\Phi$ factors through $K_{\mathrm{reg}/\mathrm{lex}}$.

Theorem

For any finitely complete 2-category $K$, the 2-category $K_{\mathrm{reg}/\mathrm{lex}}$ is regular, and the functor $\Phi :K\to K_{\mathrm{reg}/\mathrm{lex}}$ induces an equivalence

$$\mathrm{Reg}(K_{\mathrm{reg}/\mathrm{lex}},L)\simeq \mathrm{Lex}(K,L)$$Reg(K_{reg/lex},L) \simeq Lex(K,L)

for any regular 2-category $K$.

Here $\mathrm{Reg}(-,-)$ denotes the 2-category of regular functors, transformations, and modifications between two regular 2-categories, and likewise $\mathrm{Lex}(-,-)$ denotes the 2-category of finite-limit-preserving functors, transformations, and modifications between two finitely complete 2-categories.

Proof

It is easy to verify that $K_{\mathrm{reg}/\mathrm{lex}}$ is closed under finite limits in $2{\mathrm{Cong}}_s(K)$, and also under the eso-ff factorization constructed in Theorem 28; thus it is regular. If $F:K\to L$ is a lex functor where $L$ is regular, we extend it to $K_{\mathrm{reg}/\mathrm{lex}}$ by sending $\ker (f)$ to the quotient in $L$ of $\ker (Ff)$, which exists since $L$ is regular. It is easy to verify that this is regular and is the unique regular extension of $F$.

In particular, if $K$ is a regular 1-category, $K_{\mathrm{reg}/\mathrm{lex}}$ is the ordinary regular completion of $K$. In this case our construction reduces to one of the usual constructions (see, for example, the Elephant).

To solve the second and third problems with $n{\mathrm{Cong}}_s(K)$, we need to modify its morphisms.

Exact completion

Recall that 2-congruences in $\mathrm{Cat}$ can be identified with certain double categories. As noted in PAPDC, edge-symmetric double categories with a thin structure are essentially the same as 2-categories, and homwise-discreteness makes them the same as 1-categories. Our lack of edge-symmetry means that we really have a 1-category with distinguished subclass of morphisms (the vertical ones), which must be preserved by functors between congruences. (Note that the transformations are “horizontal” and need not have distinguished components. Since every vertical arrow has a horizontal companion, any vertical transformation is represented by a horizontal one.) In order to eliminate the effect of the distinguished vertical morphisms, we can replace functors between congruences by anafunctors.

Definition

Suppose that $K$ is a finitely complete 2-site and that $D$, $E$, and $F$ are 2-congruences in $K$. A functor $g:F\to D$ is a weak equivalence if 1. the square

$$\begin{array}{ccc}{F}_1& \stackrel{g_1}{\to }& D_1\\ \downarrow & & \downarrow \\ F_0\times F_0& \stackrel{g_0\times g_0}{\to }& D_0\times D_0\end{array}$$\array{F_1 &\overset{g_1}{\to} & D_1 \\ \downarrow && \downarrow\\ F_0\times F_0 & \overset{g_0\times g_0}{\to} & D_0\times D_0}

is a pullback, and 1. $g_0:F_0\to D_0$ is a cover (a one-element covering family). An anafunctor $D\to E$ is a span of functors $D\stackrel{f^s}{\leftarrow }F\stackrel{f^t}{\to }E$ such that $f^s$ is a weak equivalence.

The primary example we have in mind is when $K$ is a regular 2-category with its regular coverage, but it is useful to consider the general case.

Definition

If $D\leftarrow F\to E$ and $D\leftarrow G\to E$ are anafunctors between 2-congruences, then a transformation $F\to G$ is a transformation between the two induced functors $F{\times }_{D}G\rightrightarrows E$.

(Here $F{\times }_{D}G$ denotes the pullback in $2{\mathrm{Cong}}_s(K)$.)

Theorem

For any subcanonical and finitely complete 2-site $K$ (such as a regular $n$-category with its regular coverage), there is a finitely complete 2-category $2\mathrm{Cong}(K)$ of 2-congruences, anafunctors, and transformations in $K$. It contains $2{\mathrm{Cong}}_s(K)$ as a homwise-full sub-2-category (that is, $2{\mathrm{Cong}}_s(K)(D,E)\hookrightarrow 2\mathrm{Cong}(K)(D,E)$ is ff) closed under finite limits.

Proof

Composition is, of course, by pullback. Since covers are stable under pullback and composition, the composite of anafunctors is again an anafunctor. The coverage must be subcanonical in order to define the vertical composite of natural transformations. We regard a functor as an anafunctor by taking $f^s$ to be the identity; it is then clear that a transformation between functors is the same as a transformation between their corresponding anafunctors.

It is easy to see that products in $2{\mathrm{Cong}}_S(K)$ remain products in $n\mathrm{Cong}(K)$. Before dealing with inserters and equifiers, we observe that if $A\leftarrow F\to B$ is an anafunctor in $2\mathrm{Cong}(K)$ and $e:X_0\to F_0$ is any eso, then pulling back $F_1$ to $X_0\times X_0$ defines a new congruence $X$ and an anafunctor $A\leftarrow X\to B$ which is isomorphic to the original in $2\mathrm{Cong}(K)(A,B)$. Thus, if $A\leftarrow F\to B$ and $A\leftarrow G\to B$ are parallel anafunctors in $2\mathrm{Cong}(K)$, by pulling them both back to $F{\times }_{A}G$ we may assume that they are defined by spans with the same first leg, i.e. we have $A\leftarrow X\rightrightarrows B$.

Now, for the inserter of $F$ and $G$ as above, let $E\to X$ be the inserter of $X\rightrightarrows B$ in $2{\mathrm{Cong}}_s(K)$. It is easy to check that the composite $E\to X\to A$ is an inserter of $F,G$ in $2\mathrm{Cong}(K)$. Likewise, given $\alpha ,\beta :F\rightrightarrows G$ with $F$ and $G$ as above, we have transformations between the two functors $X\rightrightarrows B$ in $2{\mathrm{Cong}}_s(K)$, and it is again easy to check that their equifier in $2{\mathrm{Cong}}_s(K)$ is again the equifier in $2\mathrm{Cong}(K)$ of the original 2-cells $\alpha ,\beta$. Thus, $2\mathrm{Cong}(K)$ has finite limits. Finally, by construction clearly the inclusion of $2{\mathrm{Cong}}_s(K)$ preserves finite limits.

We write $n\mathrm{Cong}(K)$ for the full sub-2-category of $2\mathrm{Cong}(K)$ on the $n$-congruences, which is a finitely complete $n$-category. Of course, it contains $n{\mathrm{Cong}}_s(K)$ as a homwise-full sub-$n$-category closed under finite limits, and when $K$ is an $n$-category we have $\Phi :K\to n\mathrm{Cong}(K)$.

Theorem

If $K$ is a subcanonical finitely complete $n$-site, then the functor $\Phi :K\to n\mathrm{Cong}(K)$ is 2-fully-faithful. If $K$ is an $n$-exact $n$-category equipped with its regular coverage, then $\Phi :K\to n\mathrm{Cong}(K)$ is an equivalence of 2-categories.

Proof

Since $\Phi :K\to n{\mathrm{Cong}}_s(K)$ is 2-fully-faithful and $n{\mathrm{Cong}}_s(K)\to n\mathrm{Cong}(K)$ is homwise fully faithful, $\Phi :K\to n\mathrm{Cong}(K)$ is homwise fully faithful. For homwise essential-surjectivity, suppose that $\ker (A)\leftarrow F\to \ker (B)$ is an anafunctor. Then $h:F_0\to A$ is a cover and $F_1$ is the pullback of $A^2$ along it; but this just says that $F_1=(h/h)$. The functor $F\to B$ consists of morphisms $g:F_0\to B$ and $F_1=(h/h)\to B^2$, and functoriality says precisely that the resulting 2-cell equips $g$ with an action by the congruence $F$. But since $F$ is precisely the kernel of $h:F_0\to A$, which is a cover in a subcanonical 2-site and hence the quotient of this kernel, we have an induced morphism $f:A\to B$ in $K$. It is then easy to check that $f$ is isomorphic, as an anafunctor, to $F$. Thus, $\Phi$ is homwise an equivalence.

Now suppose that $K$ is an $n$-exact $n$-category and that $D$ is an $n$-congruence. Since $K$ is $n$-exact, $D$ has a quotient $q:D_0\to Q$, and since $D$ is the kernel of $q$, we have a functor $D\to \ker (Q)$ which is a weak equivalence. Thus, we can regard it either as an anafunctor $D\to \ker (Q)$ or $\ker (Q)\to D$, and it is easy to see that these are inverse equivalences in $n\mathrm{Cong}(K)$. Thus, $\Phi$ is essentially surjective, and hence an equivalence.

Note that by working in the generality of 2-sites, this construction includes the previous one. Specifically, if $K$ is a finitely complete 2-category equipped with its minimal coverage, in which the covering families are those that contain a split epic, then $n\mathrm{Cong}(K)\simeq n{\mathrm{Cong}}_s(K)$. This is immediate from the proof of Theorem 28, which implies that the first leg of any anafunctor relative to this coverage is both eso and ff in $n{\mathrm{Cong}}_s(K)$, and hence an equivalence.

We also remark in passing that this allows us to reconstruct 2-exact 2-categories with enough groupoids or discretes from their subcategories of such.

Theorem

If $K$ is a 2-exact 2-category with enough groupoids, then $K\simeq 2\mathrm{Cong}(\mathrm{gpd}(K))$. Likewise, if $K$ is 2-exact and has enough discretes, then $K\simeq 2\mathrm{Cong}(\mathrm{disc}(K))$.

Proof

Define a functor $K\to 2\mathrm{Cong}(\mathrm{gpd}(K))$ by taking each object $A$ to the kernel of $j:J\to A$ where $j$ is eso and $J$ is groupoidal (for example, it might be the core of $A$). Note that this kernel lives in $2\mathrm{Cong}(\mathrm{gpd}(K))$ since $(j/j)\to J\times J$ is discrete, hence $(j/j)$ is also groupoidal. The same argument as in Theorem 31 shows that this functor is 2-fully-faithful for any regular 2-category $K$ with enough groupoids, and essentially-surjective when $K$ is 2-exact; thus it is an equivalence. The same argument works for discrete objects.

In particular, the 2-exact 2-categories having enough discretes are precisely the 2-categories of internal categories and anafunctors in 1-exact 1-categories.

Our final goal is to construct the $n$-exact completion of a regular $n$-category, and a first step towards that is the following.

Theorem

If $K$ is a regular $n$-category, so is $n\mathrm{Cong}(K)$. The functor $\Phi :K\to n\mathrm{Cong}(K)$ is regular, and moreover for any $n$-exact 2-category $L$ it induces an equivalence

$$\mathrm{Reg}(n\mathrm{Cong}(K),L)\to \mathrm{Reg}(K,L).$$Reg(n Cong(K), L) \to Reg(K,L).

Proof

We already know that $n\mathrm{Cong}(K)$ has finite limits and $\Phi$ preserves finite limits. The rest is very similar to Theorem 28. We first observe that an anafunctor $A\leftarrow F\to B$ is an equivalence as soon as $F\to B$ is also a weak equivalence (its reverse span $B\leftarrow F\to A$ then provides an inverse.) Also, $A\leftarrow F\to B$ is ff if and only if

$$\begin{array}{ccc}{F}_1& \to & B_1\\ \downarrow & & \downarrow \\ F_0\times F_0& \to & B_0\times B_0\end{array}$$\array{F_1 & \to & B_1\\ \downarrow && \downarrow \\ F_0\times F_0 & \to & B_0\times B_0}

is a pullback.

Now we claim that if $A\leftarrow F\to B$ is an anafunctor such that $F_0\to B_0$ is eso, then $F$ is eso. For if we have a composition

$$\begin{array}{ccccc}& & & & F\\ & & & \swarrow & & \searrow \\ & & G& & & & M\\ & \swarrow & & \searrow & & \swarrow & & \searrow \\ A& & & & C& & & & B\end{array}$$\array{ &&&& F \\ &&& \swarrow && \searrow\\ && G &&&& M\\ & \swarrow && \searrow && \swarrow && \searrow\\ A &&&& C &&&& B}

such that $M$ is ff, then $F_0\to B_0$ being eso implies that $M_0\to B_0$ is also eso; thus $M\to B$ is a weak equivalence and so $M$ is an equivalence. Moreover, by the construction of pullbacks in $n\mathrm{Cong}(K)$, anafunctors with this property are stable under pullback.

Now suppose that $A\leftarrow F\to B$ is any anafunctor, and define $C_0=F_0$ and let $C_1$ be the pullback of $B_1$ to $C_0\times C_0$ along $C_0=F_0\mathrm{to}{B}_0$. Then $C$ is an $n$-congruence, $C\to B$ is ff in $n{\mathrm{Cong}}_s(K)$ and thus also in $n\mathrm{Cong}(K)$, and $A\leftarrow F\to B$ factors through $C$. (In fact, $C$ is the image of $F\to B$ in $n{\mathrm{Cong}}_s(K)$.) The kernel of $A\leftarrow F\to B$ can equally well be calculated as the kernel of $F\to B$, which is the same as the kernel of $F\to C$.

Finally, given any $A\leftarrow G\to D$ with an action by this kernel, we may as well assume (by pullbacks) that $F=G$ (which leaves $C$ unchanged up to equivalence). Then since the kernel acting is the same as the kernel of $F\to C$, regularity of $n{\mathrm{Cong}}_s(K)$ gives a descended functor $C\to D$. Thus, $A\leftarrow F\to C$ is the quotient of its kernel; so $n\mathrm{Cong}(K)$ is regular.

Finally, if $L$ is $n$-exact, then any functor $K\to L$ induces one $n\mathrm{Cong}(K)\to n\mathrm{Cong}(L)$, but $n\mathrm{Cong}(L)\simeq L$, so we have our extension, which it can be shown is unique up to equivalence.

When $K$ is a regular 1-category, it is well-known that $1\mathrm{Cong}(K)$ (which, in that case, is the category of internal equivalence relations and functional relations) is the 1-exact completion of $K$ (the reflection of $K$ from regular 1-categories into 1-exact 1-categories). Theorem 33 shows that in general, $n\mathrm{Cong}(K)$ will be the $n$-exact completion of $K$ whenver it is $n$-exact. However, in general for $n>1$ we need to “build up exactness” in stages by iterating this construction.

It is possible that the iteration will converge at some finite stage, but for now, define $n{\mathrm{Cong}}^r(K)=n\mathrm{Cong}(n{\mathrm{Cong}}^{r-1}(K))$ and let $K_{n\mathrm{ex}/\mathrm{reg}}={\mathrm{colim}}_{r}n{\mathrm{Cong}}^r(K)$.

Theorem

For any regular $n$-category $K$, $K_{n\mathrm{ex}/\mathrm{reg}}$ is an $n$-exact $n$-category and there is a 2-fully-faithful regular functor $\Phi :K\to K_{n\mathrm{ex}/\mathrm{reg}}$ that induces an equivalence

$$\mathrm{Reg}(K_{n\mathrm{ex}/\mathrm{reg}},L)\simeq \mathrm{Reg}(K,L)$$Reg(K_{n ex/reg},L) \simeq Reg(K,L)

for any $n$-exact 2-category $L$.

Proof

Sequential colimits preserve 2-fully-faithful functors as well as functors that preserve finite limits and quotients, and the final statement follows easily from Theorem 33. Thus it remains only to show that $K_{n\mathrm{ex}/\mathrm{reg}}$ is $n$-exact. But for any $n$-congruence $D_1\rightrightarrows D_0$ in $K_{n\mathrm{ex}/\mathrm{reg}}$, there is some $r$ such that $D_0$ and $D_1$ both live in $n{\mathrm{Cong}}^r(K)$, and thus so does the congruence since $n{\mathrm{Cong}}^r(K)$ sits 2-fully-faithfully in $K_{n\mathrm{ex}/\mathrm{reg}}$ preserving finite limits. This congruence in $n{\mathrm{Cong}}^r(K)$ is then an object of $n{\mathrm{Cong}}^{r+1}(K)$ which supplies a quotient there, and thus also in $K_{n\mathrm{ex}/\mathrm{reg}}$.

2-internal logic

Could not include 2-internal logic

Classifying discrete opfibrations

Definition

As in WeberYS2T, a classifying discrete opfibration in a finitely complete 2-category $K$ is a discrete opfibration $p:E\to S$ such that for any $X$, the functor

$$K(X,S)\to \mathrm{DOpf}(X),$$K(X,S) \to DOpf(X),

given by pullback of $p$, is full and faithful.

The canonical example is when $K$ is some 2-category of “large categories” and $S$ is the category of (small) sets. More generally, we could take $K$ to be the 2-category $\mathrm{Cat}$ and $S$ the category of sets of cardinality bounded by some cardinal $\lambda$.

When $K$ is equipped with a classifying discrete opfibration, we make the following definitions.

• A discrete opfibration is small if it is in the image of the above functor.
• A discrete object $X$ is small if $X\to 1$ is a small discrete opfibration.
• If $K$ has a duality involution, we say an object $A$ is locally small or arrow-small if the discrete opfibration $X\to A\times A^{op}$ corresponding to the 2-sided fibration $A\leftarrow A^2\to A$ is small.
• A not-necessarily-discrete object $A$ is small if it is locally small and admits an eso from a small discrete object.

If $K$ lacks a duality involution, then merely giving the discrete opfibration $E\to S$ doesn’t suffice to characterize the notion of “smallness,” since we can’t define what it means to be locally small. This suggests the definition of a size structure.

Additional axioms

We may impose additional axiom on a classifying discrete opfibration, many of which assert closure conditions of the class of small maps.

• Identity maps are small.
• The composite of small discrete opfibrations is small (the “axiom of replacement”).
• All cosieves are small (the “axiom of separation”).
• If $qr$ and $q$ are small discrete opfibrations, then so is $r$ (“full slices”).
• If $q$ is a discrete opfibration, $qr$ is a small discrete opfibration and $r$ is eso, then $q$ is a small discrete opfibration (“quotients”).
• If $q$ is a discrete opfibration whose pullback along an eso is a small discrete opfibration, then $q$ is small (“descent”).
• The map $p:E\to S$ is exponentiable.

Some immediate consequences are:

• If identity maps are small, then each category $K(X,S)$ has a natural terminal object, and so $S$ “has a terminal object” internally, i.e. $S\to 1$ has a right adjoint.
• If small discrete opfibrations are closed under composition, then if $Y\to X$ and $Z\to X$ are small discrete opfibrations, so is $Y{\times }_{X}Z\to Y$, and thus so is the composite $Y{\times }_{X}Z\to X$. Hence $K(X,S)$ has binary products naturally, and thus $S$ “has binary products” internally, i.e. the diagonal $S\to S\times S$ has a right adjoint.
• In particular, if small discrete opfibrations form a subcategory, then $S$ is a cartesian object.
• One can also show that the “axiom of replacement” implies that any small object is the quotient of an internal category (2-congruence) in $\mathrm{sm}(\mathrm{disc}(K))$, the category of small discrete objects.

We will see some further consequences of these axioms below.

The universal map as a comma object

Theorem

Suppose that $p:E\to S$ is a classifying discrete opfibration for which identity maps are small. Then there is a comma square

$$\begin{array}{ccc}E& \stackrel{}{\to }& 1\\ {}^p\downarrow & \Downarrow & {\downarrow }^1\\ S& \underset{\mathrm{id}}{\to }& S\end{array}$$\array{E & \overset{}{\to} & 1\\ ^p\downarrow &\Downarrow& \downarrow^1\\ S & \underset{id}{\to} & S}

in which the map $1\to S$ classifies the discrete opfibration ${\mathrm{id}}_1:1\to 1$.

Proof

A map $X\to E$ is the same as a discrete opfibration $q:Y\to X$ equipped with a section $s:X\to Y$ with $ps\cong 1$. Thus, it suffices to show that giving such data is equivalent to giving a square

$$\begin{array}{ccc}X& \stackrel{}{\to }& 1\\ \downarrow & \Downarrow & \downarrow \\ S& \underset{\mathrm{id}}{\to }& S\end{array}$$\array{X & \overset{}{\to} & 1\\ \downarrow & \Downarrow& \downarrow\\ S & \underset{id}{\to} & S}

in which the left-hand vertical map $X\to S$ classifies $q$. But the composite $X\to 1\to S$ classifies $\mathrm{id}:X\to X$, so since pullback of $p$ is full and faithful into discrete opfibrations, giving such a 2-cell is the same as giving a map $\mathrm{id}\to q$ of discrete opfibrations over $X$, which is precisely to give a section of $q$.

Families

Suppose that $p:E\to S$ is a CDO which is exponentiable. Then for any object $A$, we call the exponential

$$\mathrm{Fam}(A)≔(S\times A\to S{)}^{(E\to S)}$$Fam(A) \coloneqq (S\times A \to S)^{(E\to S)}

the object of (small) families in $A$. It comes with a projection to $S$ which “assigns to each family its indexing set.” Moreover, as observed in our study of exponentials, since $p$ is an opfibration and $S\times A\to S$ is a fibration, then $\mathrm{Fam}(A)\to S$ is also a fibration, as we would expect.

$\mathrm{Fam}(A)$ has a universal property that can be directly expressed as follows. Evidently, to give a morphism $X\to \mathrm{Fam}(A)$ is equivalent to giving a map $X\to S$ together with a map $X{\times }_{S}E\to S\times A$ over $S$. But $X{\times }_{S}E$ is simply the discrete opfibration classified by $X\to S$, and a map to $S\times A$ over $S$ is just an arbitrary map to $A$. Thus to give a map $X\to \mathrm{Fam}(A)$ is the same as to give a small discrete opfibration $Y\to X$ together with a map $Y\to A$: in other words, an $X$-indexed family of small sets, each of which indexes a family of objects of $A$.

(This sort of thing is closely related to the construction of generic families in Algebraic Set Theory.)

Families of sets as a codomain fibration

Now consider the special case when $A=S$. As above, to give a map $X\to \mathrm{Fam}(S)$ is to give a small discrete opfibration $Y\to X$ and a map $Y\to S$. But a map $Y\to S$ is in turn equivalent to a small discrete opfibration $Z\to Y$. Thus $K(X,\mathrm{Fam}(S))$ is naturally equivalent the category of composable pairs $Z\to Y\to X$ of small discrete opfibrations. Recalling that any map between discrete opfibrations over $X$ is again a discrete opfibration, we observe that the 1-category $\mathrm{DOpf}(K/X{)}^2$ consists of composable pairs $Z\to Y\to X$ of discrete opfibrations; thus $K(X,\mathrm{Fam}(S))$ is naturally a full subcategory of this category.

On the other hand, we can consider another full subcategory of $\mathrm{DOpf}(K/X{)}^2$ determined by those composable pairs $Z\to Y\to X$ in which $Y\to X$ and the composite $Z\to X$ are small. This is precisely the subcategory $\mathrm{SDOpf}(K/X{)}^2$, where $\mathrm{SDOpf}(K/X)$ consists of small discrete opfibrations, and is thus equivalent to $K(X,S)$. It follows that this second full subcategory of $\mathrm{DOpf}(K/X{)}^2$ is equivalent to $K(X,S^2)$. Clearly these two subcategories agree if and only if small discrete opfibrations are closed under composition and have full slices, in the terminology defined above. Thus we have proven:

Theorem

Let $p:E\to S$ be an exponentiable classifying discrete opfibration; the following are equivalent.

1. Small discrete opfibrations are closed under composition and have full slices.
2. For each $X$, the categories $K(X,\mathrm{Fam}(S))$ and $K(X,S^2)$ are equivalent as full subcategories of $\mathrm{DOpf}(K/X{)}^2$.

When these conditions hold, we clearly have a natural equivalence $K(X,\mathrm{Fam}(S))\simeq K(X,S^2)$ lying over $K(X,S)$, and therefore, by the Yoneda lemma, an equivalence over $S$ between $\mathrm{Fam}(S)\to S$ and the codomain fibration $S^2\to S$.

(Note the slight peculiarity of this result: it is more common, when showing that two things are equivalent under certain conditions, to construct a canonical map between them which always exists and happens to be an equivalence in the cases of interest. Here instead we have constructed a canonical cospan which induces an equivalence in the cases of interest.)

Colloquially speaking, this theorem says that the category $S$ of sets satisfies the “replacement axiom” if and only if the “naive indexing” $\mathrm{Fam}(S)$ of $S$ over itself is equivalent to its “self-indexing” $S^2$. In classical material set theory, this is well-known to be equivalent to the usual axiom of replacement.

Note, though, that depending on what $K$ is, $\mathrm{Fam}(S)$ may not be the “naive indexing” at all. For instance, if $K$ is the category of stacks on a topos $E$, then the self-indexing of $E$ is a classifying discrete opfibration in $K$, which always satisfies the “axiom of replacement,” essentially by construction. Analogous facts are well-known in algebraic set theory, and are one reason why “the axiom of replacement” is a bit slippery in structural set theory. Generally, in intuitionistic logic, the axioms of replacement and collection add no extra proof-theoretic strength because they can be made to hold internally in suitable (2-)topoi of sheaves/stacks; it is the axiom of separation which carries all the power distinguishing IZF from IETCS.

Constructing familiar categories

Given a classifying discrete opfibration, we can use finite 2-categorical limits and the “internal logic” to construct all the usual concrete categories out of the object $S$. For instance, if small discrete opfibrations are a subcategory, so that $S$ is a cartesian object, then we have the composite $S\to S\times S\to S$ of the diagonal with the “binary products” morphism which, intuitively, takes a set $A$ to the set $A\times A$. Now the inserter of this composite and ${\mathrm{id}}_S$ can be considered “the category of sets $A$ equipped with a function $A\times A\to A$,” i.e. the category of magmas.

Now we have a forgetful morphism $\mathrm{magma}\to \mathrm{set}$, and also a functor $\mathrm{magma}\to \mathrm{set}$ which takes a magma to the triple product $A\times A\times A$, and there are two 2-cells relating these constructed from two different composites of the inserter 2-cell defining the category of magmas. It makes sense to call the equifier of these 2-cells “the category of semigroups” (sets with an associative binary operation). Proceeding in this way we can construct the categories of monoids, groups, abelian groups, and eventually rings.

A more direct way to describe these categories with a universal property is as follows. Since $S$ is a cartesian object, each hom-category $K(X,S)$ has finite products, so we can define the category $\mathrm{ring}(K(X,S))$ of rings internal to it. Then the category $\mathrm{ring}$ is equipped with a forgetful functor $\mathrm{ring}\to \mathrm{set}$ which has the structure of a ring in $K(\mathrm{ring},\mathrm{set})$, and which is universal in the sense that we have a natural equivalence $\mathrm{ring}(K(X,S))\simeq K(X,\mathrm{ring})$. The above construction then just shows that such a representing object exists.

Preservation

If $K$ has a duality involution and $p:E\to S$ is a classifying discrete opfibration, then $p^o:E^o\to S^o$ is a “classifying discrete fibration,” and therefore also a classifying discrete opfibration in $K^{\mathrm{co}}$.

A classifying discrete opfibration in $K$ is not inherited by any category of truncated objects in $K$, since $E$ and $S$ will generally not be truncated. However, it is inherited by (op)fibrational slices.

Recall first that opfibrations in $\mathrm{Opf}(X)$ can be identified with morphisms in $\mathrm{Opf}(X)$ whose underlying morphism in $K$ is an opfibration. Moreover, such an opfibration is discrete if and only if its underlying morphism in $K$ is so. Thus, it is natural to hope for the following.

Theorem

If $K$ has exponentials and a classifying discrete opfibration, then each 2-category ${\mathrm{Opf}}_K(X)$ has a classifying discrete opfibration, and the small opfibrations in $\mathrm{Opf}(X)$ are those whose underlying opfibrations in $K$ are small.

Proof

Recall that when $K$ has exponentials, $\mathrm{Opf}(X)$ is comonadic over $K/X$; let $G_X$ denote the comonad. For any $A$, write $\mathrm{SOpf}(A)$ for the category of small discrete opfibrations over $A$. Then our goal is for ${\mathrm{SOpf}}_{\mathrm{Opf}(X)}(A\to X):=\mathrm{SOpf}(A)$ to be representable. But we have

$$\mathrm{SOpf}(A)\simeq K(A,S)\simeq K({\Sigma }_X(A\to X),S)\simeq K/X(A,X\times S)\simeq \mathrm{Opf}(X)(A,G_X(X\times S)).$$SOpf(A) \simeq K(A,S) \simeq K(\Sigma_X (A\to X), S) \simeq K/X(A, X\times S) \simeq Opf(X)(A,G_X(X\times S)).

Therefore, defining $S_X=G_X(X\times S\to X)$ we obtain a classifying discrete opfibration in $\mathrm{Opf}(X)$ that classifies the desired small opfibrations.

Corollary

If $K$ has exponentials, a duality involution, and a classifying discrete opfibration, then each 2-category ${\mathrm{Fib}}_K(X)$ also has a classifying discrete opfibration.

Proof

This follows from Theorem 36 since $\mathrm{Fib}(X)\simeq \mathrm{Opf}(X^o)$. The classifying object is explicitly given by $V_X(G_{X^o}(X^o\times S\to X^o))$, although the small maps are not as explicitly characterized.

Classifying cosieves

A cosieve is a morphism $A\to X$ in a 2-category that is both ff and a discrete opfibration. Equivalently, it is a subterminal object in $\mathrm{Opf}(X)$. It is easy to check that in $\mathrm{Cat}$, this is equivalent to saying that $A$ is a full subcategory of $X$ such that if $a\in A$ and $f:a\to b$, then $b\in A$.

A classifying cosieve is a classifying discrete opfibration which is a cosieve—and hence classifies only cosieves, since cosieves are stable under pullback. We write $\zeta \to \Omega$ for a classifying cosieve. Clearly any such $\Omega$ is posetal.

A cosieve classifier is a classifying cosieve which classifies all cosieves. In this case one can show, just as for the subobject classifier in a topos, that $\zeta =1$. In $\mathrm{Cat}$, the “walking arrow” $2$ is a cosieve classifier.

Construction from classifying discrete opfibrations

If $E\to S$ is any classifying discrete opfibration in a Heyting 2-pretopos $K$, then the subobject of $S$ described in the internal logic by

$$\{x:S\mid (\forall a:E(x))(\forall b:E(x))(\exists f:{\mathrm{hom}}_E(a,b))\top \}$$\{x:S | (\forall a:E(x))(\forall b:E(x))(\exists f:hom_E(a,b))\top \}

is the largest subobject $\Omega \hookrightarrow S$ such that the pullback of $E$ to $\Omega$ is a cosieve. (Verifying this is a straightforward argument using the Kripke-Joyal semantics?.) It is thus a classifying cosieve, which is canonically associated to $E\to S$.

In $\mathrm{Cat}$, the cosieve classifier $2$ arises from $\mathrm{Set}$ (or any full subcategory of it containing $0$ and $1$) in this way.

From cosieve classifiers to subobject classifiers

If $X$ is groupoidal, then every ff into $X$ is a cosieve. Therefore, maps from a groupoidal $X$ into a cosieve classifier $\Omega$ classify all subobjects of $X$. Since subobjects of $X$ are the same as subobjects of its core $J(X)$ if that exists, subobjects of $X$ can be classified by maps $J(X)\to \Omega$.

Moreover, if a cosieve classifier $\Omega$ itself has a core, then since $J(\Omega )$ is a coreflection of $\Omega$ into $\mathrm{gpd}(K)$, it is a subobject classifier in $\mathrm{gpd}(K)$ in a suitable (2,1)-categorical sense. Moreover, since $\Omega$ is posetal, its core (if it exists) is discrete. Thus:

Theorem

If $K$ is a 2-category having a cosieve classifier and enough groupoids, then $\mathrm{disc}(K)$ has a subobject classifier.

In particular, if $K$ also has (discrete) exponentials, then $\mathrm{disc}(K)$ is a topos.

However, $\mathrm{disc}(K)$ can have both a subobject classifier and a cosieve classifier without the former being a core of the latter. For instance, in the 2-presheaf 2-topos $K=[C,\mathrm{Cat}]$, the category $\mathrm{disc}(K)$ is the 1-topos of 1-sheaves on the homwise-discrete reflection of $C$, but there will not in general be a map in either direction relating its subobject classifier to the cosieve classifier.

A subobject classifier can also be constructed from a cosieve classifier in a Heyting 2-category with a duality involution. For then if $\Omega$ is a cosieve classifier, ${\Omega }^o$ is a sieve opclassifier, i.e. $K(X,{\Omega }^o)$ is equivalent to the opposite of the poset of sieves on $X$. On $\Omega \times {\Omega }^o$ we thus have both a sieve $R$ and a cosieve $S$, pulled back from $\Omega$ and ${\Omega }^o$; let ${\Omega }_d$ be the subobject of $\Omega \times {\Omega }^o$ defined as $R\iff S$ in the Heyting algebra structure. Now maps into ${\Omega }_d$ classify sieves and cosieves that are equal as subobjects, which is to say, subobjects that are both sieves and cosieves. And transformations between maps $X\to {\Omega }_d$ correspond to both inclusions of cosieves and coinclusions of sieves, which is to say, identities; thus ${\Omega }_d$ is discrete, and hence a subobject classifier in $\mathrm{disc}(K)$.

Theorem

If $K$ is a Heyting 2-category having a cosieve classifier and a duality involution, then $\mathrm{disc}(K)$ has a subobject classifier.

Replacing subobject classifiers

If $K$ has a cosieve classifier and (discrete) exponentials, but not enough groupoids, then $\mathrm{disc}(K)$ may not be a topos. But it retains many of the properties of a topos, because even though the “power object” $PX={\Omega }^X$ is not an object of $\mathrm{disc}(K)$, it can still be quantified over in the internal logic of $K$ to define objects and properties in $\mathrm{disc}(K)$, and even in $\mathrm{gpd}(K)$, where all subobjects are cosieves.

For example, if $K$ is also Heyting, then for any groupoidal $X$ we can construct the “internally least” subobject of $X$ with some property, as

$$\{x:X\mid (\forall S:PX)(\phi (S)\Rightarrow x\in S)\}.$$\{x:X | (\forall S:P X)(\varphi(S) \Rightarrow x\in S)\}.

This allows the construction of all sorts of “closure” operations that exist in a topos, such as the equivalence relation generated by any given relation on a groupoidal object. In particular:

Proposition

If $K$ is 1-exact and Heyting with exponentials and a cosieve classifier, then $\mathrm{disc}(K)$ is finitely cocomplete.

If $X$ is not groupoidal, then the above technique only constructs cosieves in $X$ rather than arbitrary subobjects of it. However, if there are enough groupoids, we can construct arbitrary subobjects of any object $X$ in this way, since subobjects of $X$ are bijective with subobjects of its core $J(X)$. In particular:

Proposition

If $K$ is 1-exact and Heyting with exponentials, a cosieve classifier, and either enough groupoids or a duality involution, then it has discrete reflections.

Proof

It suffices to be able to construct the equivalence relation generated by the image of $A^2\to A\times A$, for any $A$. Note that these relations are not cosieves on $A\times A$, but as remarked above, we can get around this if $A\times A$ has a core. Alternately, since the relations we care about are all “2-sided sieves” (subterminals in $\mathrm{Fib}(A,A)$), if there is a duality involution we can turn them into cosieves on $A^{\mathrm{op}}\times A$ and perform the closure there.

In another vein, if $K$ is a positive Heyting 2-category with a (necessarily discrete) natural numbers object $N$, we can of course construct the discrete object of rational numbers $Q$ in the usual way, and then define the Dedekind real numbers as two-sided cuts. Thus, $R$ is a subobject of $PQ\times PQ$, and hence posetal, but since the order relation on $R$ inherited from the two copies of $PQ$ would go in different directions, in fact $R$ is discrete.

I haven’t made a concerted effort yet, but I haven’t yet thought of any really important aspect of topos-ness for $\mathrm{disc}(K)$ that isn’t almost as well-served by having a posetal power-object rather than a discrete one. Mathieu Dupont was the one who originally pointed out to me that 2-categorically, power-objects are naturally posets rather than sets.