Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 25, 2012

PSSL 93 trip report

Posted by Mike Shulman

I just got back from an excellent trip to the U.K., which started with my first visit ever to Wales, continued with my second PSSL, and concluded with my first ever visit to Scotland (thanks Tom!). Homotopy type theorists may be interested to have a look at my slides from Swansea (and also the slides from a seminar we had at UCSD last quarter), but I won’t say any more about that now. Instead I want to discuss briefly several of the PSSL talks.

One talk that I particularly enjoyed was John Bourke’s. He’s found a way to use F-categories to formulate a 2-dimensional “monadicity theorem” which includes lax and oplax morphisms as well as strict and pseudo ones. This further justifies Steve’s and my claim that \mathcal{F}-categories are a natural context in which to talk about 2-monads.

As it happens, doctrinal adjunction becomes one of the defining properties of a monadic \mathcal{F}-functor, similar to conservativity and creation of split coequalizers in the traditional case. The others are that the forgetful functor is locally an isofibration (i.e. any morphism which is isomorphic to a lax (or pseudo or oplax) morphism has a unique compatible such structure) and reflects identity-ness of 2-cells.

This is one of those things that when you see it, you think (or at least I did) “why on Earth hasn’t someone done this before?” As John pointed out, in ordinary monad theory, Beck’s monadicity theorem lets us say that (for instance) the category of groups is monadic over sets without knowing anything about the “free group” functor other than that it exists. In 2-monad theory, we had the strict CatCat-enriched monadicity theorem to tell us about strict algebras and strict morphisms, and a bicategorical monadicity theorem to tell us about pseudo algebras and pseudo morphisms, but in order to identify (say) lax monoidal functors with lax TT-morphisms, where TT is the monad induced on CatCat by the forgetful functor from MonCatMonCat and its left adjoint, we needed to compute TT very carefully! This is kind of a barrier to working with 2-monads in practice, since left adjoints to forgetful functors are often quite hairy to construct. John’s 2-dimensional monadicity theorem solves this problem.

Mike Stay’s subject of compact closed bicategories was also close to my heart, although I don’t have much to say about it. We’ve talked about presenting “theories with duality” once or twice over two years ago. Mike described the “free compact closed bicategory on a symmetric-monoidal-closed object”, using some pretty but intricate pictures.

Eugenia Cheng’s talk was also related to duality, but in a different way. Ordinary adjunctions are something we can talk about internal to any 2-category, but they give rise to a mates correspondence which is most naturally described using double categories. Multi-variable adjunctions are something we can talk about internal to a compact closed bicategory (or proarrow equipment, or extraordinary 2-multicategory, etc.). But they also give rise to a “parametrized mates” correspondence, which is most naturally described using something that Eugenia (describing joint work with Nick Gurski and Emily Riehl) called a cyclic double multicategory. What on earth is that?

In the double category that we use to talk about ordinary mates, the vertical morphisms are adjoint pairs. In a multivariable version of this, the vertical morphisms should therefore be multivariable adjunctions. A two-variable adjunction from (C,D)(C,D) to EE is usually described using three functors looking like this: : C×DE hom l: C op×ED hom r: D op×EC \begin{aligned} \otimes :& C \times D \to E \\ hom_l :& C^{op} \times E \to D \\ hom_r :& D^{op} \times E \to C \end{aligned} but EGR realized that it looks a lot more symmetric if you write F=E opF=E^{op}, since then we have functors: : C×DF op hom l op: F×CD op hom r op: D×FC op \begin{aligned} \otimes :& C \times D \to F^{op} \\ hom_l^{op} :& F \times C \to D^{op} \\ hom_r^{op} :& D \times F \to C^{op} \end{aligned} We also switched the order of the inputs to hom l ophom_l^{op}, so as to make the cyclic ordering of the objects be preserved in all three cases. Thus, the “vertical part” of this double-category-like structure should contain “morphisms” indexed by cyclically ordered nn-tuples of objects. Once you make that precise (a “cyclic multicategory”) you can just define a cyclic double multicategory to be an internal category in cyclic multicategories.

