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: learning: questions

Topic: reference: initial algebras

Leopold Schlicht (Aug 11 2021 at 16:02):

Where can I find a self-contained and clean proof of the fact that each polynomial endofunctor on Set has an initial algebra?

Mike Shulman (Aug 11 2021 at 16:55):

A fairly clean argument is sketched at https://ncatlab.org/nlab/show/transfinite+construction+of+free+algebras, if you accept that polynomial functors are accessible.

Leopold Schlicht (Aug 12 2021 at 09:09):

Thanks for the link, but I don't know what an accessible functor is, so the page doesn't look self-contained and accessible to me. :P

David Michael Roberts (Aug 12 2021 at 11:20):

It's probably worth giving polynomial endofunctors on Set as an example at https://ncatlab.org/nlab/show/accessible+functor, then.

For endofunctors of $Set$ arising from $1 \leftarrow X\stackrel{g}{\to} Y \to 1$, we need to know $A \mapsto \Pi_g (X\times A)$ preserves $\kappa$-filtered colimits for some $\kappa$. This would follow from knowing $\Pi_g$ preserved filtered colimits, but maybe only the polynomial functor itself does. My guess is that we have to take $\kappa$ to be as small as it can be, i.e. $\kappa=\aleph_0$, and then use the fact filtered colimits commute with limits in $Set$.

David Michael Roberts (Aug 12 2021 at 11:30):

I'm being a little bit lazy, and a little bit busy, and not checking this myself, sorry!

Mike Shulman (Aug 12 2021 at 13:04):

$\Pi_g$ is accessible because any right or left adjoint between locally presentable categories is accessible.

David Michael Roberts (Aug 12 2021 at 15:30):

Added the examples Mike discussed to https://ncatlab.org/nlab/show/accessible+functor

Leopold Schlicht (Aug 17 2021 at 17:35):

Although I still haven't looked at the proofs, because they seem to be a bit too technical to be understandable in a short space of time, let me ask the following questions: I read (probably in the HoTT book) that some classical uses transfinite recursion can be replaced by (higher) inductive types. So I thought the proof that W-types exist must use transfinite recursion. But I just can't imagine transfinite recursion to be relevant here because all examples of W-types that come to my mind (such as natural numbers or binary trees) can simply be constructed as "the smallest set of strings over the alphabet of constructors satisfying ...".
Is the notion of a W-type (in Set) the same as the notion of an initial algebra of an endofunctor, or is it more general?
If transfinite recursion is necessary for the existence of W-types: is there some special class of W-types that don't need transfinite recursion to construct?

Reid Barton (Aug 17 2021 at 17:39):

If you have constructors of infinite arity then "strings" might not be enough. But in fact you can construct W-types in ZF for example using some kind of encoding of trees.

Leopold Schlicht (Aug 17 2021 at 17:56):

I see. But if one has only finite arities (but maybe infinitely many constructors!) one doesn't need transfinite recursion, right?

Also, what does ZF have but type theory not, that allows the first to construct W-types for itself while the latter needs to have their existence postulated via additional rules of inference?

Reid Barton (Aug 18 2021 at 13:41):

Leopold Schlicht said:

I see. But if one has only finite arities (but maybe infinitely many constructors!) one doesn't need transfinite recursion, right?

In the finite arity case, even the transfinite recursion construction doesn't need much. You only need to build a sequence $A_0 \to A_1 \to \cdots$ of length $\omega$, and doing this constructively isn't a problem.

The subtlety is in the infinite arity case. In that case, the transfinite recursion construction needs to continue up to some ordinal whose cofinality exceeds the arities of all constructors, and constructing that ordinal can be a problem: even in ZF, which is a very mild sort of "non-classicality", it's (probably?) consistent that there is no ordinal of uncountable cofinality. Nevertheless, the construction of W-types via trees still works in ZF even in the infinite arity case.

Reid Barton (Aug 18 2021 at 13:45):

Leopold Schlicht said:

Also, what does ZF have but type theory not, that allows the first to construct W-types for itself while the latter needs to have their existence postulated via additional rules of inference?

That probably depends on which particular type theory you consider, but one issue is the impredicative-style definition "the smallest set such that ...".
Also, in a type theory context you usually want W-types to have computation rules which are definitional equalities, and it seems unlikely that you could get those through this kind of construction.

Cody Roux (Aug 18 2021 at 18:30):

Reid Barton said:

even in ZF, which is a very mild sort of "non-classicality", it's (probably?) consistent that there is no ordinal of uncountable cofinality. Nevertheless, the construction of W-types via trees still works in ZF even in the infinite arity case.

Just take the ordinal of size ${\cal P}({\cal P}(\mathbb{N}))$!

