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: community: our work

Topic: Type theory vs set theory

Astra Kolomatskaia (Dec 05 2023 at 03:01):

I gave a talk last Friday in which I began by considering set theory. There are two perspectives on what set theory does. The first [more correct one] is that it's hard to give a convincing example of any mathematical concept that clearly sits outside of the comfort zone of being foundable in set theory. The second [naïve] one is that students in a typical intro to proofs course are taught set theory and then learn concepts such as functions and families and then go on to do math with these concepts, so one might think that set theory is an optimal framework for discussing such concepts

Astra Kolomatskaia (Dec 05 2023 at 03:02):

The talk was titled "diagram models", and the first example that I considered was taking a model of set theory [whatever that means] and replacing it with the model in which every object now denotes a pair of sets, i.e. the model Set × Set

Astra Kolomatskaia (Dec 05 2023 at 03:04):

After some discussion, the first observation made was that this "model" violates LEM. However, even if we work in a constructive set theory, I still think that this model violates extensionality, for any meaningful way that I can think of formulating extensionality with a global membership ∈ operation

Astra Kolomatskaia (Dec 05 2023 at 03:05):

However, all of the basic concepts of functions and families [i.e. pi-types and universes] make sense equally well in a diagram model

Astra Kolomatskaia (Dec 05 2023 at 03:06):

I then argued that type theory is the optimal framework for studying concepts like functions and families in maximal generality, such that if at any point in the future you have an idea for a new model, you automatically get All Of Mathematics Ever Written Down In Type Theory for free

Astra Kolomatskaia (Dec 05 2023 at 03:09):

v.s. in set theory, it would be hard to make the case that you could not give the construction of what is meant by the structure of such a model, viz. defining what is meant by a pair of sets and what it means to be a morphism between such pairs, but you would have to manually rewrite all of the mathematics that you wanted to port to this setting as it would not be an actual semantic model of the syntax of set theory

Astra Kolomatskaia (Dec 05 2023 at 03:13):

This was the intro and the rest of the talk was basically an elaboration of the concept of a Category With Families

Notification Bot (Dec 05 2023 at 04:26):

7 messages were moved here from #community: our work > Mike Shulman by Mike Shulman.

Mike Shulman (Dec 05 2023 at 04:28):

Interesting. My first question is in what sense the "model" of pairs of sets violates LEM? The topos $\rm Set\times Set$ is Boolean, so it satisfies LEM.

Astra Kolomatskaia (Dec 05 2023 at 04:53):

We can consider a multi-modal theory whose diagram mode interprets into $\mathsf{Set} \times \mathsf{Set}$ and that has modalities $\lozenge_0$ and $\lozenge_1$ that land in the discrete mode. I want to say that assuming LEM as an axiom (i.e. in the global context) in the diagram mode implies contradiction in the discrete mode

Astra Kolomatskaia (Dec 05 2023 at 04:54):

Consider $X = (\top, \bot)$

Astra Kolomatskaia (Dec 05 2023 at 04:57):

If we have $\ \vdash_{bm} X \to \bot\$ then $\ \vdash_{dm} \lozenge_0 X \to \lozenge_0\bot$, or equivalently $\ \vdash_{dm} \top \to \bot$, conversely given $\vdash_{bm} X$ we get $\ \vdash_{dm} \lozenge_1 X$ or $\ \vdash_{dm} \bot$. This is not an anti-classical result, but it shows that LEM cannot hold in an arbitrary context

Astra Kolomatskaia (Dec 05 2023 at 05:00):

This is just an extended way of saying that there is a diamond of four truth values

Mike Shulman (Dec 05 2023 at 05:03):

No, it doesn't show that LEM can't hold. It shows that $X$ doesn't hold in an empty context, and that $\neg X$ doesn't hold in an empty context, but it doesn't show that $X+\neg X$ can't hold in an empty context. And in fact if you work it out you can see that $X+\neg X \cong (\top,\top)$.

Mike Shulman (Dec 05 2023 at 05:05):