Eugenia also mentioned a subtle issue that I don’t fully understand. It turns out to be kind of tricky to make precise what you mean by “morphisms indexed by cyclically ordered tuples of objects”. The way that EGR did it is to consider instead morphisms indexed by an ordered tuple of inputs and a single output, but with an action of cyclic groups. That is, given a morphism in Hom(a,b,c;d op)Hom(a,b,c \,;\, d^{op}), we can act on it cyclically to obtain morphisms in Hom(b,c,d;a op)Hom(b,c,d \,;\, a^{op}), Hom(c,d,a;b op)Hom(c,d,a \,;\, b^{op}), and Hom(d,a,b;c op)Hom(d,a,b \,;\, c^{op}).

Note that we need an involution () op(-)^{op} on objects here. This is true even if you take more literally the idea of “morphisms indexed by cyclically ordered tuples of objects”, since in order to “compose” two of these morphisms along an object aa, you need to be able to specify that aa is part of the “domain” of one morphism and the “codomain” of the other. With only a cyclically ordered list of objects, the only way to do that is to have it appear “opped” in one list but not the other.

It may seem at first glance as though the two ways of describing cyclic multicategories should be equivalent, once you figure out how to make them both precise. But no — the one with cyclic group actions seems to be more expressive, because the group actions don’t have to be free. The other description can apparently only describe versions where the action is free.

While writing this post, it just occurred to me that this issue already comes up in the single-variable case! The vertical category whose morphisms from aa to bb are adjoint pairs aba\rightleftarrows b also has an involution () op(-)^{op}, and an adjoint pair aba\rightleftarrows b yields equivalently an adjoint pair b opa opb^{op}\rightleftarrows a^{op} (passing to opposite categories switches which functor is the left and which the right adjoint). And we can also have non-free actions here: if it should happen that b=a opb = a^{op}, then we can ask whether an adjoint pair aa opa\rightleftarrows a^{op} is fixed by the involution. If so, what we have is a contravariant endofunctor which is “adjoint to itself on the right”, i.e. we have isomorphisms Hom(x,F(y))Hom(y,F(x))Hom(x,F(y)) \cong Hom(y,F(x)). For instance, the powerset functor has this property. Perhaps Eugenia, Nick, and Emily have already thought about this.

There were many other nice talks: Nick spoke about the Gray tensor product, Tom about the eventual image, and I talked about cardinalities and Euler characteristics. I’ll blog about the latter some day (hopefully soon) when the paper is finished. But the only other one I want to say anything about right now is Benno van den Berg’s.

The notion of “elementary topos” is considered “impredicative” in that it contains subobject classifiers. Various people have proposed “predicative” versions of it, but none of them have ever been really satisfactory. For one thing, since the notion of “Grothendieck topos” makes perfect sense predicatively, you’d like your “predicative elementary toposes” to be closed under constructions like sheaves — but this turns out to be kind of tricky to do predicatively.

Benno (describing joint work with Ieke Moerdijk, which has now appeared) proposed that a predicative topos should be a Pi-W-pretopos (a fairly standard thing to ask) which also satisfies the internal version of the axiom WISC. (They also propose to call WISC the “axiom of multiple choice”, replacing the axiom previously known by that name and now to be called “strong AMC”, since it implies WISC but seems just a bit stronger. I don’t think I have strong feelings about that either way.) WISC turns out to be “just enough choice” to deduce closure under sheaves and realizability, as well as ex/lex completion (which ordinary elementary toposes are not closed under).

Of course, WISC has the disadvantage that not all elementary toposes satisfy it, so not every elementary topos would be a predicative topos (although since WISC is preserved by sheaves, every Grothendieck topos over a classical version of Set will be). Benno took the radical point of view that that means something is not quite right with the definition of elementary topos!

