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: Are objects just types?

Alex Kreitzberg (Sep 23 2024 at 16:17):

Is it safe to think of the objects in a category as types?

Depending on the assumptions of your category, you can talk about elements, subsets, whether a subset corresponds to an object, etc.

But can you always think of objects as types? Or, as an example of a conflict, do types have elements in all of their definitions?

John Baez (Sep 23 2024 at 16:18):

Define "type". I can define "object in a category", but before knowing whether it's safe for you to think of it as a type, I need to know what you mean (you mean) by a type.

Alex Kreitzberg (Sep 23 2024 at 16:27):

The question is motivated by Leinster's notes.

My basic understanding of "type" is it tracks what operations are allowed on some data (both in and out).

I'm open to types being "plug and socket" pairs, so you're only allowed to connect a wire "if the ends match", as synonymous with "if the types match".

I guess I'm half asking if types can be safely understood as generally as objects "but no further" or if there is some key distinct insight that makes them different.

Alex Kreitzberg (Sep 23 2024 at 16:36):

Another way I've thought about types is as expression combination rules. An expression is composed of smaller expressions with specific types, and the whole expression has its own type.

So types then are a sort of grammer, that's especially simple to understand.

Mike Shulman (Sep 23 2024 at 16:56):

Formally, a "type" is usually a thing in a formal system of syntax. Most or all such "type theories" include judgments describing the "elements" or "terms" of a type, so that inside the theory, types behave a lot like sets.

Alex Kreitzberg (Sep 23 2024 at 16:57):

Thank you! I think that answers my question

Mike Shulman (Sep 23 2024 at 16:57):

Categorical semantics provides a way to interpret such a system of syntax into a category, so that each type corresponds to an object. But I wouldn't normally say that the objects of a category are types.

Mike Shulman (Sep 23 2024 at 16:57):

(Except for particular special categories, like the "syntactic category" of a type theory in which the objects are defined to be the types of that theory.)

Kevin Carlson (Sep 23 2024 at 17:06):

You probably should try not to think of the objects in a(n arbitrary) category as anything at all. In general, they're just dots that can mark out domains and codomains, much as elements of an arbitrary set are just dots that can't do anything at all.

Alex Kreitzberg (Sep 23 2024 at 17:35):

If I provide a categorical semantics for a type system like HoTT - can I argue each term has a unique type, because each term is an arrow from the terminal object to a unique codomain $\cdot \rightarrow T$?

Edit: I know term's types are unique because they are, but is this necessary for the categorical semantics to work?

John Baez (Sep 23 2024 at 17:39):

Kevin wrote:

You probably should try not to think of the objects in a(n arbitrary) category as anything at all. In general, they're just dots [....]

Either that, or get used to thinking of them in a bunch of different ways, and choose the way that's most appropriate for a given context. They're kind of like dots, and sometimes they're kind of like sets, and sometimes they're kind of like types, and sometimes they're kind of spaces, and... so on.

Kevin Carlson (Sep 23 2024 at 17:57):

Yeah, you can't survive actually thinking of them as "just dots" all the time, but that's often the hardest perspective to learn at first, and it's the only one that in some middlebrow sense is sufficient for all cases.

Mike Stay (Sep 23 2024 at 18:04):

Melliès and Zeilberger wrote a nice paper, "Functors are type refinement systems". In it, they say

Our starting point here will be the observation that this analysis may be turned around: in fact, any functor
$U : D \to T$
may be alternatively viewed as a “type system” in a generalized sense, if we interpret the (arbitrary) category $D$ as a category of typing derivations and the (arbitrary) category $T$ as a category of terms. This will lead us to a purely categorical way of speaking about typing derivations and terms—but also conversely to a purely type-theoretic way of speaking about functors.

John Baez (Sep 23 2024 at 18:05):

Kevin Carlson said:

Yeah, you can't survive actually thinking of them as "just dots" all the time, but that's often the hardest perspective to learn at first, and it's the only one that in some middlebrow sense is sufficient for all cases.

You definitely don't want to get stuck in any one way of thinking that's more specific than 'just dots', because then a category will come along for which that way of thinking may be more confusing than helpful.

The otherwise stupid modern saying "it is what it is" actually applies pretty well to the concept of category.

Madeleine Birchfield (Sep 23 2024 at 19:02):

The real numbers equipped with $\leq$ is a category where each hom-set has at most one morphism. Are real numbers types?

Alex Kreitzberg (Sep 23 2024 at 19:19):

I don't want to say this is a uniquely important point of view.

But where my intuition goes with that thought, is say you have a manufacturing facility which processes widgets, and the widgets are allowed to go through a given unit provided the widget is below that unit's height requirement, and that's it.

