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: Does this variation in the "slice category"have a name?

Davi Sales Barreira (Dec 06 2023 at 17:45):

Hello, friends. In my PhD I'm trying to formalize some of my code using Category Theory. I've then stumbled on the following construction, which I'm trying to understand. The question requires me to explain my construction, so it will have to take some time to explain the idea. But my main question is to try to understand two things: first, if this type of construction has a name (if people use it and have done work on it); secondly, how I can understand the "morphism" $\theta$ (is it a natural transformation, a functor,...?).

Consider I'm working in the category $Set$, and that I have a monad $D$ and a fixed object $P$.

I state that $A$ belongs to a category $M$ if it has a unique function $\theta_A: A \to D P$. Informally, what I want to say is that a type $A$ is an object of the category $M$ if and only if it has a unique way to turn elements of $A$ into elements of $D P$.

Davi Sales Barreira (Dec 06 2023 at 17:45):

In this construction, the $\theta$ 's are morphisms in $M$. Thus, $D P$ is the terminal object in this category, since each $\theta$ is unique and has $DP$ as codomain.

Davi Sales Barreira (Dec 06 2023 at 17:46):

Note that $DP$ belongs to $M$ by considering $\theta_{DP}$ as the identity function.

Davi Sales Barreira (Dec 06 2023 at 17:47):

Moreover, we can also use the fat that $D$ is a monad to say that $DA$ is in $M$, by making $\theta_{DA} = \mu D \theta_A$.

Davi Sales Barreira (Dec 06 2023 at 17:48):

After one has populated $M$ with some objects and morphisms, one can devise a new method for constructing objects of $M$. Let $B$ be an object of $Set$. Then, if we define a function $\zeta_B:B \to DM$, we can obtain a function $\theta_B = \mu D \theta \zeta_B$

Davi Sales Barreira (Dec 06 2023 at 17:50):

Finally, my question is what is this $\theta$ that appears in $\mu D \theta \zeta_B$? Note that it does not have an index as the rest, but one can understand it as a polymorphic function. Still, how can we understand it categorically?

David Egolf (Dec 06 2023 at 18:21):

Someone else can probably give you a more complete answer. But here's my best guess!

You are considering a collection of certain morphisms from various objects to a fixed object $DP$. This sounds like a sink to me. The book "Abstract and Concrete Categories" talks about sources and sinks starting in section III.

For example, here's the definition of a sink from that book:
sink

So maybe $\theta$ is a certain kind of sink? I'm not totally following how you formed $\theta_B$, but I know that one can compose sinks with morphisms (or other sinks) to get new sinks.

Davi Sales Barreira (Dec 06 2023 at 18:35):

Thanks, @David Egolf . I'll take a look in the book. The sink does seems similar.

About $\theta_b$, the idea is that if I know how to turn $B$ into $DA$ and I know how to turn $A$ into $DP$, then I know how to turn $B$ into $DP$. Which is true due to the monadic nature of $D$.

David Egolf (Dec 06 2023 at 18:38):

Thanks for clarifying!

I drew a picture to try and illustrate the situation, as I understand it:
getting theta B

Davi Sales Barreira (Dec 06 2023 at 18:38):

Yes!

Davi Sales Barreira (Dec 06 2023 at 18:42):

The idea in this construction is the following.
The $D$ monad constructs tree expression over a type. The type $P$ is a primitive, and consists of objects that I can represent in the screen, and I can evaluate a tree of type $DP$ and produce an image in the screen by rendering each $P$. The $\theta_A : A \to DP$ is a way to say that an element $a$ of $A$ has a representation since I can express it as an $DP$.
But the thing is that, if I can define a new type $B$ and express it as an expression of $A$'s, than I should still be able to get an element of $DP$.

David Egolf (Dec 06 2023 at 18:43):

You may already be aware of this, but the composition you described I believe corresponds to composition in the Kleisli category for $D$:
Kleisli composition

(The screenshot is from p. 138 of this book by Perrone).

Davi Sales Barreira (Dec 06 2023 at 18:46):

I dont't think it's exactly the composition in Kleisli due to the construction... The idea is that $\zeta_B$ goes from $B$ to any expression of type $DM$.

