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: 'Cumulative hierarchy without truncation' in HoTT

James Hanson (Nov 06 2023 at 03:10):

Consider a modification of Definition 10.5.1 in the HoTT book where we just don't truncate (as in don't truncate in the definition of extensionality and don't add a $0$-truncation constructor). Is the resulting higher inductive type inequivalent to $V$? If so, how do you show this?

I'll try to write out what I mean explicitly, but I might not have terminology or notation completely down. I'm talking about the higher inductive type $W$ with the following constructors:

• For any $A : \mathcal{U}$ and $f : A \to W$, there is an element $\mathrm{set}(A,f) : W$.
• For any $A,B : \mathcal{U}$, $f : A \to W$, $g : B \to W$, $h : \prod_{(a : A)}\sum_{(b : B)}f(a)=_W g(b)$, and $i : \prod_{(b:B)}\sum_{(a:A)}f(a) =_W g(b)$, there is a path $\mathrm{ext}(A,B,f,g,h,i) : \mathrm{set}(A,f) =_W \mathrm{set}(B,g)$.

I'm guessing that it will be fairly immediate that $W$ is not $0$-truncated. Assuming it's not, is it also true that the $0$-truncation of $W$ is not equivalent to $V$, and if so how do you show this?

Morgan Rogers (he/him) (Nov 06 2023 at 08:32):

Proving that a type is not 0-truncated doesn't sound like it would necessarily be straightforward.

Kenji Maillard (Nov 06 2023 at 09:39):

I would expect that it depends on the universe $\mathcal{U}$, for instance if $\mathcal{U}$ happens to be a universe of propositions ($-1$-types), it might well be $0$-truncated, and I would guess that $W$ is $0$-truncated in that case.

James Hanson (Nov 06 2023 at 14:15):

Morgan Rogers (he/him) said:

Proving that a type is not 0-truncated doesn't sound like it would necessarily be straightforward.

Yeah I guess I shouldn't have said that because this question came to me because in my mind there's a fairly intuitive proof by transfinite induction that this ought to construct 'the same thing' as the ordinary V (at least on the level of objects). I'm just not sure if it actually goes through in HoTT.

Chris Grossack (they/them) (Nov 06 2023 at 15:25):

I don't have an actual proof that truncation is necessary, but here's a slightly imprecise argument:

a HIT is the free type on some data. So there shouldn't be any identifications that aren't forced to be there. Now consider two maps

• $f : \mathbb{2} \to \mathbb{V}$ sending $T \mapsto \emptyset$ and $F \mapsto \{ \emptyset \}$
• $g = f \circ \text{not}$

We want to identify ($\text{set}(-)$ of) these maps with their images in $\mathbb{V}$, so these should represent equal elements of $\mathbb{V}$, which is why your second bullet adds a path $\text{set}(f) =_\mathbb{V} \text{set}(g)$.

But, in the absence of truncation, I don't see why this path should be forced to be equal to the reflexivity path on $\{ \emptyset, \{ \emptyset \} \}$.

Chris Grossack (they/them) (Nov 06 2023 at 15:26):

Coupled with the fact that the people writing the HoTT book thought quite hard about these things, I would be surprised if they truncated unnecessarily

Chris Grossack (they/them) (Nov 06 2023 at 15:29):

That said, as of earlier this year, @Tom de Jong and collaborators showed that the type of (marked) MEWOs is equivalent to $\mathbb{V}$. See definition 47 here, through the end of the paper. Naively to me, it looks like this definition doesn't enforce any kind of truncation. Instead, we get set-ness of any given MEWO "for free" from its well order.

I'm sure he'll have lots to say about this topic ^_^

James Hanson (Nov 06 2023 at 15:42):

Chris Grossack (they/them) said:

I don't have an actual proof that truncation is necessary, but here's a slightly imprecise argument:

a HIT is the free type on some data. So there shouldn't be any identifications that aren't forced to be there. Now consider two maps

