Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: mathematics

Topic: natural numbers

John Baez (Mar 24 2021 at 18:59):

A new paper:

• Nima Rasekh, Every elementary higher topos has a natural number object.

The abstract says:

We prove that every elementary (∞,1)-topos has a natural number object. We achieve this by defining the loop space of the circle and showing that we can construct a natural number object out of it.

Cute! I guess the idea must be that $\pi_1(S^1) \cong \mathbb{Z}$. So the circle holds within it the integers, which count how many time you've gone around the circle... and the integers hold within them the natural numbers.

Oscar Cunningham (Mar 24 2021 at 20:29):

Does this mean that results involving finite sets within $\mathbf{Set}$ don't have nice analogues in HoTT?

Cody Roux (Mar 24 2021 at 21:40):

This is indeed a bit surprising: it means that every $(\infty, 1)$-topos is pretty huge.

Mike Shulman (Mar 24 2021 at 22:26):

Yes, there's no real close higher-dimensional analogue of the topos $\rm FinSet$. This is a problem already for 1-groupoids: finite groupoids are not closed under finite colimits (the homotopy coequalizer of $1\rightrightarrows 1$ is $B\mathbb{Z}$, which is not finite), while finitely presented groupoids are closed under finite colimits but not finite limits (the loop space of $B\mathbb{Z}$ is the discrete $\mathbb{Z}$, which is not finitely presented).

Mike Shulman (Mar 24 2021 at 22:28):

You can, of course, talk about finite sets in HoTT, meaning finite 0-types, and prove pretty much anything about them that you like. But there isn't really a notion of "finite $n$-type" for $n>0$ that's a "world unto itself" like the finite sets are. (Although finite homotopy types are important in homotopy theory, it's just that they don't form a topos on their own.)

Mike Shulman (Mar 24 2021 at 22:29):

The fact that you get some kind of "axiom of infinity" automatically in a higher-categorical foundation is a pretty old observation, I think it's already in Lawvere's "Elementary theory of the category of categories" from the 1960s.

Mike Shulman (Mar 24 2021 at 22:31):

But it wasn't clear for a while whether we can actually get the useful kind of infinity, an NNO, just from the circle.

Mike Shulman (Mar 24 2021 at 22:32):

(We can also get it from other places, such as from an impredicative construction involving a universe.)

Joachim Kock (Mar 24 2021 at 22:59):

Could it be that the proper notion of finite in the homotopy world is some next regular cardinal, instead of omega? Or does it just go crazy beyond bounds? One reason for suggesting the first option is that there are theorems in infinity-category theory that only really work relative to regular cardinals bigger than omega. For example, theorems in 1-category theory that rely on coequalisers being finite colimits, in \infty-category theory these have to be replaced by geometric realisations, and they are not finite colimits but still kappa-small for kappa > omega.

I ask out of curiosity, because I am pretty ignorant about such size issue, and find it very difficult to form an intuition.

Mike Shulman (Mar 24 2021 at 23:53):

Well, types of size $<\kappa$ aren't closed under the operations of type theory unless $\kappa$ is not just regular but inaccessible. And we do have inaccessibles represented in type theory already, sort of, as universe types.

John Baez (Mar 25 2021 at 04:28):

At this point it's fun to remember that $\omega$ would count as inaccessible if we hadn't chosen a definition that explicitly says an inaccessible cardinal needs to be bigger than $\omega$.

Mike Shulman (Mar 25 2021 at 04:56):

Maybe the $\infty$-categorical perspective makes the exclusion of $\omega$ from inaccessibility seem less arbitrary.

dusko (Mar 25 2021 at 06:39):

my intuitions about higher toposes are very shallow, and i may be totally missing the point, and i didn't read the paper carefully at all, but doesn't the construction in Sec 2 projected down to Cat, basically boil down to constructing the coequalizer of the two embeddings of 1 into the poset 2. and sure, yes, the coequalizer is the monoid N. but do we really need any of the higher-dimensional stuff?

Amar Hadzihasanovic (Mar 25 2021 at 08:03):

Mike Shulman said:

Yes, there's no real close higher-dimensional analogue of the topos $\rm FinSet$. This is a problem already for 1-groupoids: finite groupoids are not closed under finite colimits (the homotopy coequalizer of $1\rightrightarrows 1$ is $B\mathbb{Z}$, which is not finite), while finitely presented groupoids are closed under finite colimits but not finite limits (the loop space of $B\mathbb{Z}$ is the discrete $\mathbb{Z}$, which is not finitely presented).