Davi Sales Barreira (Dec 06 2023 at 18:47):

Where $M$ is the category itself...

Davi Sales Barreira (Dec 06 2023 at 18:53):

Consider that $P$ is the collection of simple geometric shapes (circle, square,...).
Then, $D$ is a way to combine these shapes, and an expression $DP$ is a tree of geometric shapes that produces a drawing in the screen.

We then specify a type $Person$ which has a function $\theta_{Person}$ that says how to draw a person, e.g. given the size of the person and the head shape, it returns an expression of $DP$. Similarly, define a type called $Building$.
Now I want to define a City, which is just a collection of persons and buildings... Since I know how to draw a person and a building, I want to define a function $\zeta_{City}: City \to D M$. Note that what this means is that a city is drawn by combining persons and buildings, which I know how to draw.

Davi Sales Barreira (Dec 06 2023 at 18:54):

Therefore, the $\zeta$ function I've used to defined the city is indeed enough to induce the $\theta_{City}$, which actually turns the city representation into the primitive geometric shapes, which are the thing I know how to draw.

David Egolf (Dec 06 2023 at 18:55):

Thanks for explaining! (I need to go do some other stuff now, but I'll plan to read over and try to understand what you just said.)

Hopefully someone else can chime in with some thoughts as well!

Davi Sales Barreira (Dec 06 2023 at 18:55):

Thanks a lot

Todd Trimble (Dec 06 2023 at 19:06):

Davi Sales Barreira said:

Hello, friends. In my PhD I'm trying to formalize some of my code using Category Theory. I've then stumbled on the following construction, which I'm trying to understand. The question requires me to explain my construction, so it will have to take some time to explain the idea. But my main question is to try to understand two things: first, if this type of construction has a name (if people use it and have done work on it); secondly, how I can understand the "morphism" $\theta$ (is it a natural transformation, a functor,...?).

Consider I'm working in the category $Set$, and that I have a monad $D$ and a fixed object $P$.

I state that $A$ belongs to a category $M$ if it has a unique function $\theta_A: A \to D P$. Informally, what I want to say is that a type $A$ is an object of the category $M$ if and only if it has a unique way to turn elements of $A$ into elements of $D P$.

I'm sorry, I'm skimming along the surface and really am not following.

So this $D$ is a monad on the category of sets? If $DP$ has more than one element, then for any set $A$, the only way that there can be a unique function $A \to DP$ is when $A$ is the empty set. So in all cases, according to this reading, the category $M$ winds up looking pretty trivial.

I think you must mean something different from what I am reading.

Davi Sales Barreira (Dec 06 2023 at 19:10):

To clarify, I'm using Bartosz idea of interpreting programming types as sets in the category of Sets. With that said, the type $P$ is like a union type $Circle + Square + ...$ which are basic geometric shapes.
What I want to do is to construct $M$. In this case, $M$ is working like a type class.

Davi Sales Barreira (Dec 06 2023 at 19:10):

For example, a priori a type $X$ is not in $M$, since I haven't defined a function $\theta_X : X \to DP$.

Davi Sales Barreira (Dec 06 2023 at 19:11):

One I define such function, than $X$ is now part of my type class $M$ (category?)

Davi Sales Barreira (Dec 06 2023 at 19:11):

Does this makes things a bit clear?

Todd Trimble (Dec 06 2023 at 19:12):

No, it does not make things any clearer for me. Let me start with: is $D$ a monad on sets? You said, "consider I'm working in the category $Set$".

Davi Sales Barreira (Dec 06 2023 at 19:13):

Yes

Davi Sales Barreira (Dec 06 2023 at 19:13):

$D$ is a monad over the category of Sets.

Todd Trimble (Dec 06 2023 at 19:13):

And $A$ is a set satisfying a certain property?

Davi Sales Barreira (Dec 06 2023 at 19:13):

No. $A$ is any type (set).

Davi Sales Barreira (Dec 06 2023 at 19:16):

Sorry if this is all over the place. My knowledge in Category Theory is not very robust.

Todd Trimble (Dec 06 2023 at 19:16):

Okay, for people who don't know the Milewski (I presume Milewski) background you mention, like me, I'm not sure your meaning will be clear. When you give notation $A \to DP$, it is usually presumed that $A$ and $DP$ belong to the same category, in this case the category of sets.

Davi Sales Barreira (Dec 06 2023 at 19:17):

Yes, the framework is that types in programming are sets, and functions are morphisms.

Davi Sales Barreira (Dec 06 2023 at 19:17):

$f:A \to B$ means a function that takes a value of type $A$ and returns a type $B$.

Todd Trimble (Dec 06 2023 at 19:20):

So if $A$ and $B$ are any two sets, and if there is exactly one function $A \to B$, then there is a very limited number of possibilities on $A$ and $B$.

(A type B? Or a value of type $B$?)

(I'm going to bow out very quickly unless my basic confusion gets sorted out in the next few minutes.)

Davi Sales Barreira (Dec 06 2023 at 19:23):

Take $A$ to be Int, take $B$ to be strings. A function $f:Int\to String$ takes a value of type Int and returns a value of type String. The monad $D:Set \to Set$.

Davi Sales Barreira (Dec 06 2023 at 19:23):

Now, for the hom-set of functions from $A$ to $DP$ one select one function $\theta_A$. Now, $(A, \theta_A)$ belongs to the category $M$.

Todd Trimble (Dec 06 2023 at 19:26):

If $B$ is a set with more than one element (let's say $B$ has two distinct elements $a, b$), and if $A$ has at least one element, then there will be at least two functions,

$A \to \{\ast\} \rightrightarrows B$

where those two parallel arrows name the elements $a$ and $b$.

Ultimately this must be me quibbling with your use of language, and I hate to be that guy, but I am that guy.

Todd Trimble (Dec 06 2023 at 19:28):

Okay, this confirms me that the issue is one of language use. You don't really mean there is literally a unique function, you must mean a uniquely specified choice of function.

(I'm pretty picky about language use, and for that I must beg your pardon.)

Davi Sales Barreira (Dec 06 2023 at 19:30):

I understand the pickness. Bad language can mess things up. I'm actually coming to the problem trying to interpret the messy program I have into a categorical framework.

Yes, I do mean that one specifies a unique function, which I called $\theta_A$.

Todd Trimble (Dec 06 2023 at 19:30):

So an object is a set $A$ equipped with a function $\theta_A: A \to DP$?

Davi Sales Barreira (Dec 06 2023 at 19:30):

Yes.

Todd Trimble (Dec 06 2023 at 19:30):

Okay, thank you. I can reread now.

Todd Trimble (Dec 06 2023 at 19:38):

Davi Sales Barreira said:

After one has populated $M$ with some objects and morphisms, one can devise a new method for constructing objects of $M$. Let $B$ be an object of $Set$. Then, if we define a function $\zeta_B:B \to DM$, we can obtain a function $\theta_B = \mu D \theta \zeta_B$

Should that $M$ in $\zeta_B$ be an $A$ (that is the underlying set of an $(A, \theta_A)$ assumed to be an object of the category $M$)?

Todd Trimble (Dec 06 2023 at 19:49):

I'm complaining that you're overloading the letter $M$, which was originally the category, not an object of the category. I'm guessing you mean a composite

$B \overset{\zeta_B}{\to} DA \overset{D\theta_A}{\to} DDP \overset{\mu_P}{\to} DP$

No?

Davi Sales Barreira (Dec 06 2023 at 19:50):

I actually understood the question, and it made me think of a theoretical issue with what I was trying to come up with.

Davi Sales Barreira (Dec 06 2023 at 19:51):

The idea is that $\zeta_B: B \to D X$ where $X$ is any other type that belongs to $M$.
(I'm also using $X$ to mean $(X, \theta_X)$)

Todd Trimble (Dec 06 2023 at 19:54):

And that's what I said, except that I used the letter $A$, not $X$. So anyway, you seem to be confirming the point of my complaint (no?).

Anyway, the construction I mentioned (and what I thought you meant) is part and parcel of what is called the Kleisli category of $D$, which you may know about already.

Davi Sales Barreira (Dec 06 2023 at 19:54):

Yes, indeed I understood your point, and I'm confirming your objection.

Davi Sales Barreira (Dec 06 2023 at 19:55):

So I think it would fall under Kleisli.

Davi Sales Barreira (Dec 06 2023 at 19:55):

Thanks for the interjections.

Todd Trimble (Dec 06 2023 at 19:57):

So it looks like you're considering a slice category $\text{Kleisli}(D)/P$.

Davi Sales Barreira (Dec 06 2023 at 19:59):

Yes, thanks again. This will help me clarify what is going on in the code.

Todd Trimble (Dec 06 2023 at 20:00):

Just so there's no miscommunication: $\text{Kleisli}(D)$ is the category whose objects are sets, and whose morphisms $A \to B$ are functions $A \to DB$; these morphisms are composed in the way we're discussing. The identity morphism on $A$ is the monad unit $u_A: A \to DA$ as a function. (I'm sure you're familiar with this; I'm just trying to be careful.)

Davi Sales Barreira (Dec 06 2023 at 20:02):

Yes, it's clear.

Davi Sales Barreira (Dec 06 2023 at 20:03):

In my case though, I guess I'm actually working on a subcategory of $\text{Kleisli}(D)/P$.
Since I'm considering only a single function $\theta_A$ for every set $A$.

Vincent R.B. Blazy (Dec 06 2023 at 20:09):

Davi Sales Barreira said:

The idea is that $\zeta_B: B \to D X$ where $X$ is any other type that belongs to $M$.
(I'm also using $X$ to mean $(X, \theta_X)$)

So there you rather have a family $(\zeta_{B,X}: B \to X)_{(X,\theta_X)\in Obj(M)}$ of arrows in $Kleisli(D)$, and maybe one for any set B? Don’t you?

Todd Trimble (Dec 06 2023 at 20:17):

Davi Sales Barreira said:

In my case though, I guess I'm actually working on a subcategory of $\text{Kleisli}(D)/P$.
Since I'm considering only a single function $\theta_A$ for every set $A$.

I hope you don't mind my saying, but this seems a bit strange to me, from a category theorist's perspective. It seems to require that the underlying functor from your category $M$ to $Set$, taking $(A, \theta_A)$ to $A$, be injective on objects. But this is against the spirit of the principle of equivalence.

Davi Sales Barreira (Dec 06 2023 at 21:12):

@Vincent R.B. Blazy , I'm sorry, I didn't understand your point.

Davi Sales Barreira (Dec 06 2023 at 21:13):

@Todd Trimble , I actually appreciate the criticism. I didn't know about the principle of equivalence. I'm reading on it, but I'm still trying to understand how it relates to the problem at hand.

Davi Sales Barreira (Dec 06 2023 at 21:13):

The way I'm constructing $M$ is somewhat ad hoc, because it actually stems from the application I'm trying to code.

Davi Sales Barreira (Dec 06 2023 at 21:14):

I'm trying to use Category Theory as a way to inform the way I'm coding my application. But the process sort of runs in both directions.

Davi Sales Barreira (Dec 06 2023 at 21:14):

Perhaps there is a categorical way of expressing what I'm trying to do that actually has a better theoretical ground.

Vincent R.B. Blazy (Dec 06 2023 at 21:29):

Davi Sales Barreira said:

Vincent R.B. Blazy , I'm sorry, I didn't understand your point.

I’m starting from you having said that your $\zeta_B$ was meant to target BX for any X. Maybe I misunderstood you first, but I thought that this meant a family of morphisms rather than only one, for some fixed random X :smile:

Davi Sales Barreira (Dec 06 2023 at 21:30):

At first the idea was that, but I realized that there was an issue with this definition.

Davi Sales Barreira (Dec 06 2023 at 21:32):

The main property is that $\zeta_B$ has to take $B$ to $D X$ where $X$ is of $M$.

Davi Sales Barreira (Dec 06 2023 at 21:32):

Now this $X$ could be any object of $M$, hence why I first wrote $DM$.

Davi Sales Barreira (Dec 06 2023 at 21:33):

But this is problematic, specially since $\zeta_B: B \to DB$ would not be valid.

Davi Sales Barreira (Dec 06 2023 at 21:35):

This whole discussion actually lies in a very practical problem, which is the one I was trying to describe. The ideia that $P$ is a special type and that $DP$ is an expression composed of elements of $P$, which is a description of how to represent a scene as a combination of geometric objects.

Davi Sales Barreira (Dec 06 2023 at 21:40):

One then want to define things like "a house". A house would be a combination of a roof, the walls, the door and the windows. Thus, instead of defining $\theta_{House}: House \to DP$, one defines a function $\zeta_{House}: House \to D(Roof + Wall + Window + Door)$, which means that instead of defining how to draw a house directly, we actually specify how to combine a roof, walls and windows... IF we know how to draw a roof, a wall and a window, then we should be able to draw the house. And to be able to draw the roof, windows and walls is the same as having $\theta_{Roof}:Roof \to DP$, $\theta_{Window}:Window \to DP$, $\theta_{Wall}: Wall \to DP$.

Davi Sales Barreira (Dec 06 2023 at 21:42):

The idea that the $\theta_X$ is unique is not inspired in the categorical definition, but in the practical idea that each type should have a single "canonical" drawing representation.

Todd Trimble (Dec 07 2023 at 03:05):

Possibly to save you some time, Davi, let me describe a scenario meant to illustrate this business of the principle of equivalence (aka, "the problem of evil") .

Todd Trimble (Dec 07 2023 at 03:05):

Say Janice has a particular liking for the set $\{1, 2, 3\}$ and dreams up plans for a $\theta: \{1, 2, 3\} \to DP$. After carefully considering exactly what $\theta$ should look like, she has her plans written up and notarized, and takes her materials over to the government office in charge of approving these things. The official looks in his records, and sorrowfully answers, "I'm sorry, but that set has already been considered, and the rules are: only one $\theta$ per set".

Todd Trimble (Dec 07 2023 at 03:05):

Crestfallen, Janice walks away. After a while, she thinks to herself: why don't I simply create a clone of the set $\{1, 2, 3\}$? It would be exactly alike $\{1, 2, 3\}$ in every single detail (we'll call it $\{1', 2', 3'\}$ for the sake of discussion), so much so that if you placed the two sets side by side, you could not tell which is the original and which is the copy. (Is it live, or is it Memorex? went the old 70's commercial.) But, it's a new set, and so it hasn't been assigned a $\theta$ yet. And so she reasons the government official now can have no grounds for complaint, can he?

Todd Trimble (Dec 07 2023 at 03:06):

She brings in her clone $\{1', 2', 3'\}$ into the office. The fellow looks up at her and says, "Weren't you here last week? As I already explained, only one $\theta$ per set." She says, "I know, but this isn't the same set as the one from last week." "It's not?! It looks exactly the same!" "I know! But this one is mine, and I've called it $\{1', 2', 3'\}$." "Listen, lady -- don't get smart with me. Admit it: it's the same set."

Todd Trimble (Dec 07 2023 at 03:06):

Later, the government official checks up on the old set $\{1, 2, 3\}$, but is now suddenly unsure whether that's the true original, or a clone matching it to perfection, or whether someone swapped out its $\theta$ for another $\theta'$ in the dead of night.

Todd Trimble (Dec 07 2023 at 03:06):

In category theory, it's generally better to arrange definitions so that any issue of having to distinguish between two indiscernably different things doesn't have to be faced, or in other words, the concept doesn't change if you replace the original category with an equivalent one (like the category of sets). Having a rule that a functor be injective on objects would fly in the face of that principle.

Davi Sales Barreira (Dec 07 2023 at 09:55):

Wow, thanks for the explanation!

Vincent R.B. Blazy (Dec 07 2023 at 10:48):

Davi Sales Barreira said:

One then want to define things like "a house". A house would be a combination of a roof, the walls, the door and the windows. Thus, instead of defining $\theta_{House}: House \to DP$, one defines a function $\zeta_{House}: House \to D(Roof + Wall + Window + Door)$, which means that instead of defining how to draw a house directly, we actually specify how to combine a roof, walls and windows... IF we know how to draw a roof, a wall and a window, then we should be able to draw the house. And to be able to draw the roof, windows and walls is the same as having $\theta_{Roof}:Roof \to DP$, $\theta_{Window}:Window \to DP$, $\theta_{Wall}: Wall \to DP$.

Ookay then you want a specific object X of M for each B! You should perhaps use a dedicated functor giving it for each B, then (in addition of the evilness issue)?

Davi Sales Barreira (Dec 07 2023 at 10:58):

It seems that indeed the $\mathcal M = \text{Kleisli}(D)/P$ is the category I'm working on. But now I have objects such as $(A, \theta_A)$ and $(A, \theta_A')$.

Davi Sales Barreira (Dec 07 2023 at 11:00):

Given $(B, \theta_B)$, the $\zeta_B:(B,\theta_B) \to A$ is a morphism of $\mathcal M$ iff $\theta_B = \mu \circ D\theta_A \circ\zeta_B$.

Davi Sales Barreira (Dec 07 2023 at 11:04):

This would mean that $(DB, \mu D\theta_B)$ also belongs to $\mathcal M$.

Davi Sales Barreira (Dec 07 2023 at 11:04):

I now have to figure out how this can be implemented as code.

Davi Sales Barreira (Dec 07 2023 at 11:05):

I'm actually writing code in Julia, so it is not straight-forward. Also, I haven't seen much how slice categories are used in programming. The Kleisli category and monads are more common.

Davi Sales Barreira (Dec 07 2023 at 11:07):

@Vincent R.B. Blazy, your suggestion would be to create a functor $M:Set \to \text{Kleisli}(D)/P$ ?

Vincent R.B. Blazy (Dec 07 2023 at 11:23):

Davi Sales Barreira said:

Given $(B, \theta_B)$, the $\zeta_B:(B,\theta_B) \to A$ belongs to $\mathcal M$ iff $\theta_B = \mu \circ D\theta_A \circ\zeta_B $.

You mean «belongs to $\mathcal M$» as an arrow then? Because satisfying this equation by definition what being an arrow in $\text{Kleisli}(D,μ,η)/P$ amounts to!

Vincent R.B. Blazy (Dec 07 2023 at 11:24):

Davi Sales Barreira said:

This would mean that $(DB, \mu D\theta_B)$ also belongs to $\mathcal M$.

Why so?

Davi Sales Barreira (Dec 07 2023 at 11:25):

I meant that it is a morphism.

Davi Sales Barreira (Dec 07 2023 at 11:25):

Isn't this the definition in a slice category?

Davi Sales Barreira (Dec 07 2023 at 11:27):

That a function $f:B\to A$ in the original category generates a morphism between $(B,\theta_B)$ to $(A,\theta_A)$ in the slice category if $\theta_A \circ f = \theta_B$

Vincent R.B. Blazy (Dec 07 2023 at 11:28):

Davi Sales Barreira said:

Isn't this the definition in a slice category?

Yes that’s what I say, arrow is synonym of morphism in cat theory :big_smile: (I prefer to reserve the latter only to functions preserving structure)

Davi Sales Barreira (Dec 07 2023 at 11:28):

About $(DB, \mu D\theta_B)$, it is an object of $\mathcal M$ because $\mu D\theta_B: DB \to DP$, no?

Vincent R.B. Blazy (Dec 07 2023 at 11:30):

Davi Sales Barreira said:

Vincent R.B. Blazy, your suggestion would be to create a functor $M:Set \to \text{Kleisli}(D)/P$ ?

Yes, but that was independently of the implementation, in order to map each «B» to the desired combination of characters you need to define it, following your house-building example!

Vincent R.B. Blazy (Dec 07 2023 at 11:31):

Davi Sales Barreira said:

About $(DB, \mu D\theta_B)$, it is an object of $\mathcal M$ because $\mu D\theta_B: DB \to DP$, no?

Ah this time as an object! Yes ok indeed; sorry

Davi Sales Barreira (Dec 07 2023 at 12:42):

BTW, is there any references on $\text{Kleisli}(D)/ P$? I mean, slice category over the Kleisli category.

Davi Sales Barreira (Dec 07 2023 at 12:49):

Another caveat, the monad $D$ is the free monad over a functor $F$.