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: theory: applied category theory

Topic: chemical recipes as functors

Jade Master (Feb 13 2021 at 03:32):

Combustion_reaction_of_methane.jpg

Jade Master (Feb 13 2021 at 03:32):

Hi @John Baez (and anyone else who is reading) I had an idea that I thought you might like or have helpful feedback on. If P and Q are Petri nets, then I think a sort of chemical recipe can be described as a symmetric monoidal functor

$R: FP \to FQ$

where F gives the free commutative monoidal category on each Petri net. The idea is that the places of Q are all the different chemicals you're working with and the transitions of Q give all relevant reactions between those chemicals. Then P is a Petri net whose places represent macroscale quantities of chemicals and whose transitions represent steps in your chemical recipe. For example Q could contain the reaction in the image above as a transition and P could contain a transition which mixes one mole of methane with 2 moles of oxygen to produce one mole of carbon dioxide and two moles of water.

Jade Master (Feb 13 2021 at 03:37):

Then the functor R would map the place representing on mole of CH4 to the making of Q which has about 6.02 x 10^23 tokens in the place representing CH4.

Jade Master (Feb 13 2021 at 03:39):

And the step in the recipe, represented by the transition combining one mole of methane with two moles of oxygen, could get mapped to one mole of the transition instances in Q.

Jade Master (Feb 13 2021 at 03:40):

...and the rest of the data of R is determined similarly, making sure that everything is symmetric monoidal.

Jade Master (Feb 13 2021 at 03:42):

I didn't describe this in my example but some features of this approach is that one step in the recipe could get mapped to (a sum of) a sequence of chemical reactions in Q. Maybe this is something like a mechanism? Also the firing sequences of P could represent steps which must be performed in parallel.

Jade Master (Feb 13 2021 at 03:43):

My question is if this really represents things that chemists really do. So if there are any chemists reading then lmk :)

Jade Master (Feb 13 2021 at 03:51):

I guess that the absurd numbers of tokens in Q is probably impractical for most purposes...

Jade Master (Feb 13 2021 at 03:52):

Also this relates to @Fabrizio Genovese's ideas about extensions of Petri nets. This is an example of an extension in the sense you've been exploring I believe i.e. functorial semantics from the category of executions of a net.

Joe Moeller (Feb 13 2021 at 05:29):

Are there any transitions in these Petri nets?

Jade Master (Feb 13 2021 at 07:41):

Lots! In Q they represent chemical reactions and in P they represent steps in your recipe. I should draw some pictures to explain better... maybe tomorrow.

Fabrizio Genovese (Feb 13 2021 at 09:50):

Jade Master said:

Then the functor R would map the place representing on mole of CH4 to the making of Q which has about 6.02 x 10^23 tokens in the place representing CH4.

I'd refine this a bit: If you are going micro-to-macro, probably what you want to really describe is a functor that maps a Petri net to a stochastic net

Fabrizio Genovese (Feb 13 2021 at 09:51):

I never really tackled stochastic nets yet, but the criticism that all chemists move when we do Petri nets is that the quantities are too big to make them useful in practice. So what you want is a way to extract a system of differential equations from the net, that you can numerically plot

Fabrizio Genovese (Feb 13 2021 at 09:52):

I should also mention that the equation attached to a stochastic net is called the "Master Equation", you may interpret this as a sign if you like :grinning:

Jade Master (Feb 13 2021 at 15:50):

It's actually macro to micro...but you're right this would make more sense with some stochasticisty. The problem is that I don't know a correct categorical operational semantics for stochastic nets. Do chemists ever do discrete simulations, maybe when the reactions are on a very small scale (maybe something happening inside a single cell)

Jade Master (Feb 13 2021 at 15:54):

Probably those discrete simulations are still stochastic.

Jade Master (Feb 13 2021 at 16:47):

https://en.m.wikipedia.org/wiki/Artificial_chemistry I think I've described an artificial chemistry

John Baez (Feb 13 2021 at 17:03):

Hi, Jade! It's weird - I was talking to Evan Patterson and others about this sort of map

$R : FP \to FQ$

in our discussion last Thursday, because it came up in something Evan was doing. But he was doing something else with these maps.

One cool thing is that these maps are more or less morphisms in the Kleisli category of the monad coming from the adjunction

