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.
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,
This is evidently a categorification of a definition such as
On the other hand, according to StreetCBS,
This is evidently a categorification of a definition such as
The definition I propose to categorify is
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 ) 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:
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.
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
from (or any topos) to posets is representable by the set of truth values, the functor
from (or, hypothetically, any 2-topos) to categories is representable by the category of sets. Here means the category of discrete opfibrations over .
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 actually takes place in the fibration of subobjects of objects of . In particular:
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 being a poset; that is, a (0,1)-category. However, for an ordinary category we also have a fundamental fibration of 1-categories, which has a corresponding “logic of 0-categories,” that is, sets. If is (for instance) a locally cartesian closed category with finite colimits, then each 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 from propositions and , we construct a new type from types and . And instead of constructing a new proposition from a proposition that depends on a variable , we construct a new type (a “dependent product”) from a type that depends on .
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 -pretopos. From an -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 and a “logic of (-1,0)-categories” (ordinary logic) that takes place in the slice posets .
It is now clear how to categorify this: in a 2-category we will have a “logic of 1-categories” that takes place in the slice 2-categories , a “logic of 0-categories” that takes place in the slice 1-categories , and a “logic of (-1,0)-categories” that takes place in the slice posets . (Actually, we could easily add logics of (1,0)-categories and (0,1)-categories taking place in and , 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 and in place 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.
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.
In many cases it turns out to be just as easy to develop the theory not just for 2-categories, but for -categories for some and . We will say that and is directed to mean that for some such . This includes the following cases:
The following values of are considered , but are not directed.
These values of are also important, but for them one doesn’t expect a notion of -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 . Sure, the concepts tend to be trivial then, but so they also tend to be when .
And actually, I don't think it's appropriate to refer to as ‘directed’. Directedness is provided only by .
—Toby
You’re right about directedness; I’ve fixed the page. What sort of “use” of nondirected were you expecting? They do come up, of course; for instance it’s important to talk about -truncated objects when is not necessarily directed. The only point is that no nontrivial -categories can be regular, exact, coherent, etc. unless is directed.
I guess it might be useful to distinguish -truncated 2-toposes even when is not directed. For instance, 0-truncated (Grothendieck) 2-toposes are just powers of , and (1,0)-truncated 1-toposes are toposes of actions by a groupoid. But you can’t say any more that an -truncated 2-topos is the category of 2-sheaves on an -topos, since there is no longer any notion of -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 ); 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 . Thus, for instance, saying that -categories form an -category includes the statements that:
and so on. For this convention it is important to remember that (-1)-category is a shorthand for (-1,0)-category, so that , not (0,0). And of course, . Note that is directed if and only if it is of the form for some .
Note that -categories are the same as -categories whenever either or . (Although for monoidal categories, and can be distinguished.) Thus, to avoid duplication, usually one restricts to . However, these requirements conflict when (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 and is .
From a previous discussion at truncated object, which doesn't really belong there:
Yes, definitely. A so called ‘-category’ (a truth value) is really a -groupoid or a -poset, that is a -category, not a -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 instead of in all cases… -Mike
Partly, this would work better if we said ‘-poset’ all the time for various values of . In general, an -category is an -poset. The bad part is that now these pages focus on , which is not so slick to say. But the general theory works better; we require (with the same exception as before, now when ) and no glitch crossing from to . —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 ‘-category’, ‘-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 -category?) —Toby
What are you claiming is the “fundamental concept?” The only candidates for a fundamental concept that I see are either full-blown -categories or -categories for arbitrary . 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 “-order” (I don’t use “poset”, since this word suggests that they have a set of objects) rather than “-category” and even -order instead of -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 -orders, which are the most general -orders of dimension . 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 -categories, for natural numbers , 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 -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 -order (= -category) there is some groupoidality; it just doesn’t kick in until the -cells. To me, a much stronger intuitive association is that “order” implies that parallel morphisms are equal. This is not true for -orders for any , except at the -cells, and is not true for any dimension of cells in an -order (= -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 to properties of -categories that maps to being an -poset (or -order) is simpler (hence should be regarded as more fundamental, with the other defined in terms of it) than the partial function that maps to being an -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 -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 , since an ordinary category is groupoidal at and above level ; and ‘order’ and ‘poset’ have the connotation of being trivial at and above level , since an ordinary order or poset is trivial at and above level . (But I don't see what's wrong with the connotation that a poset has an underlying set, since even an -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
The 1-category 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 is a pretopos.
However, at first glance, the axiom of choice seems to be necessary in order for to be a regular 2-category. Specifically, given a commutative square of functors
in which is full and faithful and is essentially surjective, in order to define a lift we have to first choose, for each , an object and an isomorphism , then defining with its action on morphisms determined by (since is ff).
Of course, there is a sense in which this is not a “real” use of choice, since is determined by 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 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.
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 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, (his ) is cartesian closed in the sense that there is an anaequivalence , and this is all one ought to need or want. Am I wrong?
Toby: But without that SCSA thing, I don't know what means in this context. That is, the category of small anafunctors from a small category to a small category is not itself small (at least not if 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 is isomorphic to one whose set of specifications is of the form
for some . And there is clearly a set of these, so the full subcategory of on them should be an exponential in .
You only need choice if you want there to be a function assigning to each anafunctor an isomorphism to one of the above form. And you can avoid using the full strength of choice by allowing yourself to replace 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 , the set of specifications from to is, if inhabited, isomorphic to . However, that isomorphism is non-canonical (to be precise, is a torsor over ). 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 and such that is inhabited, an isomorphism , and that requires some choice. Where SCSA is weaker than AC is that you don’t need to be able to choose isomorphisms to , 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, “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
The slice 2-category of a 2-category over an object is the 2-category whose objects are morphisms in , whose morphisms are triangles in that commute up to a specified isomorphism, and whose 2-cells are 2-cells in forming a commutative 2-diagram with the specified isomorphisms in triangles.
In particular, any 2-cell in must become an isomorphism in . 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 . Frequently a better replacement is the fibrational slice.
If has pullbacks, then for any there is a pullback functor . However, this does not make the assignation into a functor or , 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 always has a left adjoint given by composition with . However, cannot be expected to have a right adjoint for all maps , since this fails even in . It is true in when is a fibration or opfibration, however; see exponentials in a 2-category.
The fibrational slice of a 2-category over an object is the homwise-full sub-2-category of the slice 2-category whose objects are fibrations over and whose morphisms are morphisms of fibrations. Likewise, we have the opfibrational slice 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 has finite limits.
The 2-category is monadic over . The relevant monad on takes to the comma object , or equivalently the pullback . It is lax-idempotent, so a morphism is an opfibration if and only if has a left adjoint with invertible counit in . Likewise, is a fibration iff has a right adjoint with invertible unit in .
Since the fibrational slices are monadic over , they inherit all limits from it. It follows that a fibration is a discrete object in iff it is discrete in . These are unsurprisingly called discrete fibrations; we write for the category of such. Every morphism in between discrete fibrations is a morphism of fibrations; thus is a full subcategory of both and .
Any pullback of an (op)fibration is again an (op)fibration. Therefore, any morphism induces a pullback functor , which restricts to a functor , 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 is groupoidal, . In particular, for (2,1)-categories and thus also for 1-categories, the fibrational slices are no different from the ordinary slices.
Central for us is the following fact, which would be false if we replaced by . It underlies the inheritance of all sorts of structure by fibrational slices, such as regularity, coherency, extensivity, and exactness.
A morphism in is ff in ) iff its underlying morphism in is ff.
Suppose that and are opfibrations, and that is a morphism in which is ff in . Then since is homwise faithful, is clearly faithful in . And given a 2-cell in , since is ff in , we must have for some 2-cell . But then , so must also be a 2-cell in .
Conversely, suppose that is ff in , and that we have 2-cells in such that . Then since we have ; call this 2-cell . Since and are opfibrations and is a map of opfibrations, we have an opcartesian 2-cell lying over such that is also opcartesian. Then and both factor through to give 2-cells in whose images under are equal. Since is faithful in , we have , and hence . Thus, is faithful in . The proof of fullness is analogous.
Therefore, if is an (op)fibration in , we have , although in general the inclusion is proper. Of course, the dual result about is also true.
It is well-known that a composite of fibrations is a fibration. Moreover:
A morphism in is a fibration in the 2-category iff its underlying morphism in is a fibration.
This is a standard result, at least in the case , and is apparently due to Benabou. References include:
Therefore, for any fibration in we have , and similarly for opfibrations. This is a fibrational analogue of the standard equivalence for ordinary slice categories. It also implies that any morphism between discrete fibrations over is itself a (discrete) fibration in , since in 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:
A span is called a (two-sided) fibration from to if
of 2-cells, is an isomorphism.
Such two-sided fibrations in correspond to functors . The third condition corresponds precisely to the “interchange” equality in . We write for the 2-category of two-sided fibrations from to .
A span is a two-sided fibration from to if and only if
Recall that the projection is a fibration (and also an opfibration, although that is irrelevant here), and the cartesian 2-cells are precisely those whose component in is an isomorphism. Therefore, saying that is a morphism in , i.e. that it preserves cartesian 2-cells, says precisely that takes -cartesian 2-cells to isomorphisms.
Now, by the remarks above, is an opfibration in iff has a left adjoint with invertible counit in , and is an opfibration in iff has a left adjoint with invertible counit in . Of crucial importance is that here denotes the comma object calculated in the 2-category , or equivalently in , and it is easy to check that this is in fact equivalent to the comma object calculated in .
Therefore, is an opfibration in iff is an opfibration in and the left adjoint of is a morphism in . It is then easy to check that this left adjoint is a morphism in iff inverts -opcartesian arrows, and that it is a morphism of fibrations iff the final condition in Definition is satisfied.
In particular, we have . By duality, , and therefore , a commutation result that is not immediately obvious.
It follows that the 2-categories of two-sided fibrations also inherit any properties that can be shown to be inherited by the “one-sided” fibrational slices and . Thus, we will usually concentrate on the latter, although two-sided fibrations will make an appearance in our treatment of duality involutions.
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 -category, every object is internally a -category; exactness says that conversely every “internal -category” is represented by an object. When , 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.
If is a finitely complete 2-category, a homwise-discrete category in consists of a discrete morphism , together with composition and identity maps and in , which satisfy the usual axioms of an internal category up to isomorphism. (Since 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 are a version of the notion for internal categories, thus given by a morphism in . The 2-cells in 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 rather than a 3-category.
If is any morphism in , there is a canonical homwise-discrete category , where is the comma object of with itself. We call this the kernel of . In particular, if then , so we have a canonical homwise-discrete category called the kernel of . It is easy to check that taking kernels of objects defines a functor ; this might first have been noticed by Street.
If is a homwise-discrete category in , the following are equivalent.
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.
We consider the case ; the general case follows because all the notions are defined representably. A homwise-discrete category in 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 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 is a two-sided fibration. Then for any (vertical) arrow in we have cartesian and opcartesian morphisms (squares) in :
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
induced by factoring the horizontal identity square of through these cartesian and opcartesian squares, must be an isomorphism. We can then show that (or equivalently ) is a companion for just as in Theorem 4.1 here. Conversely, from a companion pair we can show that 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 is essentially found in this paper, although stated only for the “edge-symmetric” case. In their language, a kernel is the double category of commutative squares in , and a functor which is the identity on is a thin structure on . In one direction, clearly has companions, and this property is preserved by any functor . In the other direction, sending any vertical arrow to its horizontal companion is easily checked to define a functor .
In particular, we conclude that up to isomorphism, there can be at most one functor which is the identity on objects.
A 2-congruence in a finitely complete 2-category is a homwise-discrete category in satisfying the equivalent conditions of Theorem .
Of course, the kernel of any object is a 2-congruence. More generally it is easy to see that the kernel of any morphism is also a 2-congruence.
The idea of a 2-fork is to characterize the structure that relates a morphism to its kernel . The kernel then becomes the universal 2-fork on , while the quotient of a 2-congruence is the couniversal 2-fork constructed from it.
A 2-fork in a 2-category consists of a 2-congruence , , , and a morphism , together with a 2-cell such that and such that
The comma square in the definition of the kernel of a morphism gives a canonical 2-fork
It is easy to see that any other 2-fork
factors through the kernel by an essentially unique functor that is the identity on .
If is a 2-fork, we say that it equips with an action by the 2-congruence . If also has an action by , say , a 2-cell is called an action 2-cell if . There is an evident category of morphisms equipped with actions.
A quotient for a 2-congruence in a 2-category is a 2-fork such that for any object , composition with defines an equivalence of categories
A quotient can also, of course, be defined as a suitable 2-categorical limit.
The quotient in any 2-congruence is eso.
If is ff, then the square we must show to be a pullback is
But this just says that an action of on is the same as an action of on which happens to factor through , and this follows directly from the assumption that is ff.
A 2-fork is called exact if is a quotient of and is a kernel of .
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.
The opposite of a homwise-discrete category is again a homwise-discrete category. However, the opposite of a 2-congruence in is a 2-congruence in , since 2-cell duals interchange fibrations and opfibrations. Likewise, passage to opposites takes 2-forks in to 2-forks in , and preserves and reflects kernels, quotients, and exactness.
A 2-category 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.
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.
In StreetCBS the last condition is replaced by
We now show that this follows from our definition. First we need:
(Street’s Lemma) Let be a finitely complete 2-category where esos are stable under pullback, let be eso, and let be a map. 1. If the induced morphism is ff, then is faithful. 1. If is an equivalence, then is ff.
First note that being ff means that if and are such that , then . Likewise, being an equivalence means that given any , there exists a unique such that .
We first show that is faithful under the first hypothesis. Suppose we have and with . Take the pullback
Then we have two 2-cells
such that the composites
are equal. By the hypothesis, implies . But is eso, since it is a pullback of the eso , so this implies . Thus, is faithful.
Now suppose the (stronger) second hypothesis, and form the pair of pullbacks:
Then , being a pullback of , is eso. We also have a commutative square
By assumption, is an equivalence. Since we have shown that is faithful, the bottom map is ff, so since the eso factors through it, it must be an equivalence as well. But this says precisely that is ff.
A 2-category is regular if and only if 1. it has finite limits, 2. esos are stable under pullback, 3. every morphism factors as where is ff and is eso, and 4. every eso is the quotient of its kernel.
First suppose is regular; we must show the last two conditions. Let be any morphism. By assumption, the kernel can be completed to an exact 2-fork . Since is the quotient of the 2-congruence , it is eso, and since comes with an action by , we have an induced map with . But since the 2-fork is exact, we also have , so by Street’s Lemma, is ff.
Now suppose that in the previous paragraph were already eso. Then since it factors through the ff , must be an equivalence; thus is equivalent to and hence is a quotient of its kernel.
Now suppose satisfies the conditions in the lemma. Let be any morphism; we must show that can be completed to an exact 2-fork. Factor where is ff and is eso. Since is ff, we have . But every eso is the quotient of its kernel, so the fork is exact.
In StreetCBS it is claimed that the final condition in Theorem follows from the other three, but there is a flaw in the proof.
In a regular 2-category , we call a ff with codomain a subobject of . We write for the preorder of subobjects of , as a full sub-2-category of the slice 2-category . Since is finitely complete and pullbacks preserve ffs, we have pullback functors for any .
If where is ff and is eso, we call the image of . Taking images defines a left adjoint to in any regular 2-category, and the Beck-Chevalley condition is satisfied for any pullback square, because esos are stable under pullback.
It is easy to check that if is regular, so are:
The slice 2-category does not, in general, inherit regularity, but we have:
If is regular, so are the fibrational slices and .
In general, the idea is that an -congruence in an -category , where , is an “internal -category” in . Of course, we only deal formally with the case , although we allow and to be of the form ; see n-prefix.
Let be a 2-congruence in a 2-category .
Note that in a 1-category,
Of course, a (0,1)-congruence in any 2-category is completely determined by any object .
Let be a morphism in . If is -truncated for , then is an -congruence. This means that:
In all these cases the converse is true if is regular and is eso.
The forward directions are fairly obvious; it is the converses which take work. Suppose first that is a (2,1)-congruence, and let be any 2-cell. Pulling back the eso along and gives and ; let be the pullback . Since is regular, is eso. By definition of kernels, the 2-cell corresponds to a map . But is a (2,1)-congruence, so composing this map with the “inverse” map gives another map , and thereby another 2-cell which is inverse to . Finally, since is eso, precomposing with it reflects invertibility, so must also be invertible. Thus is groupoidal.
Now suppose that is a (1,2)-congruence, and let be two parallel 2-cells. With notation as in the previous paragraph, the 2-cells and correspond to morphisms which become isomorphic in . But since is a (1,2)-congruence, this implies that the two maps are isomorphic, and hence . And since is eso, precomposing with it is faithful, so ; thus is posetal.
The discrete case follows by combining the posetal and groupoidal cases, so it remains to show that if is a (0,1)-congruence then is subterminal. We know it is discrete, so it suffices to show that given two we have a 2-cell . Continuing with the same notation, and letting be the induced maps with and , we have , and therefore the 2-cell defining the fork gives us a 2-cell and therefore . Now is the quotient of its kernel, so for this 2-cell to induce a 2-cell it suffices for it to be an action 2-cell for the actions of on and ; but this is automatic since we know to be posetal. Thus we have a 2-cell as desired, so is subterminal.
A regular 1-category is exact when every congruence has a kernel. The definition for 2-categories is analogous.
Let be directed (see n-prefix). A 2-category is -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.
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 is 2-exact, then by the classification of congruences, is (2,1)-exact, is (1,2)-exact, is 1-exact, and is (0,1)-exact.
If is -exact, then so is , 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.
A 2-category is called coherent if 1. it has finite limits, 1. finite jointly-eso families are stable under pullback, and 1. every finitary 2-polycongruence which is a kernel can be completed to an exact 2-polyfork.
Here a family is said to be jointly-eso if whenever is ff and every factors through (up to isomorphism), then is an equivalence.
Likewise, we have infinitary coherent 2-categories in which “finite” in the second two conditions is replaced by “small.”
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.
The following are proven just like their unary analogues in a regular 2-category.
(Street’s Lemma) In a finitely complete 2-category where finite jointly-eso families are stable under pullback, if is finite and jointly-eso and is such that the induced functor is an equivalence, then is ff.
A 2-category is coherent if and only if 1. it has finite limits, 1. finite jointly-eso families are stable under pullback, 1. every finite family factors as where is ff and is jointly-eso, and 1. 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 have finite (resp. small) unions that are preserved by pullback.
A coherent 2-category has a strict initial object; that is an initial object such that any morphism is an equivalence.
The empty 2-congruence is the kernel of the empty family (over any object), so it must have a quotient , which is clearly an initial object. The empty family over is jointly-eso, so for any the empty family over is also jointly-eso; but this clearly makes initial as well.
Two ffs and are said to be disjoint if the comma objects and are initial objects. If initial objects are strict, then this implies that the pullback is also initial, but it is strictly stronger already in .
In a coherent 2-category, if and are disjoint subobjects, then their union in is also their coproduct .
If and are disjoint subobjects of , then the kernel of is the disjoint union of and . Therefore, a quotient of it (which is a union of and in ) will be a coproduct of and .
A coproduct in a 2-category is disjoint if and are disjoint subobjects of . We say a coherent 2-category is positive if any two objects have a disjoint coproduct. By Lemma , 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:
A regular and extensive 2-category is coherent (and positive).
In the presence of finite coproducts, a family is jointly-eso iff is eso; thus regularity and universal coproducts imply that finite jointly-eso families are stable under pullback. And assuming extensivity, any 2-polycongruence gives rise to an ordinary 2-congruence . Likewise, 2-polyforks correspond to 2-forks , and the property of being a kernel or a quotient is preserved; thus regularity implies coherency.
If is coherent, then easily so are , , , , and . Moreover, we have:
If is a coherent 2-category, so are the fibrational slices and for any .
A coproduct in a 2-category is said to be disjoint if we have comma squares
The first two say that and are ff and the second two say that they are disjoint subobjects of .
A coproduct is said to be universal if for any morphism , the pullbacks
exist and exhibit as a coproduct .
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.
If is extensive, so is , obviously. Less obvious is:
If is extensive, so are , , and . In other words, if is extensive, so is its -category of -truncated objects for .
Since the three given categories are closed in under limits and strict initial objects, it suffices to show they are closed under coproducts. First suppose given two morphisms . Then decomposes , and decomposes . Then the inclusions also decompose each . Now if there exists a 2-cell , it induces a map from each to the comma object of and . Since coproducts are disjoint and initials are strict, this implies that . Therefore, we have a decomposition so that and , where and .
Now, by universality of the coproduct , it follows that 2-cells are determined uniquely by pairs of 2-cells and . Therefore, if and are groupoidal, any 2-cells and are invertible, and thus so is any 2-cell ; so is groupoidal. And if and are posetal, any parallel 2-cells and are equal, and thus so are any ; so is posetal. And of course the discrete case follows by combining these.
However, the (0,1)-category (= poset) of (-1)-truncated objects (= subterminal objects) does not inherit extensivity, and in fact posets are almost never extensive: the only disjoint coproduct is .
We also have:
If is extensive, so are the fibrational slices and for any .
Let be 2, (2,1), (1,2), or 1. That is, and is directed; see n-prefix.
An -pretopos is an -exact -category which is also extensive. An infinitary -pretopos is an -pretopos which is infinitary-extensive.
As remarked here, regularity plus extensivity implies coherency. Thus an -pretopos is, in particular, a coherent -category. Conversely, we have:
An -category is an -pretopos if and only if it is coherent and every (finitary) -polycongruence is a kernel.
is a 2-pretopos. Likewise, is a (2,1)-pretopos and 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 -pretopos for any .
Since no nontrivial (0,1)-categories are extensive, the definition as phrased above is not reasonable for . 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).
An -pretopos has coproducts and quotients of -congruences, which are an important class of colimits. However, it can fail to admit all finite colimits, for essentially the same reason as when : 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 does in fact have all finite colimits, but the 2-pretopos of finite categories (that is, finitely many objects and finitely many morphisms) does not have coinserters, coinverters, or coequifiers. (The category of finitely presented categories does have finite colimits, but fails to have finite limits.)
However, I conjecture that just as in the case , once an -pretopos is also countably-coherent, it does become finitely cocomplete. See colimits in an n-pretopos.
A 2-category is Heyting if it is coherent and each pullback functor has a right adjoint .
As in the 1-categorical case, this also ensures that each is a Heyting algebra and that each is a homomorphism of Heyting algebras. Moreover, the right adjoints satisfy the Beck-Chevalley condition for pullback squares, because the left adjoints do. This is just what is necessary for the internal interpretation of (finitary) first-order logic.
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.
Clearly if is Heyting, so are , , , , and (the Heyting algebra of subterminals).
Moreover, Heytingness is also preserved by fibrational slicing. First we show:
If is Heyting, then for any and any , is a coreflective sub-poset of .
As proven here, is a full sub-poset of . Moreover, it is easy to see that a ff is in precisely when
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
factors through , where is the action making into a fibration. Note that is alternately written as , where is the projection onto the first factor. Therefore, is in just when , or equivalently when .
We claim that coreflects into , and given the above, it suffices to verify that it is a comonad. First, let be the inclusion of identities; then and , so we have
This gives the counit of the comonad. The comultiplication is a little more involved. First note that we have a pullback square
where denotes projection onto the first two factors. Thus, by the Beck-Chevalley condition, and therefore
where is the “composition” morphism.
Let us write for , the object of composable arrows in , and write for the power of with the category
Let forget the “lonely” arrow, and let make the lonely arrow into the composite of the other two. Then , and moreover , where and are and applied to the non-lonely arrows. Thus, we have
as desired. (Here we have used another Beck-Chevalley condition to move past and , turning them into and and it into .)
If is Heyting, so is each fibrational slice and .
This follows from the adjoint lifting theorem for posets: for any in we have a commutative square
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.
We may naturally say that a coherent 2-category is Boolean if each is a Boolean algebra. As usual, this implies that is Heyting; we have .
Note that a subobject and its complement in 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 (though it holds in any (2,1)-category).
The core of a category is the maximal subcategory of that is a groupoid, consisting of all its objects and all isomorphisms between them. The core is not a functor on the 2-category , but it is a functor on the (2,1)-category of categories, functors, and natural isomorphisms. In fact, it is a coreflection of into .
In general, for any 2-category we write for its “homwise core:” the sub-2-category determined by all the objects and morphisms but only the iso 2-cells. Of course, is a (2,1)-category. Then is a full sub-2-category of , 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.
A core of an object in a regular 2-category is a morphism which is eso, pseudomonic, and where is groupoidal.
In a regular 2-category , any core is a coreflection of from into .
We must show that for any groupoidal , the functor
is an equivalence. Since is pseudomonic in , it is ff in , so this functor is full and faithful; thus it remains to show it is eso. Given any map , take the pullback
and let be the kernel of . Since the composite descends to , it comes equipped with an action by this kernel. However, since is groupoidal, is a (2,1)-congruence, so the 2-cell defining the action must be an isomorphism. Therefore, it must factor uniquely through the pseudomonic , so has an action as well; thus it descends to a map , as desired.
In particular, cores in a regular 2-category are unique up to unique equivalence. We write for the core of , when it exists.
An object of a (2,1)-exact 2-category has a core if and only if there is an eso where is groupoidal.
“Only if” is clear, so suppose that is eso and is groupoidal. Let be the pullback. Then is also groupoidal and is a (2,1)-congruence on , so by exactness it is the kernel of some eso . There is an evident induced map ; we claim that this is a core of .
Evidently is eso, since the eso factors through it. And since is a (2,1)-congruence, the classification of congruences implies that is groupoidal; thus it remains to show that is pseudomonic.
First suppose given . Pulling back along and gives esos and , whose pullback comes with an eso and two morphisms with and . Then any pair of 2-cells induce maps , since is the kernel . But if , then these two maps must be equal, since is also the kernel . Therefore, , and since is eso, ; thus is faithful.
On the other hand, again given , any isomorphism induces a map and therefore a 2-cell with . To show that descends to a 2-cell , we must verify that it is an action 2-cell for the actions of on and . But is an action 2-cell, since , and we now know that is faithful, so it reflects the axiom for an action 2-cell. Therefore, is full-on-isomorphisms, and hence pseudomonic.
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 has enough groupoids, then 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 . 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.
We also remark that cores, when they exist, “capture all the information about subobjects.”
If is a regular 2-category and is an object having a core , then is an equivalence.
It is a general fact in a regular 2-category that for any eso , is full (and faithful, which of course is automatic for a functor between posets). For if , then we have a square
in which is eso and is ff, hence we have over .
Thus, in our case, is full and faithful since is eso, so it suffices to show that for any ff we have in . But we have a commutative square
where the vertical arrows are ff and the bottom arrow is faithful and pseudomonic, from which it follows that is also faithful and pseudomonic. Since is eso by definition, is a core of , and since is a groupoid mapping to , it factors through , as desired.
If is a 2-category with finite limits, a successor algebra in is an object equipped with morphisms and . A morphism of successor algebras is a morphism with isomorphisms and . Likewise a 2-cell of successor algebras is a 2-cell commuting with the above isomorphisms in an obvious way.
Finally, a natural numbers object in is an initial object in the 2-category of successor algebras. This means that for any successor algebra there is a morphism of successor algebras, unique up to unique isomorphism. Clearly any NNO in is also an NNO, in the usual sense, in .
If 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:
This enables us to show the following, using the internal logic.
If is a positive Heyting coherent 2-category with an NNO , then is discrete.
First note that since and coproducts are disjoint, we have
Now consider the subobject described in the internal logic as determined by those for which the above sequents remain true when is replaced by . (This requires universal quantification over .) The above observation shows that . Suppose that , , and , . If then and is an isomorphism; otherwise ; but is ff, so we have and which are equal and isomorphisms; hence so are and . Thus, is closed under , so it is all of . Therefore, is discrete.
The 2-category 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 be the ordinal ; then there is a pushout
in which pulls back along the inclusion to
which is certainly not a pushout. Note that the same counterexample applies in .
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, is extensive), as are quotients of 2-congruences (since is regular), but these seem to be about it for pullback-stable colimits in .
However, there are a number of other useful exponentiability properties that do hold when .
Fibrations and opfibrations are exponentiable. That is, if is an (op)fibration, then exponentials exist in the slice 2-category . Equivalently, has a right adjoint . (Fibrations and opfibrations are not the only exponentiable morphisms in , but they are some of the most important, commonly encountered, and easily characterized ones.)
If is an opfibration and is a fibration, then the exponential in is a fibration, and dually.
For any , the functor has a right adjoint , and likewise for .
For any , the functors and have right adjoints .
The 2-categories and are all cartesian closed.
itself is cartesian closed.
The 2-categories and are all locally cartesian closed.
Note that and are not the same even when both exist, and likewise the exponentials in are not the same as the exponentials in 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:
A 2-category with finite limits is said to have exponentials if all fibrations and opfibrations in 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.
We begin with a couple of easy observations.
If either fibrations or opfibrations are exponentiable in , then is cartesian closed.
Of course, is cartesian closed just when every morphism is exponentiable; but every such morphism is both a fibration and an opfibration.
If is an opfibration and is a fibration, then the exponential in (if it exists) is a fibration, and dually.
We say briefly how to construct an action morphism
Of course, by adjointness it suffices to construct a morphism
over . Now the left-hand side is a limit of the diagram
We first map it via a diagonal to the limit of
then use the covariant action of on to map to the limit of
then the evaluation to get to the limit of
and finally the contravariant action of on to get to
It is then straightforward to check that this action makes into a fibration.
The key observation for many of the proofs below is the following.
If has exponentials, then for any , and are comonadic, as well as monadic, over .
The monad on whose category of algebras is takes to , or equivalently where are the two projections. But is an opfibration, so has a right adjoint . 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.
If has exponentials, then and inherit any colimits possessed by .
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.
Given a commutative square
of functors between 2-categories, if and are monadic, has reflexive codescent objects, and has a left adjoint, then also has a left adjoint. Dually, if and are comonadic, has reflexive descent objects, and has a right adjoint, then also has a right adjoint.
The 1-categorical version of this, referring to reflexive (co)equalizers, is well-known; see for instance
The idea is the same as that in Beck’s (co)monadicity theorem: we express any object of as a reflexive coequalizer of free algebras, then apply the left adjoint of to obtain a reflexive pair of free algebras in and take its coequalizer. The 2-categorical version is analogous, using the ideas of a 2-categorical monadicity theorem as found, for example, in
The dual is, of course, obvious.
Using comonadicity, we can show that certain exponentials are stable under slicing. First we observe:
If is a fibration, then is monadic over . If additionally has exponentials, then is also comonadic over .
The first statement is an instance of a general fact: if is a monad on a (2-)category and is a -algebra, then there is an induced monad on whose (2-)category of algebras is , defined by taking to the composite .
The second statement is also an instance of a general fact: if such a has a right adjoint , then also has a right adjoint defined to take to the pullback
Here the lower map is the adjunct of the algebra structure map .
If has exponentials, then a morphism in or is exponentiable if its underlying morphism in is so. In particular, if has exponentials, then for any , fibrations are exponentiable in and opfibrations are exponentiable in .
Suppose that is a morphism in and that is exponentiable in . Then we have a commutative square
in which the vertical functors are comonadic by Lemma , and the bottom functor has a right adjoint since is exponentiable in . Therefore, by Proposition , the top functor has a right adjoint as well. The second statement follows because the underlying morphism in of any fibration in is a fibration in , and dually (see the theorems on iterated fibrations).
If has exponentials and a duality involution, then and also have exponentials for any .
After Proposition , it remains to show that opfibrations are exponentiable in (and dually, fibrations are exponentiable in ). Note that an opfibration in will not, in general, be an opfibration in . But with a duality involution we have , and opfibrations are exponentiable in , hence also in .
We say that a 2-category has local exponentials if has exponentials and each 2-category and 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
Since duality involutions are stable under fibrational slicing, Corollary implies that if 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).
If has exponentials, then the 2-categories and are all cartesian closed.
If has exponentials, then the categories and are all locally cartesian closed.
Since right adjoints preserve discrete objects, Corollary implies that and are cartesian closed for any . Now, given a discrete fibration , we have by the theorem on iterated fibrations, and so . Thus, since is cartesian closed, so is , and thus is locally cartesian closed.
We now turn to the existence of left and right adjoints to pullback functors. So far what we know is
Note that even if is a fibration, so that maps to , it will not in general be a left adjoint to . However, if is a discrete fibration, then is left adjoint to , since is a full sub-2-category of .
We now consider how to construct left adjoints for non-discrete fibrations.
If has exponentials and reflexive codescent objects, then each pullback functor and has a left adjoint .
Because of the existence of , by Proposition it suffices to show that and always have reflexive codescent objects; but this follows from Corollary .
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 , 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).
We now consider the existence of right adjoints to pullback functors between fibrational slices.
If has exponentials, then and have right adjoints for any .
If is exponentiable in , this follows directly from Lemma and Proposition . In particular, this applies when is a fibration or opfibration.
Now let be any morphism, and consider the comma square:
Suppose first that all the left adjoints exist for opfibrational slices and satisfy the Beck-Chevalley condition for comma squares. Then this comma square gives us an equivalence , so that has the right adjoint .
We now show that regardless of the overall existence of left adjoints, the particular value exists for any and is given by . This clearly suffices to prove the result.
According to the proof of Proposition , should be given by the codescent object of
where
Now we have a map
the first map is a Beck-Chevalley morphism, and the second comes from the fact that is an opfibration. We claim that is actually a codescent object of the above diagram, and in fact it is a split codescent object. Recall from
that a split codescent object is a diagram
with isomorphisms , , , , , and satisfying certain axioms. In this situation, is necessarily the codescent object of the diagram composed of .
Tracing through the definitions above, we see that our is the limit of the span weighted by
Likewise, is the limit of weighted by
and is the limit by an evident more complicated weight. Finally, itself is the limit of the same span weighted by
The morphism is induced by the action of on the opfibration , applied twice. The morphism is induced by the inclusion of the second arrow in a composable pair and the action of on applied once. The morphism is induced by the composition of a composable pair. We define the splitting 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.
If has exponentials, then and have right adjoints for any .
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.
One further observation:
If has exponentials, then each category is enriched over the cartesian closed category .
We define the hom-object to be , where is the exponential in and
is the right adjoint to . A composition map is obtained by adjointness in the usual way. We also have
so the underlying ordinary category of this -enriched category is the ordinary category .
In fact, more is true: I believe can be made into a locally internal category, or equivalently a locally small fibration, over . Its fiber over a discrete object is the category . This follows by localizing the previous lemma in the slices ; one also has to check that a suitable Beck-Chevalley condition is satisfied by the right adjoints .
An important structure possessed by the 2-category is the duality involution . Here we consider what the important properties of this involution are that should be generalized to other 2-categories.
The most obvious property of is that it is coherently self-inverse. To state this formally, let be the walking isomorphism , considered as a 3-category with only identity 2-cells and 3-cells. Thus, a (pseudo) functor from to any 3-category can be considered an “internal adjoint (bi)equivalence in .” If is a 3-category, let denote the 3-cell dual of ; note that and that is a functor . Finally, let be the evident involution that switches and .
A 2-contravariant involution (hereafter merely an involution) on a 2-category is functor such that and the square
commutes (on the nose).
We write (or equivalently ) for the functor ; the rest of the data of simply says that in a coherent way.
Any (2,1)-category admits a canonical involution that is the identity on objects and morphisms and sends each 2-cell to its inverse.
Let be a 2-category equipped with an involution and let . Then has a canonical induced involution defined by
Conversely, if is Cauchy-complete, then can be identified with the full subcategory of indecomposable projectives in , and thus an involution on induces an involution on .
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.
For any 2-category , the 2-category of involutions on , if nonempty, is a torsor for the 3-group of (covariant) automorphisms of .
Easy.
In particular, any automorphism of a (2,1)-category induces an involution on .
As observed by WeberYS2T, experience suggests that the most important additional property of the involution on is that fibrations over can be identified with opfibrations over , since both are equivalent to functors . So it is reasonable to consider, together with an involution on a 2-category , a family of equivalences .
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.
A duality involution on a 2-category is an involution together with the following data.
which are natural in (that is, is a natural equivalence between functors ),
in which all the displayed maps are fibrations, an invertible modification between the two composites
and
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 , by naturality of we have , and thus . Also, , so again by naturality . Thus , 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 is a 2-contravariant involution, we automatically have equivalences (these are the vertical maps in the displayed square). In , this equivalence corresponds to composing a functor with as well as reinterpreting it as an opfibration. Commutation of opposites then says that this operation commutes with .
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 . We will see others below.
If is a (2,1)-category, then its canonical involution extends to a canonical duality involution, since .
If is a (2,1)-category, then the canonical involution on extends in a natural way to a duality involution. This does not seem to be the case if is merely a 2-category equipped with an involution.
The 3-group also acts on the 2-category of duality involutions on ; 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 and the definition of WeberYS2T are threefold.
Of course, since any equivalence of 2-categories preserves discrete objects, our definition implies an equivalence . More surprisingly, it turns out that the seemingly stronger two-sided version is a consequence of our definition.
If is equipped with a duality involution, then we have natural equivalences .
We first construct an equivalence . Note that since is the identity, naturality implies that . Also, since is an equivalence, and products in are the same as products in , we have . Now we have the composite equivalence (using the theorem on iterated fibrations):
Note that there is also another equivalence
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:
This gives our desired equivalence.
Note, though, that this proof crucially requires that the duality involution come with an equivalence , and not merely .
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.
Any duality involution on induces a duality involution on each fibrational slice and .
We define to be the composite
To show that is an involution, we verify
Here we use commutation of opposites in to commute past . We now define
to be the composite
It is easy to see that , and to construct the pullback-commutation equivalence. Finally, we construct commutation of opposites in as the composite
The case of is dual.
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 fix groupoidal objects, as is clearly the case for the involution of and the “canonical” involutions of (2,1)-truncated 2-presheaf 2-toposes.
Note that any involution takes groupoidal objects to groupoidal objects.
An involution on fixes groupoids it it restricts to the canonical involution on , i.e. if coherently whenever is groupoidal.
If is a regular -category having enough groupoids, then it admits, up to equivalence, at most one involution that fixes groupoids. If is also -exact, then it admits exactly one such involution.
Suppose that is an involution on that fixes groupoids. Then for any and any groupoidal , we have
Now given as well, with an eso where is groupoidal, any morphism is determined by a map with an action by . But is also groupoidal, so morphisms are completely determined by morphisms to out of groupoidal objects. Thus, by the Yoneda lemma, any two values of must be canonically isomorphic.
Now suppose is exact, and let be an eso where is groupoidal. Then its kernel is also groupoidal, and so is a homwise-discrete category in . Thus we can consider its opposite, which is also a homwise-discrete category in . 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 , this extra condition is automatic, so this opposite of is also a 2-congruence in (and, in fact, an -congruence when is an -category). Thus, since is -exact, this opposite has a quotient, which we call . It is straightforward to verify that this defines an involution on that fixes groupoids.
Of course, the only interesting values of 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 is -exact, the functor ought to be a 3-sheaf? (a 2-stack). This means that if is an eso with groupoidal, then can be reconstructed from and with descent data. Similarly, should also be a 3-sheaf, and so can be recovered from and with “op-descent data.” But since is groupoidal, , and likewise for . Therefore, descent data for over , which determines an object of , is the same as op-descent data for the opposite of over , which determines an object of . This gives the equivalence .
Alternately, there is also a stronger theorem that if 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 (more precisely, it is the 2-exact completion of ). 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.
Now, since a duality involution on extends to a duality involution on and , it is natural to strengthen the notion of groupoid-fixing so that it carries over to fibrational slices. We write and similarly .
A duality involution on fixes groupoids locally if we have a equivalence modification between and the composite .
The latter equivalence is the canonical involution on the (2,1)-category . Taking , together with the second condition in the definition of a duality involution, this implies that fixes groupoids in the previous sense. Moreover, we have:
If is a duality involution that fixes groupoids locally, then the induced duality involutions on and also fix groupoids locally.
For a fibration , on we have and , so the equivalence between and in induces one between and in .
Now, suppose that is a duality involution that fixes groupoids locally. Then for any and , the pullback-commutation datum shows that the composite equivalence
derived from Theorem is equivalent to . But if we restrict to groupoidal fibrations, then
is equivalent to . Together with commutation of opposites, this implies that the canonical equivalence
is, up to equivalence, simply given by . In particular, since preserves powers, the canonical equivalence
takes to . In the 2-internal logic, this corresponds to the statement that “,” which is certainly an expected part of the behavior of opposite categories. Of course, for this it suffices that fix discretes locally, which has the evident definition.
Another natural requirement is that when is groupoidal, should be equivalent to the composite
Note that this includes the second datum in the definition of a duality involution as a special case, since is groupoidal. There seems no reason for this condition to be stable under slicing, but it could be stabilized.
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 -topos is an -category that is equivalent to the -category of -sheaves on some -site (for ); see truncated 2-topos.
The 2-Giraud theorem due to StreetCBS characterizes Grothendieck -toposes as the infinitary n-pretoposes having a small eso-generating set of objects.
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 is a Grothendieck 2-topos, so is . In the case of 2-presheaves, we can identify this as:
since we have . 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.
A coverage on a 2-category consists of, for each object , a collection of families of morphisms with codomain , called covering families, such that
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.
If is a regular 2-category, then the collection of all singleton families , where is eso, forms a coverage called the regular coverage.
Likewise, if is a coherent 2-category, the collection of all finite jointly-eso families forms a coverage called the coherent coverage.
On , the canonical coverage consists of all families that are jointly essentially surjective on objects.
Let be a 2-site having finite limits (for convenience). For a covering family we have the comma objects
We also have the double comma objects with projections , , and .
Now, a functor is called a 2-presheaf. It is 1-separated if
It is 2-separated if it is 1-separated and
It is a 2-sheaf if it is 2-separated and
there exists an object and isomorphisms such that for all the following square commutes:
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 and need not be invertible.
Note, though, they must be invertible as soon as is (2,1)-site: by definition and since an inverse is provided by , where is the symmetry equivalence.
If lacks finite limits, then in the definitions of “2-separated” and “2-sheaf” instead of the comma objects , we need to use arbitrary objects equipped with maps , , and a 2-cell . We leave the precise definition to the reader.
A 2-site is said to be subcanonical if for any , the representable functor is a 2-sheaf. When 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 of 2-sheaves on a small 2-site is, by definition, a Grothendieck 2-topos.
A pre-Grothendieck coverage on a 2-category is a coverage satisfying the following additional conditions:
If is an equivalence, then the one-element family is a covering family.
If is a covering family and for each , so is , then is also a covering family.
This is the 2-categorical version of a Grothendieck pretopology.
Now, a sieve on an object is defined to be a functor with a transformation which is objectwise fully faithful (equivalently, it is ff in ). Every family generates a sieve by defining to be the full subcategory of on those such that for some and some . The following observation is due to StreetCBS.
A 2-presheaf is a 2-sheaf for a covering family if and only if
is an equivalence, where is the sieve on generated by .
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 to consist of, for each object , a collection of sieves on called covering sieves, such that
If is a covering sieve on and is any morphism, then is a covering sieve on .
For each the sieve consisting of all morphisms into (the sieve generated by the singleton family ) is a covering sieve.
If is a covering sieve on and is an arbitrary sieve on such that for each in , is a covering sieve on , then is also a covering sieve on .
Here if is a sieve on and is a morphism, denotes the sieve on consisting of all morphisms into such that factors, up to isomorphism, through some morphism in .
As in the 1-categorical case, one can then show that every coverage generates a unique Grothendieck coverage having the same 2-sheaves.
Let be a Grothendieck 2-topos. We say that is -truncated if it has a small eso-generator consisting of -truncated objects. It is easy to see that if a coproduct of -truncated objects is -truncated (as is the case for all ), then this is equivalent to saying that has enough -truncated objects (i.e. every object admits an eso from an -truncated one). In particular:
By the 2-Giraud theorem, small eso-generating sets of objects correspond to small 2-sites of definition for . Thus, if we define an -site to be a 2-site which is an -category (where as usual), we have:
A Grothendieck 2-topos is -truncated iff it is equivalent to the 2-category of 2-sheaves on some -site.
Note that a 1-site is the same as the usual notion of site, and a -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:
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.
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 localic.
If 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 is a sublocale of the terminal locale . Thus, just as (-1)-categories are subsets of , (-1)-toposes are sublocales of . If has classical logic, this implies that either or ; and hence that either or . However, constructively there may be many other sublocales of .
It would be nice if the only (-2)-truncated Grothendieck 2-topos were . However, I don’t see a way to make this happen except by fiat.
Now, if is an -site, it is also reasonable to consider -sheaves on , by which we mean 2-sheaves taking values in -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 -topos to be an -category equivalent to the -category of -sheaves on an -site. The case gives classical Grothendieck toposes; the case gives locales. Note the distinction between a Grothendieck -topos and an -truncated Grothendieck 2-topos. The relationship is that
This relationship is completely analogous to the classical relationship between locales and localic toposes. In fact, if denotes the -category of Grothendieck -toposes (that is, -categories of -sheaves on an -site), we have inclusions
where the inclusion from to is given by taking the -category of -sheaves for the canonical coverage. (See 2-geometric morphism for the morphisms in these categories.)
If and are Grothendieck n-toposes, an -geometric morphism consists of an adjoint pair , where is the direct image and is the inverse image, such that preserves finite limits (in the -categorical sense).
When this is, of course, the usual definition. When this reduces to a continuous map between locales.
In general, we expect that Grothendieck -toposes satisfy an -categorical version of the adjoint functor theorem, so that any functor that preserves finite limits and small colimits is the inverse image of some -geometric morphism.
We define transformations and modifications between -geometric morphisms to be transformations and modifications between their inverse image functors. We then have an -category of Grothendieck -toposes and -geometric morphisms.
In a suitably exact 2-category, we can construct truncations as quotients of suitable congruences.
This case is easy and just like for 1-categories.
In any regular 2-category the inclusion of the subterminal objects has a left adjoint called the support or (-1)-truncation.
Define the support of an object to be the image of the unique morphism . That, is is an eso-ff factorization. Since is ff, is subterminal, and since esos are orthogonal to ffs, it is a reflection into .
Perhaps surprisingly, the next easiest case is the posetal reflection.
In any (1,2)-exact 2-category the inclusion of the posetal objects has a left adjoint called the (0,1)-truncation.
Given , define to be the (ff) image of . Since esos are stable under pullback, is a homwise-discrete category, and it clearly has a functor from , so it is a (1,2)-congruence. Let be its quotient. By the classification of congruences, is posetal. And if we have any where is posetal, then we have an induced functor . But is posetal, so is a (1,2)-congruence, and thus factors through a functor . This then equips with an action by the (1,2)-congruence , so that it descends to a map . It is easy to check that 2-cells also descend, so is a reflection of into .
This is actually a special case of the (eso+full,faithful) factorization system?, since an object is posetal iff is faithful. The proof is also an evident specialization of that.
The discrete reflection, on the other hand, requires some additional structure.
In any 1-exact and countably-coherent 2-category , the inclusion of the discrete objects has a left adjoint called the 0-truncation or discretization.
Given , define to be the equivalence relation generated by the image of ; this can be constructed with countable unions in the usual way. Then is a 1-congruence, and as in the posetal case we can show that its quotient is a discrete reflection of .
There are other sufficient conditions on 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.
The groupoid reflection is the hardest and also requires infinitary structure. Note that the 2-pretopos does not admit groupoid reflections (the groupoid reflection of the “walking parallel pair of arrows” is ).
In any (2,1)-exact and countably-extensive 2-category , the inclusion of the groupoidal objects has a left adjoint called the (1,0)-truncation.
In Cat there is a factorization system where is the class of initial functors and is the class of discrete opfibrations; see
We can construct an analogous factorization system in any 1-exact and countably-coherent 2-category.
A morphism in a 2-category is initial if it is left orthogonal to discrete opfibrations. That is, whenever is a discrete opfibration, the following square is a pullback in :
Every morphism in a 1-exact countably-coherent 2-category (in particular, in an -pretopos for ) factors, up to isomorphism, as an initial morphism followed by a discrete opfibration.
By the 2-categorical analogue of a standard theorem about factorization systems in 1-categories, it suffices to show that
The first point is true in any 2-category. For the second, we factor the inclusion as
and observe that both forgetful functors have left adjoints. The left adjoint to is discretization in the 1-exact and countably-coherent 2-category . The left adjoint to constructs the “free opfibration” on a functor , which is given by .
In any 1-exact countably-coherent 2-category, (initial, discrete opfibration) is a (2-categorical) factorization system.
In any 1-exact countably-coherent 2-category, each pullback functor has a left adjoint .
is given by composing with , then factoring into an initial morphism followed by a discrete opfibration.
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.
The appropriate Beck-Chevalley condition for the adjunctions 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 as the functors for which each comma category , for , is nonempty and connected.
For the rest of this page we make the standing assumption that is a 1-exact and countably-coherent 2-category.
A morphism in is initial iff the following are internally valid:
where for each , expresses “there is a zigzag of length connecting and over .”
Thus, for instance, we have
and so on.
will be initial iff the discrete-opfibration part of its factorization is an equivalence. By construction, this factorization is the discrete reflection of in , which is constructed as the quotient of the equivalence relation generated by (the power taken in ). Therefore, this discrete reflection will be the terminal object iff
It is fairly evident that is eso iff the first displayed sequent holds in . For the second, note that the kernel of in (or equivalently, in ) is just the pullback , since is discrete as an object of . By definition of , this pullback can be computed as the lax limit
and therefore it is precisely the context of the second displayed sequent. Since is the equivalence relation generated by , it is necessarily contained in this kernel, so it suffices to show the converse implication. But is defined as the symmetric transitive closure of the image of , which makes it essentially a countable union of “zigzags” from , and this translates directly into the conclusion of the second sequent.
Initial morphisms in are stable under transfer across comma squares, in the sense that if
is a comma square with initial, then is also initial.
Given the characterization of initial morphisms in Lemma , we can simply observe that the usual proof of this fact in takes place entirely in countably-coherent logic.
The adjunctions for discrete opfibrations in satisfy the Beck-Chevalley condition for comma squares. That is, if
is a comma square, then the canonical transformation between functors 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 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 between functors .
Given a discrete opfibration , let be the (initial,discrete-opfibration) factorization of the composite . 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 , and the map 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 , its left-hand morphism is initial. But then the left-hand composite is an (initial, discrete-opfibration) factorization of , and hence it exhibits the desired equivalence .
Passing to 2-cell duals, we obtain:
For a comma square as above, the canonical transformation between functors is an equivalence.
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.
Recall that a morphism is said to be faithful if is faithful for any .
A morphism in a 2-category is eso+full if for any faithful , the following square is a pullback:
A morphism is said to be full if we have where is ff and is eso+full.
Luckily, the terminology is consistent:
In any 2-category, 1. is eso+full if and only if it is both eso and full. 1. is ff if and only if it is both faithful and full.
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 is eso and where is eso+full and is ff, then is an equivalence, and hence , like , 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 is faithful and we have where is eso+full and is ff, then is also faithful, and hence an equivalence; thus , like , is ff.
Any eso+full morphism is co-ff.
Let be eso+full; we want to show that is ff. It is faithful since is eso, so suppose that and that ; we want to show for some . Let with be the inserter of . Then we have a such that and (modulo this isomorphism) . But since , being an inserter, is faithful, and is eso+full, we have with and therefore ; thus is our desired 2-cell.
If is a 2-congruence such that is eso, then its quotient (if it has one) is eso+full.
Suppose that is faithful and that ; we want to show there is a with and (the rest follows by standard arguments). Since comes with an action by , it suffices to lift this action to itself, and since 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:
which exists since is eso (by assumption) and is ff (since is faithful).
In a regular 2-category, if is a map such that is eso, then is full.
The (eso,ff) factorization of is constructed by taking the quotient of . But by assumption, this kernel has the property of Lemma , so the eso part of the (eso,ff) factorization of is eso+full. Hence is full, by definition.
For comparison, recall that
I do not know whether the converse of Lemma is true in general, but it is at least true in an exact 2-category.
Let be an -exact -category, where is 2, (2,1), (1,2), or 1. Then: 1. Every morphism factors as where is eso+full and is faithful. Thus, (eso+full, faithful) is a factorization system on . 1. A morphism is full iff is eso. 1. Therefore, is eso+full iff it is the quotient of a 2-congruence such that is eso.
Of course, the cases and are fairly trivial, since in those cases every morphism in an -category is faithful and thus the only eso+full morphisms are the equivalences. However, we include them for completeness.
For the first statement, let be any morphism, and factor as an eso followed by a ff to get . Then inherits the structure of a 2-congruence, which is an -congruence since is. Since is -exact, this -congruence has a quotient , which is eso+full by Lemma , and clearly factors through as . Finally, since is ff by definition, Street's Lemma implies that is faithful.
The “if” direction of the second statement is Lemma . Conversely, if where is ff and is eso+full, then must be obtained, up to equivalence, as the quotient of the -congruence constructed above, for which is eso. But since is ff, we have , so is eso as desired.
One direction of the third statement is Lemma . For the other, if is eso+full, then by the second statement is eso, and because is eso it is the quotient of its kernel, namely .
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 , which is not exact.
In a (2,1)-exact (2,1)-category, eso+full morphisms are stable under pullback, and therefore so are full ones.
If is eso+full, then it is the quotient of its kernel, which in a (2,1)-category is . And since is eso+full, by Theorem , is eso. If
is a pullback square, then the kernel is also the pullback of along . Thus, by properties of pullback squares, is a pullback of , and hence also eso. But , being eso (as a pullback of ), is also the quotient of its kernel, so by Lemma is eso+full. The second statement follows since ffs are certainly stable under pullback.
Let be an -exact -category. Then: 1. Full morphisms are stable under composition. 1. A morphism is full iff it is (isomorphic to) a composite of eso+full and ff morphisms. 1. If is full and is eso, then is full.
Given and , we have two pullback squares
Thus, if and are full, so that and are eso, then is also eso, hence so is ; thus is full. This proves the first statement, from which the second follows. For the third, if is full and is eso, then is eso, and so is since it is a pullback of . Thus the composite is eso, and since it factors through , it follows that is also eso; hence is full.
A morphism in a 2-category is called ff and retract-closed or rff if is fully faithful and closed under retracts for all . Explicitly this means that (in addition to being ff) if is a retract of for some , then for some .
A morphism is called Cauchy surjective or cso if it is left orthogonal to all rffs; that is, if
is a pullback whenever is rff.
Since rffs are stable under pullback, is cso if and only if whenever it factors through an rff , then 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 , the Cauchy surjective functors are those for which every object of is a retract of an object of .
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 is Cauchy surjective.
In , (cso,rff) is a factorization system. We now show that the same is true in any regular 2-category.
Given , let be its retractor. This is a 2-categorical finite limit which comes with projections and and 2-cells and such that , and which is universal with these properties.
In any 2-category, if is eso, then is Cauchy surjective.
Suppose that is eso and let be such that and is rff; we want to show is an equivalence. But since is rff and is a retract of , it follows that factors through ; whence is an equivalence since is eso.
Now suppose that is regular, and for any , let be an (eso,ff) factorization of . Since is a retract of , there is a canonical with and .
In a regular 2-category, if is ff and (hence ), then is rff.
Suppose is ff and , and let and be such that is a retract of . Then and for some . Then we have with . But since in , we have a with as well; hence is rff.
In a regular 2-category , 1. Every morphism factors as a Cauchy surjective morphism followed by an rff. 1. Therefore, (cso,rff) is a factorization system on . 1. A morphism is cso if and only if is eso. 1. Likewise, is rff if and only if it is ff and .
Given any , let , , and be as above, and define . Then . Is easy to check that ; thus is eso, so by Lemma is Cauchy surjective.
Now let be the retractor of , with , , and corresponding factorization . Let
be a pullback. Then , like , is eso, and thus so is . Now is a retract of , and is a retract of , so is a retract of . Therefore, is also a retract of , so there is a morphism with (and ). Now in the square
is ff and is eso, so we have in ; thus by Lemma is rff.
Therefore, with we have factored as a cso followed by an rff; this shows the first two statements. Moreover, satisfies the condition of Lemma , so if is cso and hence equivalent to , so does it. Likewise, satisfies the condition of Lemma , so if is rff and hence equivalent to , so does it.
From the characterization of csos and rffs in Theorem , we can conclude that csos and rffs have the expected descriptions in the internal logic.
In a regular 2-category, a morphism is Cauchy surjective if and only if the following sequent is valid in the internal logic:
The context is easily seen to be precisely .
In a regular 2-category, a morphism is rff if and only if it is ff and the following sequent is valid in the internal logic:
The validity of this sequent says that the pullback of along is eso. But since both and factor through the ff , this pullback is equivalent to the pullback of along . Since is eso, this pullback being eso is equivalent to being eso. And since is ff, so is ; thus this is equivalent to being an equivalence.
An -pretopos has coproducts and quotients of -congruences, which are important classes of colimits. From these we can construct some other colimits, such as the following.
A 2-pretopos admits copowers with any finite category.
If is a finite category and is an object, we build a finite 2-polycongruence with one copy of indexed by each object , and with the hom-object from to being . It is easy to check that a quotient of this congruence is a copower .
However, an -pretopos can fail to admit all finite colimits, for essentially the same reason as when : 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 does in fact have all finite colimits, but the 2-pretopos of finite categories does not have coinserters or coinverters. (It does have coequifiers, for the same reason that has coequalizers). The category 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 -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 “-pretopos” you meant “-pretopos with a NNO?” In my limited experience “-pretopos” means “locally cartesian closed pretopos” which certainly includes all toposes.
-Mike
Sorry, I removed the wrong letter from ‘--pretopos’. I meant a -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 s to characters that I can’t type?
-Mike
Sorry, I started to fix the ‘Π’s (and ‘’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, ‘’ (also ‘’), 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.
A countably-extensive -pretopos has all countable colimits.
It is well-known that in a 1-pretopos,
For a similar statement in an -pretopos for , 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:”
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 , 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.”
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 in a 2-category is the equifier of and . By an involution we mean an (invertible) 2-cell that is its own inverse.
Let be ff with groupoidal, and consider first the (2,1)-congruence given by , where one copy of gives the identities, and the composition treats the other copy of as an involution. Its quotient is the copower of by the “walking involution.”
Now consider the following equivalence relation on in . We have
and we define the relation to be given by
Since is a 1-pretopos, this relation has a quotient, say . It is easy to verify that is then a (2,1)-congruence on with . (This depends on being groupoidal; otherwise it would be a homwise-discrete category but not necessarily a congruence.) Let be the quotient in of this (2,1)-congruence. Then we have a 2-fork such that and is an involution of .
We claim that is an identifier of . By construction of , we have , so since is ff, it suffices to show that for any with , factors through . But since with is the kernel of , the assumption implies that in fact . If we write for the two inclusions, this means that and become equal in , and therefore factor through the kernel pair of , namely . But this is evidently tantamount to saying that factors through .
In a (2,1)-pretopos, 1. every ff is an equifier, 1. every cofaithful ff is an equivalence, and 1. every cofaithful morphism is eso.
Theorem shows the first statement. Then any ff is an equifier of , so in particular ; but if is also cofaithful, this implies , and thus their equifier is an equivalence. Finally, if is just cofaithful, we factor it as where is ff and is eso; but then is also cofaithful, hence an equivalence, and so , like , is eso.
In a (1,2)-exact positive coherent 2-category, every ff with posetal codomain is an inverter.
Let be ff, and consider the 2-congruence on defined as follows. We have
(adding subscripts to distinguish the two copies of ) and the congruence is given by
Here is defined to be the ff image of the “composition” morphism ; in other words it is “the object of arrows in which factor through some element of .” The composition is easy to define making this into a 2-congruence, and if is posetal, then it is a (1,2)-congruence.
Let be the quotient of this congruence. Analogously to the proof of Theorem , the fork defining this quotient gives a 2-cell such that is an isomorphism. Thus, to show that is the inverter of , it suffices to show that for any with invertible, factors through . Now is induced by the fork defining together with the composite . If is invertible, then its inverse is given by some map , which must lie over the diagonal .
Now, pulling back the eso along we obtain an eso with a morphism such that the identity 2-cell of is the composite of 2-cells ; in other words, is a retract of . But since is posetal, this means , and then the fact that is eso implies that factors through , as desired.
In a (1,2)-pretopos, 1. every ff is an inverter, 1. every liberal ff is an equivalence, and 1. every liberal morphism is eso.
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.
In a 2-pretopos, 1. every rff is an inverter, 1. every liberal rff is an equivalence, and 1. every liberal morphism is Cauchy surjective.
In particular, every liberal morphism is cofaithful.
The first statement is proven exactly like Theorem , except that at the last step we use the assumption that is retract-closed rather than the assumption that 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
and faithfully co-conservational if moreover
Here a strong conservative morphism is one that is right orthogonal to all liberals. Theorem 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 . And we have also seen that since every liberal is cso, it is cofaithful.
However, even fails the final condition, as shown in (CJSV, Prop. 3.4). This can be remedied by passing to the 2-category of Cauchy-complete categories. I do not yet know whether a similar construction is possible in any 2-pretopos.
Recall that there is a 2-category of homwise-discrete categories in any finitely complete 2-category . We write for its full sub-2-category spanned by the -congruences (always we take 2, (2,1), (1,2), or 1). Recall that there is a functor sending each object to its kernel; if is an -category then the image of is contained in .
Suppose that has finite limits. Then:
It suffices to deal with finite products, inserters, and equifiers. Evidently is a terminal object. If and are homwise-discrete categories, define and ; it is easy to check that then is a homwise-discrete category that is the product in . Since , and products preserve ffs, we see that is an -congruence if and are and that preserves products.
For inserters, let be functors in , define by the pullback
and define by the pullback
where is the “object of commutative squares in .” Then is a homwise-discrete category and is an inserter of . Also, is an -congruence if is, and preserves inserters.
Finally, for equifiers, suppose we have functors and 2-cells in , represented by morphisms such that . Let be the universal morphism equipped with an isomorphism such that is the given isomorphism (this is a finite limit in .) Note that since is discrete, is ff. Now let ; then is a homwise-discrete category and is an equifier of and in . Also is an -congruence if is, and preserves equifiers.
For any morphism in , is the functor that consists of and . A transformation between and is a morphism whose composites are and ; but this is just a transformation in . Thus, 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:
If is an -category with finite limits, then is regular.
It is easy to see that a functor between -congruences is ff in iff the square
is a pullback in .
We claim that if is a functor such that is split (that is, for some ), then is eso in . For if for some ff as above, then we have with , and so the fact that is a pullback induces a functor with and . But this implies is an equivalence; thus is eso.
Moreover, if is split, then the same is true for any pullback of . For the pullback of along some is given by a where ; here is the “object of isomorphisms” in . What matters is that the projection has a splitting given by combining the splitting of with the “identities” morphism .
Now suppose that is any functor in . It is easy to see that if we define and let be the pullback
then where and are the obvious functors. Moreover, clearly is ff, and satisfies the condition above, so any pullback of it is eso. It follows that if itself were eso, then it would be equivalent to , and thus any pullback of it would also be eso; hence esos are stable under pullback.
Since is ff, the kernel of is the same as the kernel of , so to prove regular it remains only to show that is a quotient of that kernel. If denotes , then is the comma object and thus we can calculate
Therefore, if is equipped with an action by , then the action 2-cell is given by a morphism , and the action axioms evidently make this into a functor . Thus, is a quotient of , as desired.
However, there are three problems with the 2-category .
The solution to the first problem is straightforward. If is a 2-category with finite limits, define to be the sub-2-category of spanned by the 2-congruences which occur as kernels of morphisms in . If is an -category then any such kernel is an -congruence, so in this case is contained in and is an -category. Also, clearly factors through .
For any finitely complete 2-category , the 2-category is regular, and the functor induces an equivalence
for any regular 2-category .
Here denotes the 2-category of regular functors, transformations, and modifications between two regular 2-categories, and likewise denotes the 2-category of finite-limit-preserving functors, transformations, and modifications between two finitely complete 2-categories.
It is easy to verify that is closed under finite limits in , and also under the eso-ff factorization constructed in Theorem ; thus it is regular. If is a lex functor where is regular, we extend it to by sending to the quotient in of , which exists since is regular. It is easy to verify that this is regular and is the unique regular extension of .
In particular, if is a regular 1-category, is the ordinary regular completion of . 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 , we need to modify its morphisms.
Recall that 2-congruences in 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.
Suppose that is a finitely complete 2-site and that , , and are 2-congruences in . A functor is a weak equivalence if
is a pullback, and
The primary example we have in mind is when is a regular 2-category with its regular coverage, but it is useful to consider the general case.
If and are anafunctors between 2-congruences, then a transformation is a transformation between the two induced functors .
(Here denotes the pullback in .)
For any subcanonical and finitely complete 2-site (such as a regular -category with its regular coverage), there is a finitely complete 2-category of 2-congruences, anafunctors, and transformations in . It contains as a homwise-full sub-2-category (that is, is ff) closed under finite limits.
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 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 remain products in . Before dealing with inserters and equifiers, we observe that if is an anafunctor in and is any eso, then pulling back to defines a new congruence and an anafunctor which is isomorphic to the original in . Thus, if and are parallel anafunctors in , by pulling them both back to we may assume that they are defined by spans with the same first leg, i.e. we have .
Now, for the inserter of and as above, let be the inserter of in . It is easy to check that the composite is an inserter of in . Likewise, given with and as above, we have transformations between the two functors in , and it is again easy to check that their equifier in is again the equifier in of the original 2-cells . Thus, has finite limits. Finally, by construction clearly the inclusion of preserves finite limits.
We write for the full sub-2-category of on the -congruences, which is a finitely complete -category. Of course, it contains as a homwise-full sub--category closed under finite limits, and when is an -category we have .
If is a subcanonical finitely complete -site, then the functor is 2-fully-faithful. If is an -exact -category equipped with its regular coverage, then is an equivalence of 2-categories.
Since is 2-fully-faithful and is homwise fully faithful, is homwise fully faithful. For homwise essential-surjectivity, suppose that is an anafunctor. Then is a cover and is the pullback of along it; but this just says that . The functor consists of morphisms and , and functoriality says precisely that the resulting 2-cell equips with an action by the congruence . But since is precisely the kernel of , which is a cover in a subcanonical 2-site and hence the quotient of this kernel, we have an induced morphism in . It is then easy to check that is isomorphic, as an anafunctor, to . Thus, is homwise an equivalence.
Now suppose that is an -exact -category and that is an -congruence. Since is -exact, has a quotient , and since is the kernel of , we have a functor which is a weak equivalence. Thus, we can regard it either as an anafunctor or , and it is easy to see that these are inverse equivalences in . Thus, 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 is a finitely complete 2-category equipped with its minimal coverage, in which the covering families are those that contain a split epic, then . This is immediate from the proof of Theorem , which implies that the first leg of any anafunctor relative to this coverage is both eso and ff in , 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.
If is a 2-exact 2-category with enough groupoids, then . Likewise, if is 2-exact and has enough discretes, then .
Define a functor by taking each object to the kernel of where is eso and is groupoidal (for example, it might be the core of ). Note that this kernel lives in since is discrete, hence is also groupoidal. The same argument as in Theorem shows that this functor is 2-fully-faithful for any regular 2-category with enough groupoids, and essentially-surjective when 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 -exact completion of a regular -category, and a first step towards that is the following.
If is a regular -category, so is . The functor is regular, and moreover for any -exact 2-category it induces an equivalence
We already know that has finite limits and preserves finite limits. The rest is very similar to Theorem . We first observe that an anafunctor is an equivalence as soon as is also a weak equivalence (its reverse span then provides an inverse.) Also, is ff if and only if
is a pullback.
Now we claim that if is an anafunctor such that is eso, then is eso. For if we have a composition
such that is ff, then being eso implies that is also eso; thus is a weak equivalence and so is an equivalence. Moreover, by the construction of pullbacks in , anafunctors with this property are stable under pullback.
Now suppose that is any anafunctor, and define and let be the pullback of to along . Then is an -congruence, is ff in and thus also in , and factors through . (In fact, is the image of in .) The kernel of can equally well be calculated as the kernel of , which is the same as the kernel of .
Finally, given any with an action by this kernel, we may as well assume (by pullbacks) that (which leaves unchanged up to equivalence). Then since the kernel acting is the same as the kernel of , regularity of gives a descended functor . Thus, is the quotient of its kernel; so is regular.
Finally, if is -exact, then any functor induces one , but , so we have our extension, which it can be shown is unique up to equivalence.
When is a regular 1-category, it is well-known that (which, in that case, is the category of internal equivalence relations and functional relations) is the 1-exact completion of (the reflection of from regular 1-categories into 1-exact 1-categories). Theorem shows that in general, will be the -exact completion of whenver it is -exact. However, in general for 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 and let .
For any regular -category , is an -exact -category and there is a 2-fully-faithful regular functor that induces an equivalence
for any -exact 2-category .
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 . Thus it remains only to show that is -exact. But for any -congruence in , there is some such that and both live in , and thus so does the congruence since sits 2-fully-faithfully in preserving finite limits. This congruence in is then an object of which supplies a quotient there, and thus also in .
This page, and subsequent ones, contains an overview of my current thinking about the “internal logic of a 2-category”, as part of the 2-categorical logic project. This logic is not by any means set in stone; it’s simply the most recent incarnation (or, more accurately, the most recent incarnation that I’ve managed to write up) of evolving ideas. Any suggestions for improvement are greatly appreciated.
As adumbrated at categorified logic, the logic we use will be a logic of dependent types. In general, we allow three different sorts of types, which we call 1-types (categories, sort denoted ), 0-types (sets, sort denoted ), and (-1)-types (propositions, sort denoted ). We could include (0,1)-types (posets) and (1,0)-types (groupoids) as well, but these rarely seem as important as the other three; thus we will just identify posets and groupoids with particular categories. (Note that by using the word “set” for the 0-types, we do not in general intend to imply any smallness condition on them.)
Eventually, we will allow dependent types, with dependencies of -types on -types whenever . This will eventually involve additional subtleties with dependent products and sums, which require the “variance” of the dependencies to be specified. For now, however, we will focus on first-order logic, with no “real” type dependencies. We will also make minimal use of the sort . We do, however, require two type dependencies: dependency of propositions on types (i.e. predicate logic) and -types which are dependent on objects. The latter will be the only types of sort we consider for now. However, we set up some of the basic notions in more generality, so as not to have to re-do them later.
A basic tenet of higher category theory is that if is an -category and then is an -category. For us, this means that if is an -type and then we have a dependent -type . For instance, if , then is a 0-type: the type of arrows from to . And if , then is a (-1)-type; in other words, a proposition, which we of course interpret as the assertion . (If , it would instead be the assertion .) So equality is a special case of the formation of hom-types.
In particular, note that equality, as a proposition, is only defined between elements of a 0-type. Thus, our language doesn’t even have the terminology to speak about equality between objects of a 1-type (category), only equality between elements of a 0-type (such as arrows in a category). This is also known as the “Speak No Evil” approach to category theory.
But if thought corrupts language, language can also corrupt thought. – George Orwell
Of course, these arrow-types are notably similar to the identity types in many versions of traditional Martin-Lof dependent type theory. In fact, it is well-known by now that equality types can be usefully interpreted in categories of groupoids or in homotopical categories. (Hoffman-Striecher, “The groupoid interpretation of type theory”; Awodey-Warren, “Homotopy theoretic models of identity types”.) Of course, the main difference is that arrow-types are (in general) directional. This makes it trickier to formulate “elimination rules” that generalize the rules for ordinary identity types, but we can still have a go?. We ought also to be able to construct “iso-types” as subtypes of , which will behave like identity types. This will all come later, however.
Treating -types on an equal footing for all , we can say that our theories will consist only of two sorts of judgments:
In each case is a context, such as , which declares the variables that occur in the rest of the judgement. Each type occurring in can depend on the variables occurring before it; thus we can have but not . Formally, this means that the contexts are generated inductively according to the following rules:
Whenever we write a context it is assumed that there is no duplication of variables; this results in implicit hypotheses on the derivation rules.
To keep things looking familiar, we will usually write instead of , instead of , and instead of . Moreover, since any two inhabitants of a (-1)-type are indistinguishable (since our type theory is extensional and proof-irrelevant), we will generally write merely instead of when is a (-1)-type (a proposition). For the same reason, we never need to think about equality for inhabitants of propositions. Likewise, there can be no interesting dependence of a proposition on another proposition, so we omit propositions from the declarations of other propositions. We do, however, allow terms of an -type to depend on a variable of an -type for any and , even .
As is usual in type theories, we write
to mean that from the judgements and , we can deduce the judgement . We write for the right-hand side of an arbitrary judgement of any sort. We write for the result of substituting the term for the variable in , and we do the same for contexts.
The following rules are the basic ones for first-order 2-categorical logic. We will add additional rules in later sections, to deal with size and type dependency. Of course, any particular theory will have its own additional basic types, terms, and axioms as well.
These are just the same as in ordinary type theory, and fairly boring.
The exchange rule has, of course, the extra restriction that cannot occur freely in the type .
As suggested above, propositional equality is only meaningful for terms of a 0-type. Recall that for now, the only 0-types we consider will be hom-sets (or constructed from hom-sets).
There are also the usual symmetry, transitivity, and substitution rules for equality. These can probably be formulated only using substitution, in the style of identity types.
In theory, there should be a “directional elimination rule” for arrow-types, akin to the elimination rule for identity types in ordinary intensional type theory. However, for its correct formulation this will certainly require functorially dependent types, and it’s not even entirely clear what it should say then. So we will just directly assert the following basic operations on arrows.
Functoriality is probably the most subtle of the rules for arrow types. The idea is that a term declaration of the form describes a morphism in the ambient 2-category from the object representing the context to the object representing the term . But morphisms in a 2-category act like functors in the internal logic, and functors act on arrows as well as objects.
The term does not indicate any actual substitution of for (which would be nonsensical since they have different types). Rather, it is a decoration which converts the term with free variable into a term with free variable . In particular, is free in while is no longer free.
Similarly, a term should represent a 2-cell between the morphisms represented by and , which should be a natural transformation in the internal logic.
The logical operations on propositions are morally special cases of operations on dependent types. But real dependent types will come later, so we introduce the logical operations explicitly now. We list all the possible logical operations here, but we will also be interested in fragments of logic containing only some of these operations.
Truth:
Conjunction:
We may also have infinitary conjunctions, with an evident extension of the rules.
Falsity:
Disjunction:
We may also have infinitary disjunctions, with an evident extension of the rules. In a theory lacking implication, we also require explicitly the distributive axiom:
Implication:
We have quantification over both 1-types and 0-types, beginning with existential quantification:
In the above elimination rule, cannot occur free in . In a theory lacking implication, we must also assert the Frobenius axiom:
Universal quantification:
A 2-categorical first-order theory, or a first-order 2-theory for short, consists of:
the choice of a particular fragment of the logical rules.
a set of basic (non-dependent) 1-types , i.e. axioms of the form .
a set of basic (non-dependent) 0-types, i.e. axioms of the form .
a set of basic dependent propositions, i.e. axioms of the form . Here will depend on the typed variables occurring in .
a set of basic terms-in-context, i.e. axioms of the form . We require that these axioms come with a well-founded ordering, such that is provable from axioms preceeding it and based on the chosen logical fragment. Note that we also allow to contain propositions.
strictly speaking, the previous list of axioms includes logical axioms, but we can state these separately anyway: a set of axioms of the form , where is provable. Note that of course, can include propositions as well as 1-types and 0-types.
Note that we do not allow axiomatic dependent 1-types or 0-types. The problem with these is that they generally need to be “functorially” dependent, and we don’t want to get into that now.
The most commonly relevant fragments of logic are:
cartesian logic: the only logical constructors are and binary . (Of course, we always have equality for terms of a 0-type as atomic formulas.)
regular logic: , binary , and (plus the Frobenius rule).
coherent logic: , binary , , binary , and (plus the distributivity and Frobenius rules).
geometric logic: , binary , , arbitrary , and (plus the (infinitary) distributivity and Frobenius rules).
(finitary: first-order logic: , binary , , binary , , , and .
Firstly, any ordinary 1-categorical theory can be regarded as a 2-categorical theory with no basic 1-types, and whose basic 0-types, terms, and propositions are those of the given theory. The necessary fragment of logic will be the same. As a special case of this, any propositional theory can be regarded as a 2-categorical theory with no 1-types or 0-types.
In this theory there is one basic 1-type, call it , and no basic 0-types or propositions. We have the following axiomatic terms:
Note the necessary use of the functoriality term-constructors in stating the two coherence axioms. Strictly speaking, we should have stated the multiplication as , so that then would be written as , and the action of functoriality such as would be written as .
Again there is one basic 1-type, call it , no basic 0-types or propositions, and the following axiomatic terms:
Here we have two basic 1-types and , no basic 0-types or propositions, and the following terms:
However, see also the page adjunctions in 2-logic for some other equivalent ways of describing adjunctions.
One subtle point of difference with the 1-categorical theory is that propositions are always interpreted by subobjects in , no matter what the context. Since not every subobject of an object of a slice 2-category is necessarily a subobject in , that means that working in in a nonempty context is not quite the same as working in in the empty context. Other than that, things are pretty straightforward.
Let be a 2-categorical theory be a 2-category with sufficient structure to interpret . That means that:
We now define the following things by mutual induction:
Here is the definition:
This interpretation is sound. In other words, the induction succeeds, and all the rules for term-formation (including all the logical rules) can be interpreted.
Of course, the definition of the interpretation depends on our choosing interpretations of the basic types and terms. For example:
Any 2-category comes with a “canonical” theory associated to it, which has a canonical model in . In this theory:
Of course, this definition is again inductive, so one has to prove that the induction succeeds. Usually when we refer to the internal logic of a 2-category it is this logic we are talking about. Of course, whatever logical structure has (regular, coherent, etc.) can be reflected in its internal logic.
As in WeberYS2T, a classifying discrete opfibration in a finitely complete 2-category is a discrete opfibration such that for any , the functor
given by pullback of , is full and faithful.
The canonical example is when is some 2-category of “large categories” and is the category of (small) sets. More generally, we could take to be the 2-category and the category of sets of cardinality bounded by some cardinal .
When is equipped with a classifying discrete opfibration, we make the following definitions.
If lacks a duality involution, then merely giving the discrete opfibration 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.
We may impose additional axiom on a classifying discrete opfibration, many of which assert closure conditions of the class of small maps.
Some immediate consequences are:
We will see some further consequences of these axioms below.
Suppose that is a classifying discrete opfibration for which identity maps are small. Then there is a comma square
in which the map classifies the discrete opfibration .
A map is the same as a discrete opfibration equipped with a section with . Thus, it suffices to show that giving such data is equivalent to giving a square
in which the left-hand vertical map classifies . But the composite classifies , so since pullback of is full and faithful into discrete opfibrations, giving such a 2-cell is the same as giving a map of discrete opfibrations over , which is precisely to give a section of .
Suppose that is a CDO which is exponentiable. Then for any object , we call the exponential
the object of (small) families in . It comes with a projection to which “assigns to each family its indexing set.” Moreover, as observed in our study of exponentials, since is an opfibration and is a fibration, then is also a fibration, as we would expect.
has a universal property that can be directly expressed as follows. Evidently, to give a morphism is equivalent to giving a map together with a map over . But is simply the discrete opfibration classified by , and a map to over is just an arbitrary map to . Thus to give a map is the same as to give a small discrete opfibration together with a map : in other words, an -indexed family of small sets, each of which indexes a family of objects of .
(This sort of thing is closely related to the construction of generic families in Algebraic Set Theory.)
Now consider the special case when . As above, to give a map is to give a small discrete opfibration and a map . But a map is in turn equivalent to a small discrete opfibration . Thus is naturally equivalent the category of composable pairs of small discrete opfibrations. Recalling that any map between discrete opfibrations over is again a discrete opfibration, we observe that the 1-category consists of composable pairs of discrete opfibrations; thus is naturally a full subcategory of this category.
On the other hand, we can consider another full subcategory of determined by those composable pairs in which and the composite are small. This is precisely the subcategory , where consists of small discrete opfibrations, and is thus equivalent to . It follows that this second full subcategory of is equivalent to . 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:
Let be an exponentiable classifying discrete opfibration; the following are equivalent.
When these conditions hold, we clearly have a natural equivalence lying over , and therefore, by the Yoneda lemma, an equivalence over between and the codomain fibration .
(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 of sets satisfies the “replacement axiom” if and only if the “naive indexing” of over itself is equivalent to its “self-indexing” . In classical material set theory, this is well-known to be equivalent to the usual axiom of replacement.
Note, though, that depending on what is, may not be the “naive indexing” at all. For instance, if is the category of stacks on a topos , then the self-indexing of is a classifying discrete opfibration in , 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.
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 . For instance, if small discrete opfibrations are a subcategory, so that is a cartesian object, then we have the composite of the diagonal with the “binary products” morphism which, intuitively, takes a set to the set . Now the inserter of this composite and can be considered “the category of sets equipped with a function ,” i.e. the category of magmas.
Now we have a forgetful morphism , and also a functor which takes a magma to the triple product , 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 is a cartesian object, each hom-category has finite products, so we can define the category of rings internal to it. Then the category is equipped with a forgetful functor which has the structure of a ring in , and which is universal in the sense that we have a natural equivalence . The above construction then just shows that such a representing object exists.
If has a duality involution and is a classifying discrete opfibration, then is a “classifying discrete fibration,” and therefore also a classifying discrete opfibration in .
A classifying discrete opfibration in is not inherited by any category of truncated objects in , since and will generally not be truncated. However, it is inherited by (op)fibrational slices.
Recall first that opfibrations in can be identified with morphisms in whose underlying morphism in is an opfibration. Moreover, such an opfibration is discrete if and only if its underlying morphism in is so. Thus, it is natural to hope for the following.
If has exponentials and a classifying discrete opfibration, then each 2-category has a classifying discrete opfibration, and the small opfibrations in are those whose underlying opfibrations in are small.
Recall that when has exponentials, is comonadic over ; let denote the comonad. For any , write for the category of small discrete opfibrations over . Then our goal is for to be representable. But we have
Therefore, defining we obtain a classifying discrete opfibration in that classifies the desired small opfibrations.
If has exponentials, a duality involution, and a classifying discrete opfibration, then each 2-category also has a classifying discrete opfibration.
A cosieve is a morphism in a 2-category that is both ff and a discrete opfibration. Equivalently, it is a subterminal object in . It is easy to check that in , this is equivalent to saying that is a full subcategory of such that if and , then .
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 for a classifying cosieve. Clearly any such 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 . In , the “walking arrow” is a cosieve classifier.
If is any classifying discrete opfibration in a Heyting 2-pretopos , then the subobject of described in the internal logic by
is the largest subobject such that the pullback of to 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 .
In , the cosieve classifier arises from (or any full subcategory of it containing and ) in this way.
If is groupoidal, then every ff into is a cosieve. Therefore, maps from a groupoidal into a cosieve classifier classify all subobjects of . Since subobjects of are the same as subobjects of its core if that exists, subobjects of can be classified by maps .
Moreover, if a cosieve classifier itself has a core, then since is a coreflection of into , it is a subobject classifier in in a suitable (2,1)-categorical sense. Moreover, since is posetal, its core (if it exists) is discrete. Thus:
If is a 2-category having a cosieve classifier and enough groupoids, then has a subobject classifier.
In particular, if also has (discrete) exponentials, then is a topos.
However, 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 , the category is the 1-topos of 1-sheaves on the homwise-discrete reflection of , 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 is a cosieve classifier, is a sieve opclassifier, i.e. is equivalent to the opposite of the poset of sieves on . On we thus have both a sieve and a cosieve , pulled back from and ; let be the subobject of defined as in the Heyting algebra structure. Now maps into classify sieves and cosieves that are equal as subobjects, which is to say, subobjects that are both sieves and cosieves. And transformations between maps correspond to both inclusions of cosieves and coinclusions of sieves, which is to say, identities; thus is discrete, and hence a subobject classifier in .
If is a Heyting 2-category having a cosieve classifier and a duality involution, then has a subobject classifier.
If has a cosieve classifier and (discrete) exponentials, but not enough groupoids, then may not be a topos. But it retains many of the properties of a topos, because even though the “power object” is not an object of , it can still be quantified over in the internal logic of to define objects and properties in , and even in , where all subobjects are cosieves.
For example, if is also Heyting, then for any groupoidal we can construct the “internally least” subobject of with some property, as
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:
If is 1-exact and Heyting with exponentials and a cosieve classifier, then is finitely cocomplete.
If is not groupoidal, then the above technique only constructs cosieves in rather than arbitrary subobjects of it. However, if there are enough groupoids, we can construct arbitrary subobjects of any object in this way, since subobjects of are bijective with subobjects of its core . In particular:
If is 1-exact and Heyting with exponentials, a cosieve classifier, and either enough groupoids or a duality involution, then it has discrete reflections.
It suffices to be able to construct the equivalence relation generated by the image of , for any . Note that these relations are not cosieves on , but as remarked above, we can get around this if has a core. Alternately, since the relations we care about are all “2-sided sieves” (subterminals in ), if there is a duality involution we can turn them into cosieves on and perform the closure there.
In another vein, if is a positive Heyting 2-category with a (necessarily discrete) natural numbers object , we can of course construct the discrete object of rational numbers in the usual way, and then define the Dedekind real numbers as two-sided cuts. Thus, is a subobject of , and hence posetal, but since the order relation on inherited from the two copies of would go in different directions, in fact 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 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.
Created on January 22, 2010 at 19:52:35. See the history of this page for a list of all contributions to it.