I’m actually in sympathy with that: the main problem I have with elementary toposes (which Benno also emphasized) is that they don’t admit all sorts of free/inductive/recursive constructions. They do automatically have W-types (at least, as soon as they have a natural numbers object), but in a way that’s sort of an accident. Having W-types bascially means having free algebras for “free” algebraic theories, but elementary toposes don’t necessarily have free algebras for arbitrary algebraic theories.

In fact, Benno mentioned a theorem of Andreas Blass that free algebras for arbitrary algebraic theories cannot even be constructed in ZF! (The problem is that you want to first build a set of all words in the operations of the theory, then quotient by all the relations of the theory, but it’s not clear how to make the operations act on the resulting quotient unless you have a choice principle to “lift” the inputs back to the set of words.) Surely something is wrong with a foundation for mathematics in which not all algebraic theories have free algebras. (-:

Personally, while I like WISC, I would prefer not to have to include any sort of choice principle in a foundational system intended as “constructive”. (I know that many “constructivists” would disagree, being fond of even stronger choice principles such as COSHEP, which are not even valid in every Grothendieck topos over ZFC.) I would prefer something like higher inductive types which are a natural generalization of W-types. Of course, they were originally motivated by \infty-considerations, but they make perfect sense even in a traditional set-based foundational system; in that case, what they essentially allow us to do is to inductively define a set and quotient it by an equivalence relation at the same time. This is sufficient to construct free algebras, and also to do things like sheafification.

The paper on HITs that Peter Lumsdaine and I are writing intends to show how to construct HITs in Grothendieck (,1)(\infty,1)-toposes over a classical foundation of ZFC. Blass’ result implies that ZF is insufficient, but we conjecture that WISC (plus ordinary W-types) suffices (and we have a general idea of how the proof will go—we’re also currently writing another paper about that sort of thing). I am also tempted to conjecture that ΠW\Pi W-pretoposes with HITs are stable under constructions like sheaves and realizability. If so, maybe they could also be a notion of “predicative elementary topos” — one which might generalize more directly to “predicative elementary (,1)(\infty,1)-toposes”. (Okay, I lied: cf. the last slide of my Swansea talks.)

I should also mention another possibly contentious issue: in contrast to Benno’s talk at the PSSL, their paper on the arXiv works in the context of “algebraic set theory”, i.e. with a “category of classes” rather than merely a topos-like “category of sets”. Benno says that this isn’t essential, though, and that there may be a second paper that works only with a topos-like category.

Relatedly, one might also be tempted to include the existence of “universes” in a notion of predicative topos — this is certainly natural from the (,1)(\infty,1)-point of view (cf. object classifiers and the univalence axiom). Benno expressed a dislike for universes as a foundational assumption; my own feeling about them seems to vacillate with the phase of the moon. One thing that universes give you is what type theorists call large elims: the ability to define sets recursively. For instance, in an elementary topos with NNO (even one satisfying full AC) one can’t in general define the \mathbb{N}-indexed family of iterated power-objects P n(X)P^n(X) of an object XX. One can consider allowing large elims directly, but universes (especially univalent ones) are a very convenient way to obtain them.

Regardless, it’s nice to see WISC finally getting some attention!

Posted at April 25, 2012 8:49 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2521

12 Comments & 0 Trackbacks

Re: PSSL 93 trip report

Since I feel that it deserves to be highlighted, let me try to highlight something that is a bit implicit in what you are saying, probably because you are being modest:

you have amplified here and elsewhere at length how homotopy type theory does not directly implement (homotopy) colimits (not in the naive way, specifying diagrams etc), but that it is the (higher) inductive types that provide (much) of the structure of (homotopy) colimits.

So when one sticks to the traditional definition of elementary toposes and its evident generalization to \infty-toposes, one has some conceptual friction between

a) the demand for finite colimits

and

b) the supply of inductive types.

So on the very very last Swansea slide you are proposing to define that friction away: to re-define the notion of elementary topos such that finite colimits no longer feature explicitly in the axioms, but are instead replaced by an explicit demand for (higher) inductive types.