$F : \mathsf{Petri} \to \mathsf{CommMonCat},$
$U : \mathsf{CommMonCat} \to \mathsf{Petri} .$

Jade Master (Feb 13 2021 at 17:10):

Oh yes true, I see that.

John Baez (Feb 13 2021 at 17:11):

They would be morphisms in the Kleisli category of the monad $U F$ if $\mathsf{CommMonCat}$ were the category of algebras of $U F$. We've never answered this question, and it's a good pure math problem.

John Baez (Feb 13 2021 at 17:11):

Anyway, these morphisms you're talking about are good things regardless of whether Petri nets are exactly the same as algebras of $U F$.

John Baez (Feb 13 2021 at 17:12):

I hadn't thought of how you are wanting to use them: as a way to scale up the number of tokens in a Petri net.

John Baez (Feb 13 2021 at 17:13):

The kind of example I got excited about was a bit different.

John Baez (Feb 13 2021 at 17:22):

For example, oxidation of sugar in a cell can be described as this reaction:

$\mathrm{C}_6\mathrm{H}_{12}\mathrm{O}_6 + 6\mathrm{O}_2 \to 6\mathrm{CO}_2 + 6 \mathrm{H}_2\mathrm{O}$

However, in reality this is just a summary of a reaction with many more steps and many intermediate chemicals!

We could describe this fact using a map $R : FP \to FQ$ where $P$ is a simple Petri net and $Q$ is a complicated one.

John Baez (Feb 13 2021 at 17:23):

The single reaction (transition) I wrote above would be mapped to a morphism composed of many reactions.

John Baez (Feb 13 2021 at 17:25):

Evan had other nice examples of maps $R: F P \to F Q$.

John Baez (Feb 13 2021 at 17:25):

So I think your idea of - I'll call them "Kleisli morphisms between Petri nets" - could be pretty generally useful.

Morgan Rogers (he/him) (Feb 13 2021 at 17:28):

John Baez said:

We've never answered this question, and it's a good pure math problem.

Is the question "Is $U$ monadic?" or something else?

John Baez (Feb 13 2021 at 17:31):

On your other question:

The problem is that I don't know a correct categorical operational semantics for stochastic nets.

@Evan Patterson is trying to work that out. I've wanted to do it for a while, and I think I know roughly how it works, but I didn't have a student who wanted to work on that. :upside_down:

Do chemists ever do discrete simulations, maybe when the reactions are on a very small scale (maybe something happening inside a single cell).

I think so: things work differently when you have small numbers of tokens. But the people who really do these stochastic simulations of Petri nets are biologists describing the interactions of organisms - population biologists. There small numbers of tokens can be very important.

This is a very good how-to book on this stuff:

• Darren James Wilkinson, Stochastic Modelling for Systems Biology, Taylor and Francis, New York, 2006.

Fabrizio Genovese (Feb 13 2021 at 21:03):

John Baez said:

For example, oxidation of sugar in a cell can be described as this reaction:

$\mathrm{C}_6\mathrm{H}_{12}\mathrm{O}_6 + 6\mathrm{O}_2 \to 6\mathrm{CO}_2 + 6 \mathrm{H}_2\mathrm{O}$

However, in reality this is just a summary of a reaction with many more steps and many intermediate chemicals!

We could describe this fact using a map $R : FP \to FQ$ where $P$ is a simple Petri net and $Q$ is a complicated one.

Well, this is exactly why in "Petri nets are monoids" morphisms of Petri nets aren't a couple of functions on places/transitions, but a function on places and a homomorphism of multisets on transitions

Fabrizio Genovese (Feb 13 2021 at 21:05):

The idea is that those morphism are simulations, that are indeed the relevant concept of morphism when you are doing Petri nets in automata theory. A morphism of Petri net is that sense is precisely intended as being able to "Compress/summarize" many transitions into one

John Baez (Feb 13 2021 at 22:10):

Yes, I was going to add that Montanari and Meseguer consider this sort of morphism. I didn't like it when I was trying to understand the category of Petri nets, because it's not the "obvious" or "basic" sort of map between Petri nets: it involves a mix of syntax and semantics. But now that I understand categories of nets, I'm a lot more interested in this more general notion of morphism!