This is the difference betweeen a topos being Boolean and being two-valued. A Boolean topos is one whose subobject lattices are Boolean algebras; they could have lots of different elements, but as long as they are Boolean algebras, it holds in the internal logic of the topos that "every truth value is either true or false" because for every proposition $P$ the proposition $P\vee \neg P$ is equal to $\top$, even if $P$ itself is neither equal to $\top$ nor $\bot$.

Mike Shulman (Dec 05 2023 at 05:07):

A two-valued topos is one with exactly two subterminal objects. This is incomparable to Booleanness in general: a topos can be Boolean without being two-valued, or two-valued without being Boolean.

Astra Kolomatskaia (Dec 05 2023 at 05:07):

Oh, this is a good point. LEM would fail in $\mathsf{Set}^\to$, though, right?

Mike Shulman (Dec 05 2023 at 05:09):

Yes, LEM fails in $\rm Set^\to$, because there you have a truth value $U = (0\to 1)$ such that $U\neg \top$, but $\neg U = \bot$, so $U\vee \neg U = U \neq \top$.

Mike Shulman (Dec 05 2023 at 05:11):

Next question is how you were thinking of formulating extensionality. (-: One can build a model of set theory internal to any topos as well, with extensionality along with the other axioms. And in $\rm Set \times Set$ I think it will just result in pairs of ordinary sets.

Astra Kolomatskaia (Dec 05 2023 at 05:13):

I saw that in the HoTT book there is a construction of such a model V with a membership predicate $\in$ as a HIT, however a global extensionality axiom in the theory shouldn't be about a specific set of symbol meanings that you can construct

Astra Kolomatskaia (Dec 05 2023 at 05:14):

On the other hand, there isn't really a natural interpretation of what $\in$ means in type theory, is there?

Astra Kolomatskaia (Dec 05 2023 at 05:16):

Or at least, it is wrong to interpret elements as global elements

Mike Shulman (Dec 05 2023 at 05:18):

Right, type theory doesn't have a global $\in$. But that's a different thing from saying that extensionality is violated; by the latter I would understand that you have fixed a meaning of $\in$ and the resulting interpretation of the statement $\forall x y, ((\forall z. (z\in x \leftrightarrow z\in y))\to x=y)$ is false.

Astra Kolomatskaia (Dec 05 2023 at 05:22):

I guess that the original question is whether you could interpret every statement written in set theory as saying something about $\mathsf{Set} \times \mathsf{Set}$

Astra Kolomatskaia (Dec 05 2023 at 05:23):

What this would mean is secretly replacing every set with a pair of sets and every function with a pair of functions, as opposed to interpreting this inside of an inner model of set theory that could be constructed inside of $\mathsf{Set} \times \mathsf{Set}$

Mike Shulman (Dec 05 2023 at 05:23):

I think in the case of $\rm Set\times Set$ you could probably do that because it's so simple.

Mike Shulman (Dec 05 2023 at 05:24):

And I think that would end up coinciding with the model of set theory constructed in the usual way inside the topos $\rm Set\times Set$, just because everything you do in $\rm Set\times Set$ is "componentwise".

Mike Shulman (Dec 05 2023 at 05:25):

In particular, the truth value of $(x_0, x_1) \in (y_0, y_1)$ would be $(x_0\in y_0, x_1\in y_1)$.

Astra Kolomatskaia (Dec 05 2023 at 05:28):

Hmm, my intuitions probably came from thinking of a model of set theory as being something that looked analogous to the categorical semantics of type theory. So every set gets interpreted as an object in the category and such that you can talk about $X \vdash t : Y$

Astra Kolomatskaia (Dec 05 2023 at 05:29):

On the other hand, if you start constructing a model instead by explaining what $\in$ means, I think that you can effectively restrict to an inner construction of V in the topos

Astra Kolomatskaia (Dec 05 2023 at 05:31):

Having judgments in a context as being primitive is what I meant by "replacing every function with a pair of functions"

Astra Kolomatskaia (Dec 05 2023 at 05:32):

It still feels to me that something is lost from the richness of $\mathsf{Set} \times \mathsf{Set}$ if you start with $\in$. What do you think about this?

Mike Shulman (Dec 05 2023 at 05:32):

Set theory as usually formulated doesn't have a notion of "term", so if you're building a model of set theory you shouldn't expect to be able to talk about $X\vdash t:Y$. The fundamental structure of (membership-based) set theory is the predicate $\in$.

Mike Shulman (Dec 05 2023 at 05:34):

Obviously I'm not a real big fan of membership-based set theory myself for other reasons, but at a technical level I think it does capture basically all the internal logic of a topos when formulated carefully.

Astra Kolomatskaia (Dec 05 2023 at 05:36):

Could $\mathsf{Set}^\to$ be made into a model of constructive set theory?

Astra Kolomatskaia (Dec 05 2023 at 05:40):

Astra Kolomatskaia said:

It still feels to me that something is lost from the richness of $\mathsf{Set} \times \mathsf{Set}$ if you start with $\in$. What do you think about this?

I think my intuition here is that pi-types and universes in the membership based model don't coincide with their type theoretic counterparts

Astra Kolomatskaia (Dec 05 2023 at 05:41):

For pi-types, this is clear because the intro rule uses terms in a context, which we just don't have as a primitive notion

Mike Shulman (Dec 05 2023 at 05:43):

Well, when you're working in set theory, you define "pi-types" differently:

$$\Pi(A,B) = \left\{ f : A \to \bigcup_{a\in A} B(a) \;\middle|\; \forall a, f(a) \in B(a) \right\}.$$

Mike Shulman (Dec 05 2023 at 05:44):

They're characterized differently, because as you say set theory doesn't have the machinery to give type-theoretic intro/elim rules, but they turn out to be equivalent semantically.

Astra Kolomatskaia (Dec 05 2023 at 05:45):

I guess that they might actually be pi-types if you derive $X \vdash t : Y$ as being defined in terms of $\in$

Madeleine Birchfield (Dec 05 2023 at 05:46):

Mike Shulman said:

Well, when you're working in set theory, you define "pi-types" differently:

$$\Pi(A,B) = \left\{ f : A \to \bigcup_{a\in A} B(a) \;\middle|\; \forall a, f(a) \in B(a) \right\}.$$

On a side note, is that how one would define dependent products in ETCS or SEAR as well?

Mike Shulman (Dec 05 2023 at 05:46):

Astra Kolomatskaia said:

Could $\mathsf{Set}^\to$ be made into a model of constructive set theory?

A model of constructive set theory can be constructed from any topos. The HIT construction in the HoTT Book is a highbrow approach, but the more traditional one is to consider internal well-founded relations. This dates back to Cole, Mitchell, and Osius in the mid-20th century; I wrote a paper myself that does some systematization and comparison to category theoretic axiom systems.

Astra Kolomatskaia (Dec 05 2023 at 05:47):

That makes sense

Astra Kolomatskaia (Dec 05 2023 at 05:48):

Astra Kolomatskaia said:

I guess that they might actually be pi-types if you derive $X \vdash t : Y$ as being defined in terms of $\in$

Specifically $X \vdash Y \mathsf{type}$ means $Y$ is a family of sets over the elements of $X$ and $t$ means a dependent function, defined set theoretically

Mike Shulman (Dec 05 2023 at 05:49):

The main limitation is that these straightforward constructions don't always "see" the whole topos: they only see the part that can be equipped with well-founded relations. In a classical topos this is all of it, but in a constructive topos it could miss part. But there's a fancier approach due to Awodey, Butz, Simpson, and Streicher that is able to "see" the whole topos.

Mike Shulman (Dec 05 2023 at 05:49):

Astra Kolomatskaia said:

Specifically $X \vdash Y \mathsf{type}$ means $Y$ is a family of sets over the elements of $X$ and $t$ means a dependent function, defined set theoretically

Right: you basically start from your model of set theory and build a model of type theory in the usual way.

Astra Kolomatskaia (Dec 05 2023 at 05:50):

Mike Shulman said:

The main limitation is that these straightforward constructions don't always "see" the whole topos: they only see the part that can be equipped with well-founded relations. In a classical topos this is all of it, but in a constructive topos it could miss part. But there's a fancier approach due to Awodey, Butz, Simpson, and Streicher that is able to "see" the whole topos.

So, for example, extensionality would say that $(\top,\bot) = (\bot,\bot)$, right?

Mike Shulman (Dec 05 2023 at 05:50):

Madeleine Birchfield said:

On a side note, is that how one would define dependent products in ETCS or SEAR as well?

Not exactly, because ETCS and SEAR don't have a notion of non-disjoint union. But you can do something similar using a disjoint union.

Mike Shulman (Dec 05 2023 at 05:51):

Astra Kolomatskaia said:

So, for example, extensionality would say that $(\top,\bot) = (\bot,\bot)$, right?

No. $(\top,\bot)$ has no global elements, but that doesn't mean that $\forall z, (z\in (\top,\bot) \leftrightarrow z\in (\bot,\bot))$ holds internally.

Astra Kolomatskaia (Dec 05 2023 at 05:59):

What does the argument that $\lozenge_1~\big(\exists~z.~z \in (\top, \bot)\big) \equiv \exists~z.~z\in\bot$ say, if anything?

Mike Shulman (Dec 05 2023 at 06:06):

Well, it implies that $\exists z. z\in (\top,\bot)$ has no global elements, since any such global element would also yield a global element of $\exists z. z\in \bot$ in $\rm Set$.

Astra Kolomatskaia (Dec 05 2023 at 06:08):

Mike Shulman said:

No, it doesn't show that LEM can't hold. It shows that $X$ doesn't hold in an empty context, and that $\neg X$ doesn't hold in an empty context, but it doesn't show that $X+\neg X$ can't hold in an empty context. And in fact if you work it out you can see that $X+\neg X \cong (\top,\top)$.

I guess that the argument that I gave at the start breaks down in that its casework derives contradiction in $dm$ by way of using different modalities, so there is no unified modal function like $(p :^\lozenge \mathsf{LEM}~X) \to \bot$

Mike Shulman (Dec 05 2023 at 06:13):

I would have said it breaks down because LEM doesn't satisfy canonicity. Postulating $\vdash \forall P. P+\neg P$ doesn't tell you that for some particular $X$ you have either $\vdash X$ or $\vdash \neg X$.

Astra Kolomatskaia (Dec 05 2023 at 06:18):

Mike Shulman said:

Astra Kolomatskaia said:

Specifically $X \vdash Y \mathsf{type}$ means $Y$ is a family of sets over the elements of $X$ and $t$ means a dependent function, defined set theoretically

Right: you basically start from your model of set theory and build a model of type theory in the usual way.

Ok, then the observation is that if you start from a model of type theory, and construct an internal model of set theory, called $\mathsf{Set}$, then construct the derived model of set theory $\mathsf{Set} \times \mathsf{Set}$, and construct its internal model of type theory, then that construction does not agree with the diagram model construction on two points in type theory

Astra Kolomatskaia (Dec 05 2023 at 06:19):

At least not definitionally; would there be any equivalence?

Astra Kolomatskaia (Dec 05 2023 at 06:22):

We can also consider the construction [set theory] -> [type theory] -> [type theory] -> [set theory]

Mike Shulman (Dec 05 2023 at 06:31):

(Is it possible to move this to a different stream?)

Astra Kolomatskaia (Dec 05 2023 at 06:35):

I don't have permission to, but pressing m gives the interface for moving a whole thread

Mike Shulman (Dec 05 2023 at 06:45):

For a general diagram construction, I think neither of these squares commutes, because the direction [type theory] -> [set theory] is lossy as I mentioned earlier. (The other direction can be lossy too for weak set theories, but not for the stronger set theories used mostly in practice; chapter 9 of my paper is about this sort of question with type theory replaced by a "structural" set theory like ETCS.)

Mike Shulman (Dec 05 2023 at 06:46):

But I think in the simple case of $\rm Set\times Set$, the direction that starts with set theory is not lossy, because when a model of type theory is constructed from a model of set theory everything in it is well-founded, and that carries over to $\rm Set\times Set$ since everything is componentwise.

Mike Shulman (Dec 05 2023 at 13:41):

Astra Kolomatskaia said:

I don't have permission to, but pressing m gives the interface for moving a whole thread

I guess one thing we could do is move all the messages in this topic to a new one in some other stream, and rename this one back to your personal topic.