Not sure if this makes sense, but loop spaces and more in general mapping spaces between finite types feel “locally finite” to me, in the sense than a cell in $Y^X$ is determined by finitely many cells in the finitely presented space $Y$. Do things get any better if we consider “locally finite types” in some sense?

Amar Hadzihasanovic (Mar 25 2021 at 08:12):

I guess that mapping out of mapping spaces would take you out of “local finiteness”, so you still can't get a closed structure.

David Michael Roberts (Mar 25 2021 at 09:53):

Cody Roux said:

This is indeed a bit surprising: it means that every $(\infty, 1)$-topos is pretty huge.

Yes, they are! There's another recent paper that shows that once you have an elementary oo-topos a la Mike, you get not just an inaccessible, but a 1-inaccessible

Joachim Kock (Mar 25 2021 at 14:49):

Mike Shulman said:

Well, types of size $<\kappa$ aren't closed under the operations of type theory unless $\kappa$ is not just regular but inaccessible.

Thanks. I have read up on these definitions, and I now have them in my short-term memory again!

Mike Shulman (Mar 25 2021 at 15:42):

dusko said:

my intuitions about higher toposes are very shallow, and i may be totally missing the point, and i didn't read the paper carefully at all, but doesn't the construction in Sec 2 projected down to Cat, basically boil down to constructing the coequalizer of the two embeddings of 1 into the poset 2. and sure, yes, the coequalizer is the monoid N. but do we really need any of the higher-dimensional stuff?