John Baez (Feb 13 2021 at 22:14):

By the way, @Jade Master, here's another way to think about "chemical recipes". Thanks to your work there's a concept of "real Petri net" where a transition can use any real number amount of something, like:

$0.3 \text{ liters of water} + 0.4 \text{ kilograms of flour} \to 1 \text{ loaf of bread}$

And thanks to your work there's a functor from the category of Petri nets to the category of real Petri nets.

John Baez (Feb 13 2021 at 22:16):

So, you can take an ordinary Petri net describing chemical reactions, like this:

Combustion_reaction_of_methane.jpg

John Baez (Feb 13 2021 at 22:16):

then convert it to a real Petri net where the numbers represent moles, and then "scale it up or down" by any constant factor.

John Baez (Feb 13 2021 at 22:20):

There should also be a functor from Petri nets to real Petri nets where "carbon" gets mapped to "12 grams" because a mole of carbon weighs 12 grams, oxygen gets mapped to "16 grams", and so on. Then we'd get a real Petri net where chemicals are measured according to mass!

John Baez (Feb 13 2021 at 22:21):

(Above I'm guessing that for any number $x$ there's an endofunctor on the category of real Petri nets where we rescale the amount of all species involved in any transition by multiplying it by $x$.)

Fabrizio Genovese (Feb 13 2021 at 23:01):

John Baez said:

Yes, I was going to add that Montanari and Meseguer consider this sort of morphism. I didn't like it when I was trying to understand the category of Petri nets, because it's not the "obvious" or "basic" sort of map between Petri nets: it involves a mix of syntax and semantics. But now that I understand categories of nets, I'm a lot more interested in this more general notion of morphism!

For me it was the opposite. I wasn't interested in the morphisms we defined in categories of nets in the beginning because they weren't the right choice from a Petri net perspective, and ended up complicating my life a lot. Then I gave up and started using the most suitable from a categorical perspective. But I do agree that we could now characterize Petri net (bi?)simulations as extensions of nets, which would be a very cool thing to do

Jade Master (Feb 14 2021 at 02:33):

@Morgan Rogers (he/him) Yes that is the question. I am currently guessing that it's not monadic but I'm not sure.

Jade Master (Feb 14 2021 at 02:43):

@John Baez @Fabrizio Genovese know that we understand the operational semantics a bit better I think we might be able to understand the Montanari-Meseguer style morphisms a bit better. They seem like some sort of Kleisli morphisms for some sort of semantics. Is that what you're getting at?

Jade Master (Feb 14 2021 at 02:50):

@John Baez Regarding the real nets. For what it's worth I do think for every real r, there is an endofunctor $\mathbb{R}-Net \to \mathbb{R}-Net$ like you described. You might be able to get it from an endofunctor on the Lawvere theory for R-modules.

Jade Master (Feb 14 2021 at 02:51):

Also I am curious about the context and motivation you had for these ideas about real nets.

Fabrizio Genovese (Feb 14 2021 at 14:18):

Jade Master said:

John Baez Fabrizio Genovese know that we understand the operational semantics a bit better I think we might be able to understand the Montanari-Meseguer style morphisms a bit better. They seem like some sort of Kleisli morphisms for some sort of semantics. Is that what you're getting at?

I tried to partially classify those morphisms in this paper: https://arxiv.org/abs/1909.03518
which though I have completely rewritten and submitted to a journal. Essentially, I define a net with a semantics as a functor $PS \to S$, where $S$ is any symmetric monoidal category, and a morphism of nets with a semantics as a functor $PS \to PQ$ that makes the obvious triangle commute. Notice that when $S$ is the terminal category, my definition of morphism completely overlaps with yours

Fabrizio Genovese (Feb 14 2021 at 14:26):

Now, what I do in that paper is classifying those functors. Essentially, everything relies on the fact that you can do colimits both in Petri nets and in symmetric monoidal categories. There are three kinds of relevant morphisms here:

• Transition-preserving functors are exactly those that we use in categories of nets. These are functors that arise from morphisms of Petri nets.
• Identifications are functors that glue places in a net together. We can use these functors to glue nets together in a slightly weird way: We take two nets $N, M$ and a witness net $W$. We define transition preserving functors $W \to N, W \to M$ and we prove that their resulting pushout is an identification from the coproduct of $N,M$ to the glued net. We can recover the pushout formalism from here.
• Synchronizations are functors that send generating morphisms of a net to executions of another net. They do what you were talking about in this discussion, and correspond to simulations in Petri Nets are Monoids. I interpret this as synchronizations: We use a transition in the domain net to trigger an execution in the target net. I also proved that noteworthy synchronizations amount to do a double pushout rewriting of Petri nets, which is kinda cool because this is exactly what the Petri net community uses. I also sketched how we can use this to recover the other open Petri net framework (the one of Sobocinski, Bonchi, Gadducci etc) which is based on identifying transitions of nets.

Overall I don't like this paper too much because I feel it could be done in a cleaner way categorically. I remember John just saying that what I was doing was kinda obvious since there were colimits in both the categories of Petri nets and Symmetric monoidal categories. I thought of restating things better but it was a time when all my papers were being rejected, so I joust thought "F it" and left it there as it is. The new version is a bit cleaner, but still not as clean as I'd like it to be categorically.

Fabrizio Genovese (Feb 14 2021 at 14:27):

In any case I'm happy to go into more detail with you if you think it's worthy, it'd be cool to clean this thing up and making it precise. :smile:

Fabrizio Genovese (Feb 14 2021 at 14:29):

One small thing: I think considering nets with a semantics is fundamental if you want to do applied stuff. I know this is not important for chemistry but it really is for distributed systems. So the question that I was trying to ask there was "Can I glue things together in a way that respects semantics?" The obvious result was that I was constantly working in a slice category. This has never been really a problem up to now, so I'd suggest to do the same unless we find out that something breaks down really seriously.

John Baez (Feb 14 2021 at 17:32):

Jade Master said:

Also I am curious about the context and motivation you had for these ideas about real nets.

In industrial chemistry people don't count always individual molecules; they probably say stuff like "take 5 liters of water and add 6.3 milligrams of quinine", so they are more or less using real number amounts of stuff.

John Baez (Feb 14 2021 at 17:33):

So, the functors I was talking about, where you translate an ordinary Petri net into a real Petri net and can then "scale it up" by any real number, seem like formalizations of things people are already doing.

Spencer Breiner (Feb 16 2021 at 18:34):

Hi all. Thought I would mention that the same sort of morphisms show up in our paper on string diagrams for documenting manufacturing processes (here, NB: the journal murdered the formatting of the diagrams). There the idea is that your morphisms can represent the relationship between a high-level version of a process plan, and a lower-level version. So we might have a factory-level plan $f\in\mathcal{F}$ (this machine, then that one, ...) and map that to a plan at the level of individual workstation operations (drill, cut, screw,...).

In that case, it is also important that we can take colimits of the nets/categories. That allows us to describe each workstation category/net $\mathcal{W}_i$ independently, and then interpret $f$ in the colimit $\mathcal{F}\to\bigoplus\mathcal{W}_i$ (relative to shared resources, say) .

Jade Master (Feb 16 2021 at 22:50):

Thank you Spencer, that is very interesting :)

John Baez (Feb 17 2021 at 02:24):

Cool! Btw, @Spencer Breiner, we continued talking about some technical aspects of these matters here.

John Baez (Feb 17 2021 at 05:05):

By the way, @Spencer Breiner, PubMed seems to be a bit snide about category theory:

.

Jade Master (Feb 17 2021 at 15:16):

I sure hope not

Keith Elliott Peterson (Aug 15 2021 at 02:39):

Just a suggestion, but can we add in other chemical species other than just atoms and molecules?

For instance, the oxidation half-reaction,

$$6\text{Fe}^{2+}\to 6\text{Fe}^{3+} + 6\text{e}^-,$$

takes in 6 $\text{Fe}^{+2}$ cations, and outputs 6 $\text{Fe}^{3+}$ cations and 6 electrons.

Jade Master (Aug 15 2021 at 04:22):

Oh yeah that's a good idea.

Keith Elliott Peterson (Aug 15 2021 at 09:19):

A little off-topic digression, but solvated electrons are neat!

Who would have thought electrons are gold in colour at high concentration?

Liquid Electrons - Periodic Table of Videos

ww (Oct 15 2021 at 09:51):