I'm not actually sure how you'd build W-types otherwise.

Reid Barton (Aug 18 2021 at 18:37):

Cody Roux said:

the ordinal of size ${\cal P}({\cal P}(\mathbb{N}))$

But you need choice to know that there is an ordinal of that size, right?

Reid Barton (Aug 18 2021 at 18:50):

There is a construction of W-types in any topos with natural numbers object in Words, free algebras, and coequalizers, summarized informally starting on page 121.

Mike Shulman (Aug 18 2021 at 19:28):

As Reid said, you can construct W-types either from transfinite recursion or from powersets. In particular, the latter shows that they exist in any topos, which is much a weaker assumption than ZF. Ordinary predicative type theory doesn't have either one, so W-types have to be postulated. However, powersets don't suffice to construct higher inductive types, as some of them can't even be constructed in ZF; to get those it seems you have to use transfinite recursion or else postulate them.

David Michael Roberts (Aug 19 2021 at 11:10):

It's consistent with ZF that every uncountable cardinal is singular, but that is not the same as saying they all have countable cofinality. But I'm not sure which way it falls.

David Michael Roberts (Aug 19 2021 at 11:12):

Aha, here's the answer: https://math.stackexchange.com/questions/416218/in-zf-does-there-exist-an-ordinal-of-provably-uncountable-cofinality

David Michael Roberts (Aug 19 2021 at 11:16):

The standard law of headlines applies to that question

Cody Roux (Aug 19 2021 at 21:04):

Reid Barton said:

Cody Roux said:

the ordinal of size ${\cal P}({\cal P}(\mathbb{N}))$

But you need choice to know that there is an ordinal of that size, right?

I don't think so: you can take the set of well-orders over some set, and that set itself is well ordered without choice, of the "right" cardinality.

Cody Roux (Aug 19 2021 at 21:06):

Wait, I guess not, per David Robert's link. Huh.

Cody Roux (Aug 19 2021 at 21:06):

But there is an ordinal with countable cofinality? I wonder why the proof doesn't generalize.

Mike Shulman (Aug 20 2021 at 00:46):