Now you're allowed to connect three units, provided the height requirements are only increasing.

I think of the natural numbers as "types" between matrices, tracking whether you're allowed to multiply them.

But I'm prepared to accept this interpretation only really makes sense with respect to categories with specified morphisms.

Alex Kreitzberg (Sep 23 2024 at 19:24):

I interpreted Shulman's answer though as implying the way I'm using type here is too broad

Mike Shulman (Sep 23 2024 at 19:41):

Perhaps what you're thinking is that when the notion of category is written in a dependently typed language, the type of the composition function is

$$\forall (x,y,z : \mathrm{ob}(C)), \hom(y,z) \times \hom(x,y) \to \hom(x,z).$$

Thus, the type system enforces that you can only compose two morphisms if their types $\hom(y,z)$ and $\hom(x,y)$ share an object. This is what's going on with multiplying matrices: the (dimension of the) codomain of one must match the (dimension of the) domain of the other. Here the objects of the category aren't themselves types, but they are parameters of the dependent hom-type which governs the allowed composites.

Alex Kreitzberg (Sep 23 2024 at 19:44):

Oh weird, that makes sense

Mike Shulman (Sep 23 2024 at 19:46):

Alex Kreitzberg said:

If I provide a categorical semantics for a type system like HoTT - can I argue each term has a unique type, because each term is an arrow from the terminal object to a unique codomain $\cdot \rightarrow T$?

Edit: I know term's types are unique because they are, but is this necessary for the categorical semantics to work?

It's true that categorical semantics requires each "thing it interprets as a morphism" to have a unique domain and codomain, since each morphism in a category has a unique domain and codomain. (For a term in a nonempty context, the domain may not be the terminal object, rather it's the object corresponding to that context.) However, the information in that domain and codomain may not be fully contained in the syntactic object called a "term" without also knowing its type. In other words, what gets interpreted as a morphism is not a bare term but a term judgment $\Gamma \vdash t:A$, with $\Gamma$ being interpreted as the domain of that morphism and $A$ as its codomain. Depending on the type theory, $A$ might or might not be determined by $t$ (and $\Gamma$ is almost never determined by $t$), but it doesn't matter since categorical semantics takes $\Gamma$ and $A$ as part of its input to produce a morphism.

Alex Kreitzberg (Sep 23 2024 at 19:49):

Thank you, your answers have been very enlightening.

This stuff is hard! I'll try and tighten up my language more to save folks time.

Alex Kreitzberg (Sep 23 2024 at 20:40):

So a "term" is sorta like a "rule", in that by itself it's not enough to make a term judgement, like a rule isn't enough to define a function.

The bookkeeping in category theory is possible in part because we have hom-sets, which depend on objects. So the compose operator has enough data to check whether arrows can compose. Types behave like sets.

I think I understand, I'm sure I'll understand it better as I mull over the answers.

Mike Shulman (Sep 23 2024 at 20:42):

Terminology-wise, in type theory the "rules" are what tell us how to form certain judgments. For instance, the "pairing" rule says that if we have judgments $\Gamma \vdash s:A$ and $\Gamma \vdash t:B$ we can form $\Gamma \vdash (s,t) : A\times B$. This probably isn't what you meant by "rule".

Alex Kreitzberg (Sep 23 2024 at 20:44):

Oh definitely not, thank you, yes by "rule" I meant just the syntax "(s, t)", but I'll try to use different language in the future.

Alex Kreitzberg (Sep 23 2024 at 20:45):

Well I guess I'll call that the "term" in the future

Mike Shulman (Sep 23 2024 at 20:47):

Note that a term is an entire expression like $(x^2+1, \lambda y. x+y)$, while something like the specific syntax of pairs $(\;,\;)$ is sometimes called a "term-former".

Alex Kreitzberg (Sep 23 2024 at 20:49):

Right, so $2x$ would be a term?

Alex Kreitzberg (Sep 23 2024 at 20:49):

Or even $\lambda x. 2x$

Mike Shulman (Sep 23 2024 at 20:51):

Yes.

John Onstead (Sep 23 2024 at 21:47):

John Baez said:

Either that, or get used to thinking of them in a bunch of different ways, and choose the way that's most appropriate for a given context. They're kind of like dots, and sometimes they're kind of like sets, and sometimes they're kind of like types, and sometimes they're kind of spaces, and... so on.