Not to open a can of worms (haha) but what about polymers?

ww (Oct 15 2021 at 09:55):

Screenshot-2021-10-15-at-10.54.57.png

John Baez (Oct 15 2021 at 12:17):

I think there are alternatives to Petri nets / chemical reaction networks that advertise themselves as being more efficient for dealing with polymers, but I've never looked into them very hard. Luca Cardelli at Oxford has done a lot of work on the interface of chemistry and computation, and he'd be the one to ask about this. It just struck me that colored Petri nets might do pretty well.

ww (Oct 16 2021 at 09:24):

Aye, there are. We use graph rewriting for this, but I'm still a bit unsure about the precise relationship between that and (coloured) Petri nets. In practice, they feel very similar. I _think_ that if you restrict to discrete graphs, what you get is like a Petri net. I'm pretty sure you could represent the original question in graph land: the cation looks like a star motif with nucleus in the centre and edges to a bunch of electrons. But that might not be the most efficient way to do it, and writing it out in a textual language with a couple of dozen electrons would be annoyingly verbose.

ww (Oct 16 2021 at 09:30):

Actually, Kappa has recently evolved the idea of counters. That would work pretty well:

Fe(e=24), Fe(e=24), Fe(e=24), Fe(e=24), Fe(e=24), Fe(e=24) ->
Fe(e=23), Fe(e=23), Fe(e=23), Fe(e=23), Fe(e=23), Fe(e=23), e(), e(), e(), e(), e(), e() @ k

A little verbose because there's no syntax for just saying "six of these".

I think this might just be equivalent to a notation for coloured Petri nets, as you say, because here there are no edges/bonds. The colours are the type of particle (e.g. iron atom or electron) and the count of electrons in the case of Fe...

ww (Oct 16 2021 at 09:33):

If we don't mind having potentially very many places, I think we don't even need colours. Just places called Fe23, Fe24 and e would do.

ww (Oct 16 2021 at 09:39):

Feels to me like there is a functor that takes a certain kind of graph rewriting into coloured Petri, and then one that goes to colourless Petri...

ww (Oct 16 2021 at 09:54):

Actually, this is definitely the case because it's what you do when generating ODEs for observables of a graph rewriting system, for example. So long as you don't have rules that do things like generate unbounded polymers, or are happy to truncate the maximum number of electrons that can be bound to an Iron atom (i.e. set of colours), you can do this finitely. Finitely, but still a potentially unreasonably high dimensional ODE system that isn't so computationally helpful. Gillespie still works ok though for the same reason.

Fabrizio Genovese (Oct 16 2021 at 14:13):

ww said:

Actually, Kappa has recently evolved the idea of counters. That would work pretty well:

Fe(e=24), Fe(e=24), Fe(e=24), Fe(e=24), Fe(e=24), Fe(e=24) ->
Fe(e=23), Fe(e=23), Fe(e=23), Fe(e=23), Fe(e=23), Fe(e=23), e(), e(), e(), e(), e(), e() @ k

A little verbose because there's no syntax for just saying "six of these".

I think this might just be equivalent to a notation for coloured Petri nets, as you say, because here there are no edges/bonds. The colours are the type of particle (e.g. iron atom or electron) and the count of electrons in the case of Fe...

There's for sure work by Nicolas Behr and colleagues about representing Kappa and MOD as rule-based graph rewriting systems, I don't know if it's useful: https://arxiv.org/abs/2003.09395

ww (Oct 17 2021 at 08:16):

Fabrizio Genovese said:

There's for sure work by Nicolas Behr and colleagues about representing Kappa and MOD as rule-based graph rewriting systems, I don't know if it's useful: https://arxiv.org/abs/2003.09395

I remember Nick well from when he was in Edinburgh, and Jean Krivine was one of the examiners of my thesis, but I hadn't seen that paper. Thank you, one for the reading list.

