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: Understanding a definition more categorically

Sean Wu (Feb 06 2024 at 01:46):

I'm (re)reading a paper defining a certain type of dynamical system and trying to make sense of the set theoretic definitions in a more categorical light, but running into problems. I will present below a small snippet of the definition that illustrates some of my issue.

First the definitions as given set theoretically. Consider a set of state variables $SV$. Let $S : SV \rightarrow \mathcal{S}$, where $\mathcal{S}$ is a set of Types we'd use to represent states (so perhaps Int, Float, char, etc). Let $Val_{0}$ be a function giving the initial value of each state variable. It is defined to be $\forall sv \in SV : Val_{0}(sv) \in S(sv)$, so for each state variable it picks out a value in the Type that state variable is sent to.

How should I be thinking of formalizing the definition of $Val_{0}$? Given that it's job is to pick out elements of a set, it really seems like it ought to be related to functions out of the terminal object into each Type in order to do that, but I'm not sure if this is a good approach to follow. Any advice?

Sean Wu (Feb 06 2024 at 01:46):

@Kevin Arlin thanks for pointing me here!

Kevin Arlin (Feb 06 2024 at 02:06):

Without any further context I would formalize $S$ as a functor from the discrete category $SV$ into some category of types (which might just be the category of sets), and then $\mathrm{Val}_0$ is a natural transformation from the terminal such functor, just as you're suggesting. If types are sets, then you can also build up $S$ as a function $p:T\to SV,$ where $T$ is the disjoint union of all the values of $S,$ and then $\mathrm{Val}_0$ is a section of $p,$ that is a function $s$ with $p\circ s=\mathrm{id}_{SV}.$ This is a more intuitive picture, to my mind.

Sean Wu (Feb 06 2024 at 02:41):

Thanks @Kevin Arlin , I'll try working with that idea, as well as typing out more of the context.

Mike Shulman (Feb 06 2024 at 03:14):

Kevin's second suggestion is what I would say. From a type-theoretic perspective, what you have is a "dependently typed function" $\mathrm{Val}_0 : (x:{\rm SV}) \to S(x)$ or alternatively $\mathrm{Val}_0 : \prod_{x:{\rm SV}} S(x)$. In a category, the standard way to represent a dependently typed function $(x:A) \to B(x)$ is as a section of the projection from $\coprod_x B(x)$ to $A$.

Sean Wu (Feb 06 2024 at 05:18):

Thanks Mike and Kevin! Given all the Types are always going to be sets, the second approach looks like the better one to follow. I appreciate the connection to type theory, I did realize $$Val_{0}$ should be a dependent function type but I'm too early in my type theory learning to see how any of it maps to category theory yet; it's very nice to get this information.

Kevin, is your $T$ the disjoint union of all types in $\mathcal{S}$? To be absolutely concrete, say we had a Petri net with 3 places, then $S$ would send those 3 places to Int, so $T$ would be Int + Int + Int?

Kevin Arlin (Feb 06 2024 at 05:39):

Not necessarily all the types in $\mathcal S,$ just all of them in the range of $S.$ So your example is right.