In the most abstract sense a category is just a directed graph with composition defined, so the objects are just vertices that don't mean anything. The meaning comes in when one specifies a (usually faithful or fully faithful) functor out of a category. If you take a category and equip it with a faithful functor to Set- if one exists- then the objects behave as sets with extra structure. If the faithful functor is into a category of types (like a syntactic category for a type theory as was mentioned) then you can view the objects as acting like types. If the faithful functor into Set is topological, then the objects act like spaces. And so on! So basically: category by itself = abstract objects, category with a specified functor = more meaning to the objects.

Mike Shulman (Sep 23 2024 at 22:42):

It's true that if you have a category with a functor defined on it, then you can think of the objects of that category as objects of the codomain of the functor equipped with extra "stuff". But in addition, in many specific categories, the objects literally are things with extra stuff. For instance, in the category of groups, the objects literally are sets equipped with group structures, not just abstract dots. It's only when we're talking about an arbitrary category that we're forced to treat the objects as featureless dots that can only be given meaning by functors.

Mike Shulman (Sep 23 2024 at 22:43):

This is the same as what happens all over mathematics. In an arbitrary group, the elements are featureless dots equipped with a composition operation, but in a specific group they are generally something specific, e.g. in a symmetric group the elements are permutations of some set. But for some reason it seems harder to wrap our mind around in the case of categories.

Madeleine Birchfield (Sep 26 2024 at 21:15):

Madeleine Birchfield said:

The real numbers equipped with $\leq$ is a category where each hom-set has at most one morphism. Are real numbers types?

On second thought this isn't a good example of a category whose objects aren't types.

One definition of a real number is a two-sided Dedekind cut, which is usually represented by an element of $\Omega^\mathbb{Q} \times \Omega^\mathbb{Q}$ satisfying certain axioms, but $\Omega^\mathbb{Q} \times \Omega^\mathbb{Q}$ is isomorphic to $(\Omega^\mathbb{Q})^2$ and thus to $\Omega^{2 \times \mathbb{Q}}$, where $2$ is the set with exactly two elements.

One can represent elements of $\Omega^{2 \times \mathbb{Q}}$ as sets with injections into the set $2 \times \mathbb{Q}$, meaning that one can define real numbers or Dedekind cuts as certain sets.

Alex Kreitzberg (Sep 27 2024 at 00:25):

Isn't that ZFC style encoding tricks though? If you think of a real number as a set, then you can write statements like $3 \in \pi$, which we don't want to do right?

Or am I dramatically misunderstanding you?

If we're not allowed $3 \in \pi$, then I think the point behind your original example still stands.

Alex Kreitzberg (Sep 27 2024 at 00:26):

i.e. I can have objects like real numbers that mediate whether I'm allowed to compose morphisms, but the objects don't have to behave like sets.

Madeleine Birchfield (Sep 27 2024 at 00:43):

Alex Kreitzberg said:

Isn't that ZFC style encoding tricks though? If you think of a real number as a set, then you can write statements like $3 \in \pi$, which we don't want to do right?

Or am I dramatically misunderstanding you?

If we're not allowed $3 \in \pi$, then I think the point behind your original example still stands.

No, that isn't a ZFC encoding trick, the definition of a Dedekind cut as an object in a category is valid in any well-pointed Heyting pretopos with NNO, where the object $2$ is defined as $1 \coprod 1$, $\mathbb{Q}$ is defined in the usual manner from the natural numbers object $\mathbb{N}$, products and quotients, injections are the monomorphisms into $2 \times \mathbb{Q}$.

Alex Kreitzberg (Sep 27 2024 at 00:45):

Interesting, okay thank you for clarifying

Madeleine Birchfield (Sep 27 2024 at 00:59):

The only difference is that without power sets, you can't define the set of all Dedekind cuts. However, you can still define addition, negation, multiplication, the order relations, etc on Dedekind cuts as operations on and relations between sets.

John Baez (Sep 27 2024 at 01:02):

@Alex Kreitzberg - in case you don't know: the idea of a Dedekind cut is to specify a real number you give the set $A$ of all rationals $<$ it and the set $B$ of all rationals $\ge$ it. That's what this $\Omega^{\mathbb{Q}} \times \Omega^{\mathbb{Q}}$ thing is about. So for the number $(A,B) = \pi$ you'd have $3 \in A$ meaning $3 < \pi$, and $3 \notin B$ meaning $3$ is not $\ge \pi$.

I'll let you decide if this is a "ZFC style encoding trick" or not.

Madeleine Birchfield (Sep 27 2024 at 01:05):

John Baez said:

Alex Kreitzberg - in case you don't know: the idea of a Dedekind cut is to specify a real number you give the set $A$ of all rationals $<$ it and the set $B$ of all rationals $\ge$ it.

Shouldn't the second condition be $\gt$ rather than $\ge$?