The ordinal with countable cofinality, namely $\omega$, is asserted to exist by its own axiom. (-:

Leopold Schlicht (Aug 21 2021 at 18:24):

Thanks all!

What are the minimal prerequisites a Martin-Löf-type type theory needs to satisfy in order to be able to construct W-types?

Mike Shulman said:

As Reid said, you can construct W-types either from transfinite recursion or from powersets.

But isn't the proof using power sets Reid sketched also based on transfinite recursion?
Reid Barton said:

But in fact you can construct W-types in ZF for example using some kind of encoding of trees.

Can you make that more precise?

Mike Shulman (Aug 22 2021 at 00:12):

Leopold Schlicht said:

What are the minimal prerequisites a Martin-Löf-type type theory needs to satisfy in order to be able to construct W-types?

When working in type theory, usually we just assert that things like W-types exist. You probably aren't going to be able to construct them with a definitional computation rule from anything else. If you're okay with a typal computation rule, then you can construct them in the same ways you do in set theory, from transfinite recursion (using choice) or power sets (using propositional resizing).

But isn't the proof using power sets Reid sketched also based on transfinite recursion?

No. Reid pointed to a proof in Blass's paper Words, free algebras, and coequalizers, and there's also a sketch in Moerdijk-Palmgren Wellfounded trees in categories. In particular, they show how to encode trees using functions and powersets.

Leopold Schlicht (Aug 23 2021 at 18:35):

Thanks! I would really like to know the two proofs, but unfortunately I am not able to quickly extract the ideas from the two papers (I don't have the time to read them in detail).

Cody Roux (Aug 23 2021 at 21:50):

Mike Shulman said:

The ordinal with countable cofinality, namely $\omega$, is asserted to exist by its own axiom. (-:

I'm confused about the definition of cofinality I guess: I thought $\Omega$ was the least ordinal with countable cofinality: that is the smallest ordinal such that every function $A \rightarrow \Omega$ has an upper bound for countable $A$.

Certainly this ordinal exists in ZF (Andre Hirshowitz taught me this way back in the day in Nice!)

Zhen Lin Low (Aug 23 2021 at 22:16):

The ordinal you describe is an initial ordinal, i.e. its cofinality is itself. In particular it does not have countable cofinality. The least ordinal with countable cofinality is $\omega$, a.k.a. the first infinite ordinal.

Mike Shulman (Aug 24 2021 at 03:44):

Specifically, your $\Omega$, which is usually written $\omega_1$, is the least ordinal with uncountable cofinality.

Cody Roux (Aug 24 2021 at 14:43):

So now I'm really confused: I thought you could take the set of well-orders $O\subseteq\mathbb{N}$, and this set had provably uncountable cofinality, in ZF.

This contradicts the linked result. What is failing here? Is it the "provably", is it the "uncountable" or is it "you can take the set" (surely not that one)?

Zhen Lin Low (Aug 24 2021 at 14:49):

If we take what is written there at face value, what fails is "provably". $\omega_1$ is provably uncountable, of course.

Reid Barton (Aug 24 2021 at 15:47):

I guess you mean for the well-orders $O$ to themselves be ordered by order type. Since there are distinct well-orders of the same order type, this is only a preorder. It seems plausible that this preorder has countable cofinality provably in ZF by some kind of $\mathbb{N} \times \mathbb{N} \cong \mathbb{N}$ argument. However, when we form the quotient by the "same order type" relation to get a partial order (hence an actual ordinal), the result might not have countable cofinality any more. The reason is that we need choice to pass from a countable sequence in the quotient (for which we are supposed to find an upper bound) to a countable sequence in the original preorder.

Cody Roux (Aug 24 2021 at 15:50):

Aaah I see. Thanks @Reid Barton !

Leopold Schlicht (Aug 24 2021 at 16:27):

Can the transfinite recursion proof of the existence of W-types be phrased as an application of Zorn's lemma? (Can each transfinite recursion proof be phrased as an application of Zorn's lemma? Probably not, but due to my limited experience I haven't yet seen a counterexample.)

Cody Roux (Aug 24 2021 at 17:26):

Now that I look at the SO question more closely; it only talks about ordinals with uncountable cofinality. Does the answer also exclude all WF posets? Your comment makes it sound like it does.

Cody Roux (Aug 24 2021 at 17:46):

Leopold Schlicht said:

Can the transfinite recursion proof of the existence of W-types be phrased as an application of Zorn's lemma? (Can each transfinite recursion proof be phrased as an application of Zorn's lemma? Probably not, but due to my limited experience I haven't yet seen a counterexample.)

Most likely yes, or at least, as a consequence of Zorn's Fixed Point Theorem (see here) but there are other aspects to consider, e.g. how many ordinals you can prove exist, which seem more important to me than whether or not you use choice (my previous questions/comments notwithstanding).

A particularly crucial one is the predicative/impredicative distinction.

Mike Shulman (Aug 25 2021 at 03:00):

Well, since Zorn's lemma is equivalent over ZF to transfinite recursion and to all other forms of the axiom of choice, the answer must be trivially yes. But I doubt offhand that it looks very natural when written in terms of Zorn's lemma.

Leopold Schlicht (Aug 25 2021 at 14:57):

Thanks!

Leopold Schlicht (Aug 29 2021 at 13:55):

Let $C$ be a $\mathcal U$-set of constructors and $a\colon C\to\mathcal U$ a function assigning an index set to each constructor. We want to define the W-type $T$ that corresponds to this "branching signature" $(C,a)$. We proceed by transfinite induction:

• $T_0:=\empty$;
• $T_{\alpha+1}:=\sum_{c\colon C}a(c)\to T_\alpha$ (this can be thought of as the set of all formal expressions $c((e_i)_{i\colon a(c)})$, where $c$ is a constructor and the $e_i$ are elements of $T_\alpha$) for each ordinal number $\alpha$;
• $T_\lambda := \sum_{\alpha < \lambda} T_\alpha$ for each limit ordinal $\lambda$.

Then we can let $T:=\sum_{\alpha\colon\mathrm{Ord}} T_\alpha$. But this $T$ lives in a universe bigger than $\mathcal U$. So we need to stop our transfinite recursion at a specific ordinal number. Which one?

How can such an argument be formalized in Martin-Löf type theory? Ordinal numbers are usually discussed in a material set theory. (I know that the HoTT book discusses ordinals, but as far as I can see, that approach exploits univalence, which basically enables one to define an ordinal as a well-ordered set, without needing to consider equivalence classes.) Also, how can one construct the ordinal at which one stops the transfinite recursion in MLTT?

Note that the above argument uses the "axiom of replacement": the universe is closed under $\sum$. So I can't imagine that one can construct $T$ just using power sets and functions (or in an arbitrary elementary topos) by encoding it as a set of trees. But as you told me this is possible. Can somebody give me a sketch of the argument?

Reid Barton (Aug 29 2021 at 14:02):

You should just read the paper by Blass I linked above, starting at page 121. The construction could not be summarized more concisely here.

Mike Shulman (Aug 29 2021 at 14:43):

Reid's answer pertains to your final question about sets of trees. The construction of W-types in a topos does not proceed by a transfinite iteration, but "directly".

Mike Shulman (Aug 29 2021 at 14:44):

For the first, one must first of all assume an axiom of choice. In this case, the standard argument works just fine for all parts of the proof. Univalence is not needed; the only important property of "ordinals" in this argument is that they are well-ordered sets.

Leopold Schlicht (Aug 31 2021 at 20:34):

Mike Shulman said:

For the first, one must first of all assume an axiom of choice. In this case, the standard argument works just fine for all parts of the proof. Univalence is not needed; the only important property of "ordinals" in this argument is that they are well-ordered sets.

Alright, thanks. But at which ordinal does the transfinite recursion I described stop?

Mike Shulman (Aug 31 2021 at 21:00):

At any ordinal whose cofinality is greater than $sup_c |a(c)|$.

Leopold Schlicht (Aug 31 2021 at 21:03):

Can such an ordinal be constructed more directly, so that one doesn't have to know what cofinality means? :-)

Leopold Schlicht (Aug 31 2021 at 21:18):

Reid Barton said:

You should just read the paper by Blass I linked above, starting at page 121. The construction could not be summarized more concisely here.

I don't see any mathematical construction being described in the paragraphs starting at page 121. The only very rough idea I can extract is that one encodes an element of a W-type using a set of positions and a function from that set to the set of constructors/arguments. But the example given on page 122 is totally confusing and not very enlightening: that's a tree in which each constructor has finite arity, so one could just as well encode it as a finite string. So I didn't get the point when I first skimmed through the paper. The paper goes on encoding the whole construction in an arbitrary elementary topos -- but I'd like to see the construction being carried out in ordinary mathematical language.
I doubt that's the most concise description possible. :-)

Leopold Schlicht (Aug 31 2021 at 21:19):

@Mike Shulman So one doesn't need replacement in the proof of the existence of W-types?

Mike Shulman (Aug 31 2021 at 21:26):

Leopold Schlicht said:

Can such an ordinal be constructed more directly, so that one doesn't have to know what cofinality means? :-)

The successor cardinal of $sup_c |a(c)|$ works. (All assuming choice, of course.)

Mike Shulman (Aug 31 2021 at 21:27):

Leopold Schlicht said:

Mike Shulman So one doesn't need replacement in the proof of the existence of W-types?

One doesn't need replacement to prove that W-types exist. But the particular proof you are talking about using a transfinite iteration does use replacement.

Mike Shulman (Aug 31 2021 at 21:27):

Mike Shulman said:

Leopold Schlicht said:

Can such an ordinal be constructed more directly, so that one doesn't have to know what cofinality means? :-)

The successor cardinal of $sup_c |a(c)|$ works. (All assuming choice, of course.)

But I doubt you would be able to prove that this works without essentially invoking cofinality.

Mike Shulman (Aug 31 2021 at 21:32):

Leopold Schlicht said:

the example given on page 122 is totally confusing and not very enlightening: that's a tree in which each constructor has finite arity, so one could just as well encode it as a finite string.

One could, but in this paragraph he is not encoding it that way. Instead he is using it as an example to describe a general encoding that works for infinite arities as well.

Leopold Schlicht (Sep 01 2021 at 14:36):

Thanks!
Mike Shulman said:

At any ordinal whose cofinality is greater than $sup_c |a(c)|$.

Really any ordinal greater than ...? I would think there's a problem when choosing a very big ordinal: as $\alpha$ increases, the cardinality of $T_\alpha$ gets bigger and bigger -- maybe bigger than the true $T$. (Although I don't know whether cofinality is monotone, so this could be the reason for my confusion.)
Mike Shulman said:

The successor cardinal of $sup_c |a(c)|$ works. (All assuming choice, of course.)

Why does one need choice here?
Mike Shulman said:

One could, but in this paragraph he is not encoding it that way. Instead he is using it as an example to describe a general encoding that works for infinite arities as well.

I see. :-)

Mike Shulman (Sep 01 2021 at 14:50):

Oh, I see now, your original definition of $T$ was wrong. You have to take colimits at limit stages, not coproducts. Otherwise you end up with duplicated stuff already at $\alpha=\omega$. The colimits are what prevent the size from getting out of control: you continue adding new stuff, but after a point all of it gets identified with stuff you already had.

Mike Shulman (Sep 01 2021 at 14:50):

Cofinality is not monotone: $\aleph_n$ has cofinality $\aleph_n$, but $\aleph_\omega$ has cofinality $\omega=\aleph_0$.

Mike Shulman (Sep 01 2021 at 14:51):

One needs choice because without choice, it's possible that all infinite cardinals are singular, so there may not be any ordinal that works.

Leopold Schlicht (Sep 03 2021 at 17:48):

Ah, thanks!