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: theory: type theory

Topic: inductive type

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

The HoTT book (specifically chapter 5) acts like there is a concept of "inductive type", of which the notion of a "W-type" is a special case:

So far, we have been discussing only particular inductive types: 0, 1, 2, N, coproducts, products, Σ-types, W-types, etc.

What would be an example of an inductive type that is not a W-type? I always thought of "W-type" as an already quite general notion of the idea of an "inductive type".

Spencer Breiner (Aug 12 2021 at 12:16):

Higher inductive types, maybe?

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

The natural numbers are one example. A W-type has only one constructor, while Nat has two. There is a W-type that "encodes" Nat (assuming we already have 2, at least), but they are different.

Spencer Breiner (Aug 13 2021 at 13:23):

Could someone say a bit more about the distinction, failure and/or encoding?

This is a bit confusing, as the first example on the nLab page says "The most basic W-type is the natural numbers." Presumably this is in reference to the alternative definition there of W-types for Type Theory (we are in the type theory thread after all).

James Wood (Aug 13 2021 at 14:24):

Perhaps Mike's point is that ℕ and W2[0,1] are only equivalent, so at the very intensional level of the syntactic rules of type theory, they literally have different rules. In fact, the equivalence relies on function extensionality, so they aren't equivalent in plain MLTT. Relatedly, not every pair of 0s of W2[0,1] is definitionally equal. The canonical 0 is sup 0 λ(), but not every f : 0 → U is definitionally equal to λ() (i.e, rec₀).

Mike Shulman (Aug 13 2021 at 15:24):

Yes, this is discussed in section 5.3 and at the beginning of section 5.5 of the HoTT Book.

Mike Shulman (Aug 13 2021 at 15:24):

Spencer Breiner said:

This is a bit confusing, as the first example on the nLab page says "The most basic W-type is the natural numbers."

I think that's a mistake on the nLab, thanks for pointing that out.

Leopold Schlicht (Aug 13 2021 at 16:51):

Thanks!
Mike Shulman said:

A W-type has only one constructor

I don't understand this, because the branching signature can consist of several labels. I'm confused. :-)

Cody Roux (Aug 13 2021 at 19:59):

The "tag" of the constructor will always be the same, but of course you can invoke that constructor with several different arguments to _encode_ an inductive with different constructors, which is what @Mike Shulman is suggesting, I think.

Mike Shulman (Aug 13 2021 at 20:09):

Yes, that's the point. It's the difference between two elements of a type $A$, on one hand, and a function $2\to A$, on the other.

Leopold Schlicht (Aug 14 2021 at 15:01):

I don't get it. What does it mean that the tag of the constructur will always be the same? Also, I don't think there's a difference between two elements of type $A$ and a function $2\to A$, since there's a bijection $A^2\cong(2\to A)$. :P Of course, you know that, but I'm not able to interpret the sentence in any other sensible way.

James Wood (Aug 14 2021 at 15:27):

I suppose the question you're really interested in asking is whether every strictly positive functor on types can be encoded (up to equivalence) as $X \mapsto \Sigma_{a : A} (B\,a \to X)$ by some choice of $A$ and $B$. I believe so, but I haven't really thought it through.

James Wood (Aug 14 2021 at 15:32):

I suppose you could argue that $X \mapsto \lVert X \rVert$ is strictly positive, but let's rule that out for now.

Mike Shulman (Aug 14 2021 at 16:38):

There is a bijection, but they are not definitionally the same set. The distinctions we're talking about here are finer than up-to-isomorphism.

Leopold Schlicht (Aug 15 2021 at 11:22):

Ah, I see, thanks.
But I don't yet see how this connects to a W-type having only one constructor.

Mike Shulman (Aug 15 2021 at 14:06):

A general inductive type $I$ has a finite list of constructors, say $c_i : P_i(I) \to I$ where $P_i$ is some functor for $1\le i\le n$. For a W-type we have $n=1$. We can take $P_1(I) = 2$ for a W-type, but this would be different from an inductive type where $n=2$ and $P_1(I) = P_2(I)=1$.

Leopold Schlicht (Aug 15 2021 at 15:40):

Ah, thanks!

Ulrik Buchholtz (Aug 15 2021 at 17:27):

BTW, if we have $\eta$ for the unit type and for $\Sigma$-types (but no function extensionality), then the natural numbers can be recovered as a W-type, satisfying all the rules, including the judgmental computation rule. This is in Jasper Hugunin's Why not W?.

David Michael Roberts (Aug 15 2021 at 21:10):

What's the category-theoretic/semantic analogue of those assumptions?

Mike Shulman (Aug 16 2021 at 00:53):

Ulrik Buchholtz said:

BTW, if we have $\eta$ for the unit type and for $\Sigma$-types (but no function extensionality), then the natural numbers can be recovered as a W-type, satisfying all the rules, including the judgmental computation rule. This is in Jasper Hugunin's Why not W?.

This is a nice result, but I don't think it's correct to say that the natural numbers are recoverd as a W-type. Rather, Jasper defines a predicate by recursion on the W-type corresponding to nat, picking out a "subtype" of it that satisfies the judgmental computation rule.

Mike Shulman (Aug 16 2021 at 00:54):

David Michael Roberts said:

What's the category-theoretic/semantic analogue of those assumptions?

It's hard to write down models where $\eta$ for unit and $\Sigma$ doesn't hold. It basically means that fibrations contain identity maps and are closed under composition.

Ulrik Buchholtz (Aug 16 2021 at 11:06):

Mike Shulman said:

This is a nice result, but I don't think it's correct to say that the natural numbers are recoverd as a W-type. Rather, Jasper defines a predicate by recursion on the W-type corresponding to nat, picking out a "subtype" of it that satisfies the judgmental computation rule.

That's a good point: I guess we should say that this result is a reduction of natural numbers to W-types in this setting. It seems like a general technique that might similarly reduce all inductive types to W-types.

Mike Shulman (Aug 16 2021 at 12:18):

Yes, it does.

Patrick Nicodemus (Aug 18 2021 at 06:03):

This discussion has been helpful. I'd like to read about this in more detail. Other than the HoTT book, can you recommend sources for the theory of inductive types?

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

The approach taken in the HoTT Book is extended and developed further in a series of papers by Awodey, Gambino, and Sojakova: https://arxiv.org/abs/1201.3898, https://arxiv.org/abs/1402.0761, https://arxiv.org/abs/1504.05531.

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

There are some more references at the nlab pages https://ncatlab.org/nlab/show/W-type and https://ncatlab.org/nlab/show/inductive+type.