This way, (homotopy) type theory would move closer still to the theory of elementary (higher) toposes.

And you are saying here: look, it is not just the closer match with (homotopy) type theory that motivates asking if the original axioms of elementary toposes shouldn’t be modified, but also the recent work by Benno and Ieke suggests such a modification which, if not the same, is at least closely related.

Is that roughly a correct summary?

Posted by: Urs Schreiber on April 25, 2012 5:37 PM | Permalink | Reply to this

Re: PSSL 93 trip report

probably because you are being modest

Say rather that I don’t want to sound too much like a broken record. (-: But yes, I think that’s about right.

Something that’s maybe worth mentioning in that connection is that in order for “inductive types” to include finite coproducts, one needs the sort of inductive types that are found in Coq, which allow multiple “constructors”. When people say “W-types” they usually refer to a particular subclass of “inductive types”, essentially corresponding to those that have only one constructor. On the other hand, if you already have well-behaved finite coproducts, then you can make any finite number of constructors into one constructor. So there’s some theorem to be expected about W-types + coproducts = inductive types, which I’ve been told about numerous times but never I think found a precise statement and proof.

Amusingly, however, higher inductive types require you to allow more than one constructor, since to be nontrivially “higher” you need at minimum one point-constructor and one path-constructor.

Posted by: Mike Shulman on April 25, 2012 10:31 PM | Permalink | Reply to this

Re: PSSL 93 trip report

So there’s some theorem to be expected about W-types + coproducts = inductive types, which I’ve been told about numerous times but never I think found a precise statement and proof.

Bas Spitters has pointed out by private email that this theorem is stated in section 7.2 of Voevodsky’s notes. A proof doesn’t seem to be included however.

Posted by: Mike Shulman on April 30, 2012 3:46 AM | Permalink | Reply to this

Re: PSSL 93 trip report

>WISC has the disadvantage that not all elementary toposes satisfy it

I know we’ve discussed the issue of the independence of WISC, Mike, and I’ve had a stab at proving it but not finished (yet). Have you proved this, or have Benno and Ieke?

Posted by: David Roberts on April 26, 2012 1:15 AM | Permalink | Reply to this

Re: PSSL 93 trip report

Have you proved [the independence of WISC], or have Benno and Ieke?

I don’t think either of us has proven it just yet. But Benno mentioned a conjecture that WISC suffices to construct free algebras for all algebraic theories, which is similar to the conclusion that Peter L. and I have been drawn towards — we need transfinite arguments to build models for HITs, with which in turn one can certainly construct free algebras; whereas in considering how to make transfinite arguments work without choice we’ve been led towards something like WISC. If this is so (that WISC implies free algebras), then Blass’ result implies that WISC is unprovable in ZF (if ZF is consistent).

Posted by: Mike Shulman on April 26, 2012 2:28 AM | Permalink | Reply to this

Re: PSSL 93 trip report

WISC is indeed independent from ZF. A posted a note to that effect on my homepage. It is also sufficient (in ZF at least!) to prove the existence of free algebras. Of course, this doesn’t mean that the same is true in a predicative topos, but I am confident that it holds there as well.

Btw, the slides of my PSSL talk are available at the conference homepage, as are the slides of a number of other talks.

Posted by: Benno van den Berg on May 4, 2012 10:07 AM | Permalink | Reply to this

Re: PSSL 93 trip report

Excellent!

Your note says that by refining the argument, WISC shows that there exist arbitrarily large regular cardinals. I’m going to guess that the argument goes something like, given a set AA, repeat the argument given with AA (or maybe subsets of AA?) replacing \mathbb{N} to obtain an ordinal with cofinality >|A|\gt{|A|}; then that cofinality is a regular cardinal >|A|\gt{|A|}.

Can you say anything about how this is related to the regular extension axiom in all its variants? Intuitively, REA is also about the existence of arbitrarily large regular cardinals, but with “regular cardinal” interpreted not as a particular kind of well-ordering but in the (arguably, constructively more sensible) way as a collection of sets with certain closure properties.

On your PSSL slides you claimed that REA is “highly set-theoretic and uncategorical” but I’m not sure I would agree with that. Certainly as usually phrased it is \in-theoretic, but why couldn’t we formulate a structural/categorical version? We know how to formulate structural versions of the axioms of collection and replacement, and the essential aspect of REA (it seems to me) is a set closed under relative versions of these axioms.

Posted by: Mike Shulman on May 4, 2012 7:30 PM | Permalink | Reply to this

Re: PSSL 93 trip report

Your note says that by refining the argument, WISC shows that there exist arbitrarily large regular cardinals. I’m going to guess that the argument goes something like, given a set A, repeat the argument given with A (or maybe subsets of A?) replacing ℕ to obtain an ordinal with cofinality >∣A∣; then that cofinality is a regular cardinal >∣A∣.

That’s right. The argument I had in mind was: if there would be a bound kappa on the size of the regular cardinals, every limit ordinal would be the supremum of at most kappa many smaller ordinals. Then the same argument as in the note works when replacing ℕ with kappa.

I agree the statement “there are arbitrarily large regular cardinals” sounds very REA-like. But what is not clear to me is whether regular cardinals in ZF have the collection property that is distinctive of the regular sets as postulated by REA.

To explain what I find so difficult about capturing REA categorically, let’s first consider the following axiom: every map is contained in a class of small maps (satisfying in particular the collection and representation axioms). At first sight, that’s just like REA. (Note that it implies AMC and hence WISC.) But it is not quite REA because here we postulate universes U such that every epi P -> T(u) is refined by one of the form T(u’) -> T(u). REA is weaker: it only says that U should have this property for epis whose codomain P is a subset of U. It’s that aspect that I find so hard to categorify.

Anyway, there are lots of interesting questions here. One would like to know which principles imply and do not imply others, in ZF, in a topos and in a predicative topos. But establishing independence results is not going to be easy, as most of these principles are (probably) going to be preserved by all standard model-theoretic constructions.

Posted by: Benno van den Berg on May 7, 2012 1:27 PM | Permalink | Reply to this

Re: PSSL 93 trip report

what is not clear to me is whether regular cardinals in ZF have the collection property that is distinctive of the regular sets as postulated by REA.

Yes, I agree that that seems very unlikely.

The Rathjen-Lubarsky paper “On the regular extension axiom and its variants” isolates several different versions of REA, each asserting that every set is contained in a set with a different regularity property:

  • a “regular set” satisfies the strong collection axiom
  • a “weakly regular set” satisfies the non-strong collection axiom
  • a “functionally regular” set satisfies the replacement axiom
  • a “strongly regular” set is regular and closed under unions and exponentials

Strong REA in ZFC of course implies weak inaccessibles, but the others are provable in ZFC. My experience is that the non-strong collection axiom is not much good, so I’m not that interested in weak REA, but the interesting thing to me is that they prove that ZF already implies functional REA. I don’t fully understand the proof, but it appears to involve something like Hartogs’ theorem (for every set there is an ordinal that doesn’t embed into it). Apparently the ordinals you get from that are “regular enough” to show fREA. I guess that without choice the functional regularity of a set doesn’t “descend” to regularity of its ordinal rank?

Anyway, do you think there’s any chance that WISC implies any form of REA?

It’s that aspect that I find so hard to categorify.

Hmm. Well, I’m not partial to classes of small maps, so here’s how I would go about categorifying it. Let’s work in a well-pointed pretopos – we can always internalize in non-well-pointed categories afterwards by passing to the stack semantics.

Suppose TUT\to U is a “universe” of some sort. I guess you are writing T(u)T(u) for the object u *Tu^\ast T classified by some u:1Uu\colon 1\to U. The hypothesis in the statement of regularity for UU is that we have some u:1Uu\colon 1\to U and an entire relation from T(u)T(u) to UU, which is to say a monomorphism RT(u)×UR\rightarrowtail T(u)\times U such that RT(u)R \to T(u) is epi. Then the conclusion that seems most natural to me is that we have an element v:1Uv\colon 1\to U and a map i:T(v)Ui\colon T(v) \to U such that (1,i) *R(1,i)^\ast R is entire in both directions from T(u)T(u) to T(v)T(v) and vice versa.

In the usual material-set-theoretic phrasing, UU is a set of sets and T={(x,y)|xyU}T = \{ (x,y) | x\in y\in U \}, with TUT\to U projecting (x,y)(x,y) to yy. Moreover, since UU is “transitive”, for any v:1Uv\colon 1\to U we have a canonical inclusion T(v)UT(v) \hookrightarrow U. But it seems to me that the material REA directly implies the one I formulated above, where we can take the map i:T(v)Ui\colon T(v) \to U to be this canonical inclusion.

Now I suppose I should actually do the translation into the stack semantics… given any XX, a map u:XUu\colon X\to U, and an entire relation from u *Tu^\ast T to X×UX\times U in the slice category over XX (that is, a monomorphism Ru *T× X(X×U)u *T×UR\rightarrowtail u^\ast T \times_X (X\times U) \cong u^\ast T \times U such that Ru *TR\to u^\ast T is epi), there exists an epi p:YXp\colon Y\twoheadrightarrow X and morphisms v:YUv\colon Y\to U and i:v *TUi\colon v^\ast T \to U such that (p,i) *R(p,i)^\ast R is bi-entire from (up) *T(u p)^\ast T to v *Tv^\ast T. How does that relate to the version you suggested?

Posted by: Mike Shulman on May 7, 2012 6:57 PM | Permalink | Reply to this

Re: PSSL 93 trip report

My experience is that the non-strong collection axiom is not much good

I absolutely agree.

Apparently the ordinals you get from that are “regular enough” to show fREA. I guess that without choice the functional regularity of a set doesn’t “descend” to regularity of its ordinal rank?

Mmm, I would have to study the proof. That might be quite delicate.

Anyway, do you think there’s any chance that WISC implies any form of REA?

AMC does (in the presence of W-types; see Moerdijk and Palmgren’s paper on predicative aspects of AST). I would guess that this is no longer possible in the presence of WISC.

If I would have to guess I would say that AMC is stronger than both WISC and REA, and both of these are genuinely stronger than postulating the existence of free algebras for algebraic theories, while WISC and REA are incomparable. But I wouldn’t be so surprised if some implications can actually be reversed (especially in ZF). And, as I said, independence results are going to be really tough to prove.

But maybe you were thinking of proving fREA using WISC in CZF with W-types? That might be interesting.

so here’s how I would go about categorifying it.

Ok, that’s fair enough. I guess I am partial to stating axioms purely in terms of categorical properties of the small objects/maps, rather than as a property of a universe. I shan’t be so dismissive about REA in the future. :-)

How does that relate to the version you suggested?

My version is more like AMC. Actually, I guess you could formulate a notion of a “super regular set” (a transitive set U such that every surjective map onto an element of U is refined by a surjection from an element in U, or maybe by a surjection in U) and then prove that AMC is equivalent to the corresponding form of REA. And perhaps one can rephrase WISC in a similar REA-like way by saying that U contains enough surjections to refine all surjective maps onto a given set A.

Posted by: Benno van den Berg on May 8, 2012 6:07 PM | Permalink | Reply to this

Re: PSSL 93 trip report

maybe you were thinking of proving fREA using WISC in CZF with W-types?

I don’t think I had anything so concrete in mind, but it would certainly be interesting to see that!

Posted by: Mike Shulman on May 9, 2012 11:30 PM | Permalink | Reply to this

Re: PSSL 93 trip report

BTW, in case anyone is too lazy to google Benno’s homepage, here is the link to his note.

Posted by: Mike Shulman on May 4, 2012 7:34 PM | Permalink | Reply to this

Post a New Comment