• $f : \mathbb{2} \to \mathbb{V}$ sending $T \mapsto \emptyset$ and $F \mapsto \{ \emptyset \}$
• $g = f \circ \text{not}$

We want to identify ($\text{set}(-)$ of) these maps with their images in $\mathbb{V}$, so these should represent equal elements of $\mathbb{V}$, which is why your second bullet adds a path $\text{set}(f) =_\mathbb{V} \text{set}(g)$.

But, in the absence of truncation, I don't see why this path should be forced to be equal to the reflexivity path on $\{ \emptyset, \{ \emptyset \} \}$.

I see the intuition here, but how do you actually prove the negation of the statement that these two paths are identical?

Chris Grossack (they/them) (Nov 06 2023 at 15:54):

James Hanson said:

I see the intuition here, but how do you actually prove the negation of the statement that these two paths are identical?

When I said "I don't have an actual proof that truncation is necessary, but here's a slightly imprecise argument", I meant that I don't know how to answer this question, haha

You would do it by building a map from your untruncated $\mathbb{V}$ to the universe (of course, by HIT-ness it suffices to say where each generator $\text{set}(f)$ goes and to ensure that equal things get sent to equal places). You would want to cleverly choose this map $\mathbb{V} \to \mathcal{U}$ so that these two identities go to provably distinct identities in the universe. This is a lot of data to keep track of, though, and I can't think of an "obvious" map to $\mathcal{U}$ that would work.

James Hanson (Nov 06 2023 at 15:58):

Do you have any intuition about the second question (whether truncating at the end is sufficient to get the ordinary V)?

Chris Grossack (they/them) (Nov 06 2023 at 16:07):

James Hanson said:

Do you have any intuition about the second question (whether truncating at the end is sufficient to get the ordinary V)?

Yeah, I think this should be true. The usual definition of $\mathbb{V}$ says to look at the free type so that

• $\text{set}(f)$ is a point in $\mathbb{V}$
• There's a path between $\text{set}(f)$ and $\text{set}(g)$ if their images agree
• For any $x,y : \mathbb{V}$, there's a unique proof that $x=y$.

If you take just the first two, you get a bigger free type, but then if you (freely) impose the third later (by 0-truncating), it should be the same as freely taking all 3 to start with. This is basically because adjoints compose.

Chris Grossack (they/them) (Nov 06 2023 at 16:08):

And this feels much easier to prove than your other question. You need to show that the truncation of $\mathbb{W}$ has the same universal property as the usual $\mathbb{V}$. This is the kind of thing that shouldn't be so hard to to just check.

Tom de Jong (Nov 06 2023 at 16:28):

Chris Grossack (they/them) said:

That said, as of earlier this year, Tom de Jong and collaborators showed that the type of (marked) MEWOs is equivalent to $\mathbb{V}$. See definition 47 here, through the end of the paper. Naively to me, it looks like this definition doesn't enforce any kind of truncation. Instead, we get set-ness of any given MEWO "for free" from its well order.

That's right. Extensionality implies your type is a set, see e.g. https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.Notions.html#extensionally-ordered-types-are-sets

I'm sure he'll have lots to say about this topic ^_^

Maybe, if I wasn't so busy :tear:

Tom de Jong (Nov 06 2023 at 16:29):

@Chris Grossack (they/them) Note that @James Hanson's condition does not really say that the image agree, because it uses $\Sigma$ over $\exists$, so you actually get maps between $A$ and $B$ (that respect $f$ and $g$).

James Hanson (Nov 06 2023 at 16:56):

@Tom de Jong So are you saying that W actually just is equivalent to V?

Mike Shulman (Nov 06 2023 at 19:13):

James Hanson said:

Do you have any intuition about the second question (whether truncating at the end is sufficient to get the ordinary V)?

I doubt this is provable, at least not constructively. If you're truncating as you go along, then there could be more functions $f:A\to V$ to put into the first constructor since you already know at that point that $V$ is 0-truncated. It's roughly the same issue with constructing free algebras for algebraic theories in the absence of choice: you can't put in all the generators first and then quotient by all the relations, because for an infinitary theory in the absence of choice, quotienting can create new possible inputs to the generators.

