It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 494
- ACT Study Group 5
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 1
- Strategy 110
- Azimuth Project 1.1K

Options

At Mathematics Stack Exchange, I asked the question How do we know if two objects in a category are the same or not?

I received some very different answers. I am curious if anybody here might post a better answer before I choose one. I think the question I posed is helpful for learning about categories. Certainly, it is helpful for me.

I have been grappling with the realization that in category theory, a category like Grp, the category of groups, may have many objects that are the trivial group. So then I wonder, what are the limits, if any, on what such objects may be? One way to think about that is to ask, as I did, how do we know whether two objects in a category are the same or not.

The conclusion that I am drawing is that set theory and category theory are different ways of thinking. In set theory, we can appeal to the axiom of extensionality, which says that singletons {a} and {b} are the same iff a=b. But in the category Set, there is no concept of element. There are simply objects (sets) and arrows (set functions). There are no "singletons" as such, but we speak instead of the terminal objects. When are two objects the same? When they have the same identity morphism. Thus, in category theory, the identity morphism resolves the question of equality in the same way that, in set theory, the axiom of extensionality resolves it for sets.

Can I have a set Z that consists of a horse, cow and pig? In set theory, I cannot, because sets are built up from the empty set. We can't even have bijections with the set Z because it is not a mathematical object. Whereas in category theory, I believe that we can have such a set Z because the horse, cow and pig are irrelevant. What matters is that we have an object Z and we have the required arrows to all of the other objects.

There can be many set theories which may or may not lead to the same category Set. But the category Set doesn't have to be based on any set theory. It simply has objects and arrows which are related as we would expect sets to be related. So it is about formalizing and studying our expectations and not about any particular implementation. A set in the category Set doesn't actually have to have an element. That's not what makes it a set. What makes it a set is that it fulfills the expectations for a set as regards the composition of arrows. Which, in the case of a terminal object, means that there is a unique arrow to it from every set, and that to every set S it has a set of arrows whose cardinality matches that of S. And then those sets of arrows are also objects in Set and so on.

From my point of view, there are practically no limits on what might possibly be a set, and so in that sense, the category Set is not completely defined. But that seems by design.

So I'm inclined to select the answer that says to look at the identity morphism. But I may be in error. So I thought I would check here. Perhaps this is interesting. I had thought about related quandaries in my post here, Question: Internal structure vs. External relationships (the terminal objects of Cat and Set).

## Comments

I don't think this is entirely accurate.

A popular formulation of the category of sets is the

Elementary Theory of The Category of Sets, Lawvere (1964). Lawvere defines the element relation \(\in\) inDefinition 1of this paper:Here \(\mathbf{1}\) denotes an initial object.

Well... I can think of at least two formulations of category theory which contradict this claim.

For instance, in the Coq Implementation of Homotopy Type Theory (HoTT), an equality primitive is defined here. I have seen this called

path equality. HoTT stipulates an axiom over path equality, called univalence. After that category theory is then built on top of this (here is the source code).In John Weigley's Coq formulation of Category Theory, on the other hand, introduces

classbased equality similar to Haskell (see the source code here). Again, he builds category theory on top of this primitive notion.Well, I think we are coming from very different backgrounds. Homotopy Type Theory has some things to say about what you are asking. But it may present a very different foundation of mathematics than you are used to.

I should say though that I am just a student, so please take everything I say with a grain of salt.

[EDIT: formatting]

`> The conclusion that I am drawing is that set theory and category theory are different ways of thinking. In set theory, we can appeal to the axiom of extensionality, which says that singletons {a} and {b} are the same iff a=b. But in the category Set, there is no concept of element. I don't think this is entirely accurate. A popular formulation of the category of sets is the [_Elementary Theory of The Category of Sets_, Lawvere (1964)](https://artscimedia.case.edu/wp-content/uploads/2013/07/14182623/Lawvere-ETCS.pdf). Lawvere defines the element relation \\(\in\\) in **Definition 1** of this paper: > (From Lawvere) Definition 1. \\(x\\) is an element of \\(A\\), denoted \\(x \in A\\), iff \\(\mathbf{1} \overset{x}{\to} A\\) Here \\(\mathbf{1}\\) denotes an initial object. > When are two objects the same? When they have the same identity morphism. Well... I can think of at least two formulations of category theory which contradict this claim. For instance, in the Coq Implementation of Homotopy Type Theory (HoTT), an equality primitive is defined [here](https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v#L212-L214). I have seen this called _path equality_. HoTT stipulates an axiom over path equality, called [univalence](https://github.com/HoTT/HoTT/blob/master/theories/Types/Universe.v#L34-L38). After that category theory is then built on top of this ([here](https://github.com/HoTT/HoTT/blob/master/theories/Categories/Category/Core.v) is the source code). In John Weigley's Coq formulation of Category Theory, on the other hand, introduces _class_ based equality similar to Haskell (see the source code [here](https://github.com/jwiegley/category-theory/blob/master/Lib/Equality.v#L202-L213)). Again, he builds category theory on top of this primitive notion. > So I'm inclined to select the answer that says to look at the identity morphism. But I may be in error. Well, I think we are coming from very different backgrounds. Homotopy Type Theory has some things to say about what you are asking. But it may present a very different foundation of mathematics than you are used to. I should say though that I am just a student, so please take everything I say with a grain of salt. [EDIT: formatting]`

Matthew, thank you very much for your very helpful answer. You give me a lot that I can study. I will start with Lawvere's paper. I was wrong about the elements. The way that Lawvere sets it up seems nice in that an element is an arrow from ("the") singleton to a set, but subsets are not "elements" of sets.

`Matthew, thank you very much for your very helpful answer. You give me a lot that I can study. I will start with Lawvere's paper. I was wrong about the elements. The way that Lawvere sets it up seems nice in that an element is an arrow from ("the") singleton to a set, but subsets are not "elements" of sets.`