Madeleine Birchfield (Sep 27 2024 at 01:10):

John Baez said:

I'll let you decide if this is a "ZFC style encoding trick" or not.

It is an encoding trick but it doesn't inherently have anything to do with ZFC, since it is also valid in non-ZFC foundations like ETCS or SEAR or dependent type theory or higher order logic. Compare with the von Neumann ordinals as an encoding of the natural numbers, which only really makes sense in ZFC style set theories.

Madeleine Birchfield (Sep 27 2024 at 01:13):

In general, it's of the same nature as using elements of power sets $P' \in \Omega^A$ instead of sets $P$ with injections $i_P:P \to A$. In categorical set theory, $P'$ is in general not a set, the associated set is given by $\{a \in A \vert a \in_A P'\}$, where the relation $\in_A$ is given as part of the structure of the power set.

John Baez (Sep 27 2024 at 01:17):

Madeleine Birchfield said:

John Baez said:

Alex Kreitzberg - in case you don't know: the idea of a Dedekind cut is to specify a real number you give the set $A$ of all rationals $<$ it and the set $B$ of all rationals $\ge$ it.

Shouldn't the second condition be $\gt$ rather than $\ge$?

If you say so you must be right. I never use Dedekind cuts in my own work, although I've occasionally taught a course where I used them to construct the reals. So I don't remember the advantage of using $\gt$. Oh, I guess it makes negatives easier to define!

John Baez (Sep 27 2024 at 01:20):

Madeleine Birchfield said:

John Baez said:

I'll let you decide if this is a "ZFC style encoding trick" or not.

It is an encoding trick but it doesn't inherently have anything to do with ZFC, since it is also valid in non-ZFC foundations like ETCS or SEAR or dependent type theory or higher order logic.

I bet when Alex said "ZFC style encoding trick" he really just meant "set-theoretic encoding trick", since I've never seen him talk about non-ZFC foundations.

Madeleine Birchfield (Sep 27 2024 at 01:20):

John Baez said:

If you say so you must be right. I never use Dedekind cuts in my own work, although I've occasionally taught a course where I used them to construct the reals. So I don't remember the advantage of using $\gt$. Oh, I guess it makes negatives easier to define!

In non-boolean elementary toposes, the left-sided Dedekind cuts, right-sided Dedekind cuts, and two-sided Dedekind cuts do not coincide, and the two-sided Dedekind cuts are the ones which have the right topology. That they coincide is equivalent to the elementary topos being Boolean.

Mike Shulman (Sep 27 2024 at 02:22):

That's true, but John did describe a two-sided version. He made the lower half of the cut open and the upper half closed, which is a little oddly asymmetrical, but I don't think it's a problem even constructively. IIRC open and closed cuts are interdefinable even constructively, although the open ones are more traditional.

Madeleine Birchfield (Sep 27 2024 at 03:10):

Mike Shulman said:

That's true, but John did describe a two-sided version. He made the lower half of the cut open and the upper half closed, which is a little oddly asymmetrical, but I don't think it's a problem even constructively. IIRC open and closed cuts are interdefinable even constructively, although the open ones are more traditional.

I wasn't aware that one could use closed cuts for Dedekind cuts; all the definitions I've seen had only used the open ones.

Madeleine Birchfield (Sep 27 2024 at 03:14):

I also seem to have misinterpreted John Baez's comment: I took it to mean the advantage of using $\gt$ over nothing at all (i.e. two-sided vs left Dedekind reals) while he may have meant the advantage of using $\gt$ over $\geq$.

Alex Kreitzberg (Sep 27 2024 at 03:36):