I don't know what you mean by "projected down to Cat". It's true that the construction takes place entirely in the world of 1-types, i.e. groupoids; the $\infty$-ness isn't necessary. And yes, that coequalizer in Cat is the delooping of the monoid N, so you can get N itself as a hom-set (directed loop space, comma object) -- that's what's already in ETCC that I mentioned above, although I don't think he proves internally that the result satisfies any kind of "axiom of infinity". Working with groupoids makes it trickier than working with categories since you get inverses automatically too, so you get the integers first and have to carve out the naturals from those. That, together with actually proving internally that the result behaves like the natural numbers (rather than seeing externally that that's what you get), is what's new here.

John Baez (Mar 25 2021 at 16:43):

Interesting. So working in the world of homotopy types rather than categories actually makes it harder to get ones hands on the natural numbers.

Fawzi Hreiki (Mar 25 2021 at 16:47):

I wonder if that remains the case in whatever directed homotopy turns out to be, or if the natural numbers emerge first

John Baez (Mar 25 2021 at 16:48):

David Michael Roberts said:

Cody Roux said:

This is indeed a bit surprising: it means that every $(\infty, 1)$-topos is pretty huge.

Yes, they are! There's another recent paper that shows that once you have an elementary oo-topos a la Mike, you get not just an inaccessible, but a 1-inaccessible.

That's crazy! When y'all were talking about "getting an inaccessible", it seemed to make sense, because I thought it was just saying that to model homotopy types we need a bunch of infinite things closed under all sorts of operations familiar from set theory and topology. But "getting a 1-inaccessible" means we get an infinite tower of inaccessible cardinals, in a very strong sense. If you can provide any intuition about that, it'd be great.

(I'm not really sure what "get"means here.)

John Baez (Mar 25 2021 at 16:50):

Oh, maybe the point is that now we're talking about axioms that include the existence of a "universe object", or whatever you call it? A type that acts like the type of all types.

John Baez (Mar 25 2021 at 16:50):

This would obviously drive up the size of the smallest model.

Mike Shulman (Mar 25 2021 at 17:19):

Yeah, I think the Lo Monaco paper is kind of misleadingly written. "Of course" if you assume as an axiom that every object is contained in an inaccessible-like universe, then to model that axiom you need arbitrarily large inaccessibles. There are details to work out, of course, and it's interesting that you only need $\Pi$-types and not $\Sigma$-types, but this isn't anything fundamental about categorical dimension, only about the choice of whether toposes (of whatever categorical dimension) are assumed to contain universes or not.

Mike Shulman (Mar 25 2021 at 17:21):

The main difference is that universes are more useful and necessary in the $\infty$-case than in the 1-case, which is why I included them in my proposed definition of elementary $\infty$-topos.

Mike Shulman (Mar 25 2021 at 17:23):

Fawzi Hreiki said:

I wonder if that remains the case in whatever directed homotopy turns out to be, or if the natural numbers emerge first

One could ask that question concretely about Riehl-Shulman directed type theory: with the interval we should be able to define a "directed HIT" with one point and an endo-arrow, and ask whether its hom-type can be proved to be a NNO.

Fawzi Hreiki (Mar 25 2021 at 17:34):

Has anyone done this?

Mike Shulman (Mar 25 2021 at 18:18):

Not that I know of.

David Michael Roberts (Mar 25 2021 at 20:12):

To me the surprising thing is not just you need a bunch of inaccessibles, but that you need more than countably-many, which is what one might naively expect from type theory, but rather "inaccessibly-many".

Cody Roux (Mar 25 2021 at 20:29):

My naive type theoretic intuition is that you need inaccessibles when you have "large elimination" i.e. when you can talk about $\mathbb{N}\rightarrow U$ as a "first class" object.

John Baez (Mar 25 2021 at 23:39):

David Michael Roberts said:

To me the surprising thing is not just you need a bunch of inaccessibles, but that you need more than countably-many, which is what one might naively expect from type theory, but rather "inaccessibly-many".

Yes. What sort of construction pushes us into needing that many?

David Michael Roberts (Mar 26 2021 at 00:29):

Probably because one needs something like a family of "universal" maps with arbitrarily large fibres, but also each closed under all kinds of operations. Mike would know better.

Mike Shulman (Mar 26 2021 at 00:44):

It just depends on what you want. If what you want is to interpret type theory with countably many universes, then you only need countably many inaccessibles. But if you want to be able to use type theory with universes to reason about any object of the category in question -- or even if you just want to use universes categorically to reason about arbitrary objects of the category -- then you need every object of the category to be contined in some universe. That's what pushes you from countably many inaccessibles to a proper class of them.

John Baez (Mar 26 2021 at 01:13):

Okay, that makes sense. Does the axiom of universes in ordinary set theory - which says that every set is in a Grothendieck universe - imply the existence of a 1-inaccessible cardinal? Is it equivalent to that?

Mike Shulman (Mar 26 2021 at 02:50):

The ordinary axiom of universes and the existence of enough universes in $\infty$-toposes (regarded as proper-class-sized categories) are the same large cardinal axiom, which can be phrased as "Ord is 1-inaccessible", and doesn't imply the existence of a "small" cardinal (i.e. a set) that's 1-inaccessible. But if you insist that all categories are sets in some universe, then to have an $\infty$-topos with enough universes you need a 1-inaccessible "outside" the topos.

John Baez (Mar 26 2021 at 05:01):

By "outside", do you mean if you're doing $\infty$-topos theory inside set theory your set theory must have an 1-accessible cardinal?

dusko (Mar 26 2021 at 07:54):

John Baez said:

David Michael Roberts said:

Yes, they are! There's another recent paper that shows that once you have an elementary oo-topos a la Mike, you get not just an inaccessible, but a 1-inaccessible.

That's crazy! When y'all were talking about "getting an inaccessible", it seemed to make sense, because I thought it was just saying that to model homotopy types we need a bunch of infinite things closed under all sorts of operations familiar from set theory and topology. But "getting a 1-inaccessible" means we get an infinite tower of inaccessible cardinals, in a very strong sense. If you can provide any intuition about that, it'd be great.

this may have nothing to do with the cardinalities in higher toposes, but it would be nice if it does.

inaccessibility is the closure under all operations that can be obtained by iterating the previous operations (a la ackermann in finite arithmetic, or doner-tarski for the transfinite). so if an algebraic theory is closed under all iterations of its operations, then the inaccessibility (ie the closure under the ackermann-doner-tarski function) implies the 1-inaccessibility (ie that the ackermann-doner-tarski function has a fixpoint in it).

i don't know many algebraic theories that are closed under all iterations of their operations, but i know one. the structure of a monoidal computer is like a cartesian closed category, but for intensional computation, where a function does not have a unique abstraction, but corresponds to lots of programs. instead of the right adjoint of every product, there is a single object, the "programming language", which is a weak right adjoint of all products --- i.e. you can program functions of arbitrary types using this object. to prove that being a monoidal computer is a property of a category (like being cartesian closed is), we need to prove a version of the hartley rogers' theorem that any two programming languages are computably isomorphic. but the hartley rogers' thm uses the well-ordering of the programming language, so i wanted to classify which ordinals can always be programmed. and the iterations provide programs for anything below $\varepsilon_0$. the inaccessibility arises by transitioning from the ordinals to the cardinals.

sorry if this is totally unrelated with $(\infty,1)$-toposes, but i think of program transformers as 2-cells, and there are program transformers between program transformers, and so on. i tend to think of the $\infty$-structures as the layers of articulation in general... there is a sort of geometry in it all.

John Baez (Mar 26 2021 at 14:37):

Wow, that sounds cool! I know a bit about the theory of computable ordinals, but I don't know what "a weak right adjoint of all products" means.

Mike Shulman (Mar 26 2021 at 15:13):

John Baez said:

By "outside", do you mean if you're doing $\infty$-topos theory inside set theory your set theory must have an 1-accessible cardinal?

I mean if the collection of objects of your $\infty$-topos is a set, then that set must be 1-inaccessibly large. Generally when doing category theory we choose some size of collections to mark the boundary between what we call "small" and what we call "large". So for instance $\rm Set$ is the category of all small sets, and it itself is a large category. Every Grothendieck ($\infty$-)topos is also a large category of small objects. Sometimes people take the small/large boundary to be the same as the set/class boundary, so that large categories have a proper class of objects; if that's the choice you make, then having enough universes in an $\infty$-topos doesn't imply there is any set that's 1-inaccessible, only that "the proper class cardinal is 1-inaccessible" (which is just another way of stating the axiom of universes). But other times people say that they fix a particular inaccessible cardinal (which is itself a set) and take "small" to mean a set smaller than that cardinal and "large" to mean a set larger than that cardinal; if that's the choice you make, then having enough universes in an $\infty$-topos means that that particular fixed inaccessible must i nfact be 1-inaccesible.

dusko (Mar 26 2021 at 19:07):

John Baez said:

Wow, that sounds cool! I know a bit about the theory of computable ordinals, but I don't know what "a weak right adjoint of all products" means.

instead of the natural bijections ${\cal C}(X,B^A) \cong {\cal C}(X\times A,B)$ we have an object $P$ with natural surjections ${\cal C}(X,P) \to {\cal C}(X\times A,B)$. that we can then construct a weak NNO like in lambda calculus and do recursion etc is probably unsurprising. but that there is algebraic lattice enrichement, approximating computable functions by finite fragments (by the myhill-shepherdson thm, from which domain theory started) makes it tighter. finding that the ordinal arithmetic just emerges by programming iterative program computations was hard to believe, and made me check very carefully, and my inaccessible cardinal friends re-checked it, and it does.

John Baez (Mar 26 2021 at 19:46):

So there's a single object $P$ such that for all $A, B$ there exists a natural surjection

$\phi_{A,B} : C(-,P) \to C(- \times A, B) ?$

I want to makes sure I have the quantifiers right.

David Michael Roberts (Mar 27 2021 at 11:13):

Mike Shulman said:

Sometimes people take the small/large boundary to be the same as the set/class boundary, so that large categories have a proper class of objects; if that's the choice you make, then having enough universes in an $\infty$-topos doesn't imply there is any set that's 1-inaccessible, only that "the proper class cardinal is 1-inaccessible" (which is just another way of stating the axiom of universes).

Oh, ok! I see now why you say "misleadingly written". Thanks for explaining.

dusko (Mar 27 2021 at 21:26):

John Baez said:

So there's a single object $P$ such that for all $A, B$ there exists a natural surjection

$\phi_{A,B} : C(-,P) \to C(- \times A, B) ?$

I want to makes sure I have the quantifiers right.

yes. the images of $id_P$ are the universal evaluators for each pair of types. ((the church-turing thesis says that they can be implemented like this or like that, but this general signature of all implementation allows deriving about half of the hartley rogers' book, or the first and the last part of odifreddi I. i have been teaching computability and complexity to undergrads in this form for 12 years, and could share the textbook with interested readers.))

André Videla (Mar 28 2021 at 02:44):

I have a quesiton about Natural numbers so I'll hijack this thread for a bit. Why do we need NNO? can't we define natural numbers in terms of a single object and identity arrows for Successor where the composition of successors builds greaters natural numbers? What's missing from this definition that NNO provide?

David Michael Roberts (Mar 28 2021 at 06:58):

So something like how lambda calculus does it? All these composites are "external", though, not indexed by something in the topos, at least a priori. I think the universal property might be tricky.

Fawzi Hreiki (Mar 28 2021 at 07:07):

André Videla said:

I have a quesiton about Natural numbers so I'll hijack this thread for a bit. Why do we need NNO? can't we define natural numbers in terms of a single object and identity arrows for Successor where the composition of successors builds greaters natural numbers? What's missing from this definition that NNO provide?

You're missing recursion/induction. There's nothing stopping these 'natural numbers' from just being the singleton set with the identity function as 'successor'

Fawzi Hreiki (Mar 28 2021 at 07:08):

That's precisely the idea of a NNO: you want the universal such 'iterative system'

André Videla (Mar 28 2021 at 11:55):

ahhh I see thanks!