Actually, cited in the first paragraph is this one: Rule Algebras for Adhesive Categories [ https://arxiv.org/abs/1807.00785 ]. If I am understanding correctly, it seems to say what I was intuiting above: rules are creatures of $\mathcal{M}$-adhesive categories, Petri is an example of an $\mathcal{M}$-adhesive category which corresponds to rules on discrete graphs.

Fabrizio Genovese (Oct 17 2021 at 15:00):

Yes, I know this line of work only very roughly, but if I recall correctly the definition of adhesive category was created exactly as a categorical answer to the question: "In what environments we can do rewriting in a nice way?" Essentially, when your category is adhesive you can apply a lot of techniques from graph rewriting (DPO rewriting etc) very straightforwardly :smile:

John Baez (Oct 18 2021 at 13:36):

ww said:

Feels to me like there is a functor that takes a certain kind of graph rewriting into coloured Petri, and then one that goes to colourless Petri...

As for the second, yes: it's standard lore in the Petri net world that anything you can do with a colored Petri net you can do with a (bigger, more annoying) Petri net, so that colored Petri nets are introduced only for convenience, not greater computational power. My students @Joe Moeller and @Jade Master were writing a paper on the functor that turns a colored Petri net into a Petri net, but they gave up when @David Spivak and @Fabrizio Genovese came out with a similar (but not isomorphic!) paper.

John Baez (Oct 18 2021 at 13:37):

I kept telling them they were making the newbie mistake of thinking that one paper on a topic diminishes the interest in other related papers on that topic... unless you're proving the exact same theorem it probably has the opposite effect.

Fabrizio Genovese (Oct 18 2021 at 16:56):

Yes, especially since the most important part of both papers was introducing the technique of using the Grothendieck construction to do stuff, an approach that proved so successful that we ended up writing five or six more papers about it lol

Fabrizio Genovese (Oct 18 2021 at 16:57):

(And at this point I'd be very glad if someone could pick it up and investigate things further, we've already too much on our plates right now!)

Joe Moeller (Oct 18 2021 at 17:41):

Puzzled over the use of the word "introduced" here, but I'd certainly be happy to pick up some of the threads you've been laying down. My career is essentially based on finding uses of the Grothendieck construction :sweat_smile:

Fabrizio Genovese (Oct 18 2021 at 18:04):

What I meant is that the idea of using the Grothendieck construction to internalize a coloured Petri net back to a classical Petri net was first exposed in the papers cited above, around 2020. Even if, to be precise, said application is something that me and David figured out in early 2018 when he came visiting in Oxford, but never bothered to write. And indeed I talked about it very excitedly with everyone during ACT in Leiden. Then two years later we decided to finally write it down properly after the Statebox summit in Berlin, and the paper came out. What I definitely did not know in 2018 (and not even in early 2020 to be honest) is that the case of coloured nets was just one of the many applications we could devise, and that indeed this techniques could be adapted to many other extensions of Petri nets, such as bounded and hierarchical. This basically came out in early 2021 and now we have a far better idea of how powerful all this is

Jade Master (Oct 18 2021 at 18:06):

Fabrizio I remember telling you about it during the Statebox summit in 2018 :thinking: Regardless I don't care. John told me about it earlier in a seminar he gave in 2017. There might still be notes from it!

Fabrizio Genovese (Oct 18 2021 at 18:06):

So now I don't see those papers anymore as "describing an application" but as "introducing a general technique to describe extensions of Petri nets", that is far more interesting in my opinion.

Fabrizio Genovese (Oct 18 2021 at 18:07):

I definitely remember telling you about this in Leiden in 2018. I also mentioned how the collage of profunctors could have a role in all this, but that approach was never developed further, not by us at least.

Joe Moeller (Oct 18 2021 at 19:09):

I wrote network models (using GC) in 2017, and I was in the middle of writing monoidal Grothendieck construction when I was at ACT in Leiden. I remember chatting with you Fabrizio about the GC, but we should've talked more!

Fabrizio Genovese (Oct 18 2021 at 19:35):

Just to be clear, what I am referring to is the Grothendieck construction applied to the context of Petri nets. I have no doubt that there were - and are - many people using it to do all sort of stuff in ACT, way before I even knew it existed. What I am saying is that the papers John cited before are the first ones applying it to the context of Petri nets, that turned into a well-defined line of research for me in the last year or so.

Joe Moeller (Oct 18 2021 at 19:39):

Definitely, I'm not attempting to refute your claim or anything! I'm just trying to map out the common interests, and lamenting not talking with you more!

Fabrizio Genovese (Oct 18 2021 at 19:57):

Well, I've been thinking more about this stuff during covid basically, which for sure didn't help. I'm sure this is true for many things people have been working on

Fabrizio Genovese (Oct 18 2021 at 19:58):

I find it very exciting to be working in person, while interacting online really draws my energy away. So for sure this made, at least for me, communication more difficult :smile:

Daniele Palombi (Oct 19 2021 at 10:35):

Fabrizio Genovese said:

I find it very exciting to be working in person, while interacting online really draws my energy away. So for sure this made, at least for me, communication more difficult :smile:

Pisa was really helpful with that, phew!

Daniele Palombi (Oct 19 2021 at 10:39):

Fabrizio Genovese said:

(And at this point I'd be very glad if someone could pick it up and investigate things further, we've already too much on our plates right now!)

Yeah, more people should come work on this and join efforts to establish it as a proper subfield of ACT :smile:

Daniele Palombi (Oct 19 2021 at 11:01):

Joe Moeller said:

Puzzled over the use of the word "introduced" here, but I'd certainly be happy to pick up some of the threads you've been laying down. My career is essentially based on finding uses of the Grothendieck construction :sweat_smile:

To be fair, using the GC for refining types and processes in concurrent systems has been around since at least 1997, so no one here can claim originality on that

Daniele Palombi (Oct 19 2021 at 11:06):

Daniele Palombi said:

since at least 1997

I'm talking about Specifying interaction categories by Abramsky and Pavlović. Maybe @dusko can tell us more about the origins of this wonderful idea :grinning:

fosco (Oct 19 2021 at 13:24):

Fabrizio Genovese said:

I definitely remember telling you about this in Leiden in 2018. I also mentioned how the collage of profunctors could have a role in all this, but that approach was never developed further, not by us at least.

I have been summoned by the word profunctor.

dusko (Nov 11 2021 at 23:22):

Daniele Palombi said:

Daniele Palombi said:

since at least 1997

I'm talking about Specifying interaction categories by Abramsky and Pavlović. Maybe dusko can tell us more about the origins of this wonderful idea :D

oh sorry, i didn't notice the question. (computers used to be useful to connect us with friends, but now i need friends to connect me with computers.)

i guess you are talking about the "generalized grothendieck liftings" to arbitrary functors, which we use there. the reason why we use them there are obviously samson's specification structures, which he invented to specify interaction categories. so that was one component.

the other component is the view of grothendieck construction as 2-comprehension. that was what my thesis was originally about: in toposes, you have the comprehension of predicates, in dependent type theories, you have the comprehension of indexed propositions. grothendieck categorified the correspondence of sheaves and etale spaces as their comprehensions to propose his construction of discrete fibrations as comprehensions of presheaves. then he defined general fibrations as comprehensions of what came to be known as indexed categories, which he needed to define descent data and ascend to stacks. well then you normally ask yourself: what would at this 2-dimensional level correspond to lifting comprehensions from predicates to dependent types in lawvere's doctrinal diagram? and you calculate the answer: the 2-dim predicates are lax functors to some sort of monoids. and the simplest category of monoids is Span. hence Cat/CC ~ [CC,Span]_lax, and the corresponding 2-dim doctrinal diagram.

but at the time we thought that the purpose of categorical semantics was to better understand type theory and logic, to make programming easier. (like that can be done by math.) the business of going into higher dimensions seemed like a way to construct more things that we don't understand, not a way to understand things that we construct. so none of that higher comprehension stuff went into my thesis. only a bit in the beginning i think.

hmm. what i said above: "grothendieck categorified the correspondence of sheaves and etale spaces" --- still sits in my throat. the man who invented categorification as the method to localize spectra, and then simplified it to generalize galois descent, and then categorified the comprehensions, and 10 other things --- the only thing he didn't invent was the word "categorification". i hope he doesn't mind about such things any more.

dusko (Nov 11 2021 at 23:30):

BTW,

i guess you are talking about the "generalized grothendieck liftings" to arbitrary functors, which we use there. the reason why we use them there are obviously samson's specification structures, which he invented to specify interaction categories. so that was one component.

i spent a lot of time thinking about interaction categories, and never wrote anything about them since 1997 --- until last year. and if the 1997 paper was of interest, then this one might also be:
http://arxiv-export-lb.library.cornell.edu/abs/2007.10057