I've already said something confused today, so I'm trying to avoid doing that twice XD, and I can't say I'm strong at foundations (I'm slightly interested in HoTT, and read "Naive set theory" by Halmos years ago)

I don't think there's an ordinary type system where you can have a judgement that looks something like $\Gamma \vdash x : \pi$, and it isn't clear to me how reals being built out of a pair of sets of rationals would let you do that. The set pair defining real numbers look like they're part of the implementation, not the interface of real numbers.

But I wanted to read and think over the answers first before commenting, because I was open to still being confused.

But yeah I meant "set-theoretic encoding trick", "implementation details", etc. An individual real number doesn't satisfy the interface of a type...right?

That was what I was trying to clarify.

And if that last paragraph was true, then individual real numbers as "not a type" still felt like a good counterexample to my (wrong) intuition that objects were types.

Madeleine Birchfield (Sep 27 2024 at 04:15):

Alex Kreitzberg said:

I don't think there's an ordinary type system where you can have a judgement that looks something like $\Gamma \vdash x : \pi$, and it isn't clear to me how reals being built out of a pair of sets of rationals would let you do that. The set pair defining real numbers look like they're part of the implementation, not the interface of real numbers.

But I wanted to read and think over the answers first before commenting, because I was open to still being confused.

But yeah I meant "set-theoretic encoding trick", "implementation details", etc. An individual real number doesn't satisfy the interface of a type...right?

What I've been trying to say is that there is a definition of a real number as a set or type. More specifically, one definition of a real number as a two-sided Dedekind cut is a set or type $A$ with an injection or embedding $i:A \to (2 \times \mathbb{Q})$ such that

• There exists $q:\mathbb{Q}$ and $a:A$ such that $i(a) = (0, q)$
• There exists $r:\mathbb{Q}$ and $b:A$ such that $i(b) = (1, r)$
• For all $q:\mathbb{Q}$, there exists $a:A$ such that $i(a) = (0, q)$ if and only if there exists $r:\mathbb{Q}$ such that $q \lt r$ and there exists $b:A$ such that $i(b) = (0, r)$
• For all $q:\mathbb{Q}$, there exists $a:A$ such that $i(a) = (1, r)$ if and only if there exists $q:\mathbb{Q}$ such that $q \lt r$ and there exists $b:A$ such that $i(b) = (1, q)$
• For all $q:\mathbb{Q}$, it is not true that there exists $a:A$ such that $i(a) = (0, q)$ and there exists $b:A$ such that $i(b) = (1, q)$
• For all $q:\mathbb{Q}$ and $r:\mathbb{Q}$, $q \lt r$ implies that there exists $a:A$ such that $i(a) = (0, q)$ or there exists $b:A$ such that $i(b) = (1, r)$

Since one can define the real number $\pi$ as a two-sided Dedekind cut, using the above definition, $\pi$ is a type with an injection $i_\pi:\pi \to 2 \times \mathbb{Q}$ satisfying the above axioms.

Madeleine Birchfield (Sep 27 2024 at 04:18):

As a result, it makes perfect sense to form the judgment $\Gamma \vdash x:\pi$ if one is using this definition of a real number.

The elements of $\pi$ in this case are codes for pairs $(b, q)$ consisting of a rational number and a boolean indicating whether the rational number is in the lower cut or the upper cut associated with the real number $\pi$. I say codes because the elements of $\pi$ aren't literally such pairs (unless one has coercion rules for injections / subtypes to mimic what happens in ZFC), but that given an element $x:\pi$, $i_\pi(x)$ is such a pair. And since $i_\pi$ is an injection, for every $(b, q)$ if there is a $x:\pi$ such that $i_\pi(x) = (b, q)$ then $x:\pi$ is the unique element of $\pi$ satisfying $i_\pi(x) = (b, q)$.

Mike Shulman (Sep 27 2024 at 04:44):

Madeleine Birchfield said:

I wasn't aware that one could use closed cuts for Dedekind cuts; all the definitions I've seen had only used the open ones.

I was surprised when I learned that too! If $L$ is an open lower cut, the corresponding closed lower cut is

$$\overline{L} = \{ r \mid \forall q<r, q \in L \}$$

and if $\overline{L}$ is a closed lower cut, the corresponding open lower cut is

$$L = \{ q \mid \exists r > q, r \in \overline{L} \}.$$

Alex Kreitzberg (Sep 27 2024 at 04:53):

Madeleine Birchfield said:

As a result, it makes perfect sense to form the judgment $\Gamma \vdash x:\pi$ if one is using this definition of a real number.

Alright thank you, I'll read what you wrote carefully, (and that's wild)

Madeleine Birchfield (Sep 27 2024 at 04:58):

More commonly, real numbers as two-sided Dedekind cuts are defined as consisting of two sets $L$ and $U$ with injections $i_L:L \to \mathbb{Q}$ and $i_U:U \to \mathbb{Q}$, where $(L, i_L)$ represents the lower cut associated with the real number and $(U, i_U)$ represents the upper cut associated with the real numbers. But one can just take the disjoint union of $L$ and $U$ and one gets a set $L \uplus U$ with a single injection $i_{L \uplus U}:(L \uplus U) \to (\mathbb{Q} \uplus \mathbb{Q})$, and $\mathbb{Q} \uplus \mathbb{Q}$ is isomorphic to $2 \times \mathbb{Q}$. Then one can simply say that the real number is represented by $L \uplus U$.

Madeleine Birchfield (Sep 27 2024 at 05:07):

And agreed that it is wild. In this formulation, sequences of real numbers are $\mathbb{N}$-indexed families of sets, and individual functions on the real numbers are modal operators on Dedekind cuts.