James Hanson (Nov 06 2023 at 19:43):

@Mike Shulman How hard do you think it would be to exhibit a model in which this fails?

Also, are you saying you think that with LEM for propositions it would work?

Mike Shulman (Nov 06 2023 at 20:19):

My guess is that what you'd need to make it work is the "strong axiom of choice" that every surjection whose codomain is a set has a section. I haven't tried to play around with models where these sorts of things fail. I don't know whether a simple $(\infty,1)$-topos model where AC fails would be enough to make this fail, or whether you need something fancier. In the case of algebraic theories, it seems you have to use some fancy set-theoretic models and maybe even large cardinals (the reference is Blass's paper "Words, free algebras, and coequalizers").

James Hanson (Nov 06 2023 at 20:34):

@Mike Shulman Do you think that there's an obvious embedding of V into the 0-truncation of my W or the other way around? Is one of them clearly 'bigger'?

Mike Shulman (Nov 06 2023 at 21:29):

I think there should be a map from the 0-truncation of your $W$ to the $V$ of the book. Since $V$ is a HIT with strictly more constructors than $W$, there should be a map $W\to V$ defined recursively to interpret each constructor of $W$ by the corresponding constructor of $V$. And then since $V$ is 0-truncated, that map should descend to $\Vert W\Vert_0$.

Mike Shulman (Nov 06 2023 at 21:29):

Without having thought about it for more than 10 seconds, I don't have a guess about whether that map is an embedding.

Mike Shulman (Nov 06 2023 at 21:33):

Chris Grossack (they/them) said:

But, in the absence of truncation, I don't see why this path should be forced to be equal to the reflexivity path on $\{ \emptyset, \{ \emptyset \} \}$.

I share that intuition, but it's not at all obvious to me how to go about proving that it isn't. In particular, we can't hope to define a map $V\to \mathcal{U}$ sending $\mathsf{set}(A,f)$ to $A$, since that wouldn't respect the paths inserted by the second constructor.

James Hanson (Nov 06 2023 at 21:48):

Mike Shulman said:

I think there should be a map from the 0-truncation of your $W$ to the $V$ of the book. Since $V$ is a HIT with strictly more constructors than $W$, there should be a map $W\to V$ defined recursively to interpret each constructor of $W$ by the corresponding constructor of $V$. And then since $V$ is 0-truncated, that map should descend to $\Vert W\Vert_0$.

What I'm struggling with is that to me it feels like there should 'obviously' be an embedding of $V$ into $W$ by using the sets in $V$ as indexing types, but there's probably a gap in my mental picture.

Mike Shulman (Nov 06 2023 at 22:10):

How are you managing to quote people but mess up the math formatting in the quotation?

Mike Shulman (Nov 06 2023 at 22:10):

If you click "quote and reply" it fills in the quote for you with the correct math formatting.

Mike Shulman (Nov 06 2023 at 22:11):

At least, it does for me.

James Hanson (Nov 06 2023 at 22:12):

It must be the mobile app?

Mike Shulman (Nov 06 2023 at 22:13):

Huh. Someone should report that as a bug in the mobile app.

Mike Shulman (Nov 06 2023 at 22:13):

Anyway, you can't define a map $V\to W$ because $V$ has a 0-truncation constructor and $W$ isn't (known to be) 0-truncated, so there is nowhere to send that constructor.

Mike Shulman (Nov 06 2023 at 22:14):

And you can't define a map $V\to \Vert W\Vert_0$ because $\Vert W\Vert_0$ doesn't (as far as we know) admit the same constructors that $W$ does, so there's nowhere to send the first two constructors of $V$.

Tom de Jong (Nov 07 2023 at 08:52):

James Hanson said:

Tom de Jong So are you saying that W actually just is equivalent to V?

No, I'm not. All I'm saying is that if a type comes equipped with a prop-valued extensional relation, then that type is a set.