Wolfram Physics Project: Relations to Category Theory

let me just give an introduction and then we'll go on okay hi everyone so today we are doing a live stream with some guests talking about connections to category theory it's something that several people have requested frankly I'm always afraid of category theory category theory is sort of the the purports to be the most abstract current game in town for thinking about mathematical kinds of things and I have only very slowly understood a very small amount about category theory but it is clear from the small amount that I understand that it has lots of relevance to things that we're doing and so our goal today is to try to understand more about relations of our physics project category theory and I do have to tell one story here related to Fabrizio who's who's joining us today how I met Fabrizio we were at South by Southwest Conference at the trade show there and there was a whole there were a whole bunch of wild things at the trade show and you know you walk up to one booth and he was what do you do and the person says we are released saying we want that we have a giant industrial robot and we're going to make it dance another person says some we're there's real things from that actual trade show that we're we're um we've got a scheme for having satellites release stuff into the upper atmosphere to generate giant consonant sized firework displays then I woke up to this next booth and I say what do you do and that was for RIT CEO and he said I do category fication of Petri Nets I was like that's that's very different from the robot next door but anyway that started a bunch of very interesting conversations from only 20 in the conversation yeah I figured that that was that was some yeah no it was it was that was why that one made the whole thing more amusing that that it's like they're robots and there's categoric asian of battery right yeah it was a good conversation that's one of many um so let's see for us today what where should we start I think let's maybe start off talking about kind of the the modern view of what is category theory I mean you know category theory originated in you know in the world of sort of organizing algebraic topology and things like that and it's been through so so maybe you guys I'm curious if you guys can sort of characterize how should one think about category theory today well I think basically as you say right from the start of unification theory basically the 40s and the 50s you know to where there was a lot of work that was being done in mathematics in that areas with some overlaps so maybe you know people were studying Proctor's the same time geometric an algebraic and stuff like this and people found themselves in this weird circumstance where they have very well-developed theories of you notice Edo period groups of brains of spaces and then study how these things interrupted was actually very difficult and then at some point people started to think oh maybe we need a theory to talk about the relationships between different theories and actually I think that one of the reasons why category theory and you know this infamous this Fame of being super complicated is because the kind of stuff that motivated the creation of category theory was actually super complicated and so unfortunately the like normally four people were inducted to category theory just from the worst part of it from the most complicated part and not by the way four bits are just practical point is it possible for you to move closer to the microphone or some other some in some other way and make it less echoey it's just a bit too it's it's we can know because we're hearing the echo from the room I think I think that's the problem so that that's not that's not fixable okay no problem the unless anybody else has another idea how to how to improve that are you sure you're using that microphone as opposed to your computer's microphone yeah right this usually mode most it looks like you're in kind of an office like setting mobian yeah that's a lot better actually nice cool oh yeah that's perfect yes I had two microphones and I was using the wrong one sorry okay no problem great okay we were so category theory it's classic use in thinking about kind of the correspondence between different kinds of arguments and different mathematical structures yes and then fast forward a few decades people started realizing that these theory you know was actually useful also to talking about applied stuff and the reason for that is that indian category theory says it studies the relationship between very difficult very different entities it's actually pretty good to describe complex systems like you know many applied systems are probably the first two biggest success successes in that wine category theory have been functional programming which is basically entirely founded you see I find that very amusing I find that statement very amusing because I've you know for 40 years or something I don't functional programming languages and yet if that's a true statement I really need to understand it because I don't understand that at all important thing you know program are functions then you want to say everything you can about how these functions compose and at that point you know all the machinery that category Theory gives you becomes very very useful it's it's actually strange because in the end when you like do Oscar or stuff like that you are still working let's say in the category of sets like all your functions are functions between sets but the point of view of category theory is practically different and and and that's what actually gives you something see for example in in symbolic functional language like Wolfram language the the idea of mapping between sort of kinds of objects is very weird and it's something that you know like you know the denotational semantics guys and Dana Scott and so on for for four years Dana has been sort of I think a little bit confused about how it fits into that way of thinking because what we're dealing with is sort of you know we have these symbolic expressions and their general symbolic expressions and we're making transformations on those and that's different from saying you know the symbolic expressions have a life of their own it's not just it's a thing in this pool of possible things of a certain type and you know maybe we should maybe this is the wrong I mean maybe a characterization thing I'm curious about so you're you're saying I'd like to understand this correspondence that you're describing between the function languages and category theory but Tim you know maybe I can ask I mean a you know in my efforts to understand what category theory is and you know morphisms all these kinds of things I mean there's some structural aspects of category theory which are a bit like graph you know that where you're dealing with things like graphs is that a fair I mean and but they're graphs with certain special associativity properties on their on their edges even more actually basically you can see a category as the transitive closure of a graph so the idea is that every time you have an edge from a and B and one from B and C you also have one from a and C represents the composition of the two and me and also you have identities so for each vertex of the graph you want an edge that is they do nothing kind of thing that goes from a from a to a and you can see that basically if you give me a graph I have a canonical way of building a category out of this graph so I basically take the edges and I complete adding formally all the possible compositions and their identities and this is a exactly called the free category generated by a graph and you can also do the opposite well you can take a category and forget that is a category and just treat it as it was graph basically and the nice thing about category theory is that you can see say that these operations are actually a couple of a joint factors so what it means is that it's not just like that I can build the category out of a graph it's also that if you give me a graph transfer me I can mock it to a transformation of the corresponding categories and again that's pretty much obvious because if you if you tell me these vertex goes to these vertex and these edge goes to these edge then I can formally extend these mapping to all the formal compositions that I introduced in the categorical word so hold on second so let me see if I understand what you're saying let me let me let's um let's actually start to fortunately the way I have my computer set up today it's going to be difficult for me to alright let's let's do this okay so let's say you're saying we have some random graph so we you might have some some graph that just looks like bigger actually random directed graph okay all right you want a random directed golf let's make a random directed graph how big would you like it to me let's just have ten let's do something like this there's a round okay let's let's make sure actually I'm not sure let's see see if we say directed edges are true okay there's a random directed graph fall okay so we can take you you mentioned transitive closure I mean we could say let's get the whoops the transitive closure graph for this graph okay so it's a the transitive closure is a big mess yes and also you want to join identities so we want self loops for every one of yes okay so we could do that we could just say I don't know how we best do this but but um well let's say we just get to say just just to draw a definite graph let's append to the edge list of this graph a something that says actually that's joined to the edge list of that graph something that Maps hash goes to hash over the vertex list of that graph and then let's go out of that so this should have little ears or hum there we go okay alright actually when you did the transitive closure there it's automatically like recursively done or okay so yeah basically this would be the underlying graph to the free category coming from the graph above well I say that this is the underlying graph because at the moment this implant when we look at this graph obviously we cannot tell that the loops have to behave like identities or that some things that we are introducing our compositions of edges this information is now forgotten from the categorical structure but this is exactly the underlying structure of the free category generated by the graph above but a cool thing is that if you map if you go all the way up to the our first graph and you map it to some other graphs and by mapping I mean we have a function from vertexes to vertexes and a function from edges to edges so that source and target of each edge are preserved then it is that we can lift this to morphism between the corresponding three categories let's start with something much simpler okay so we've got this graph and you say so you're gonna label every edge every edge is going to have an actual we're going to they have actual names mm-hmm right so I'm say edge labels that's and the okay so then now everything has a name okay now what am I gonna do so now I'm going to take this and for every one of those named vertices I'm going to say two maps and I maybe I have some other graph here yes and let's let's make another graph um let's say okay there was another somewhat similar graph maybe I admit them I mean changed some parameters here let me say we say four vertices there and five edges ok so there's another graph okay so now you're gonna you're telling me make a mapping from this graph to this graph is that right if you can yes it's not always possible clearly if you want to preserve source and target of each well we took so a mapping means what it means I'm taking it means that you are basically mapping the vertexes of the first graph to the vertices of the second graph as you want and then you are mapping the edges of the first graph to the edges of the second graph in a way so that the endpoints of the edges are compatible with the mapping you gave on the vertexes so for instance what I'm saying is that if you want to map to to tree to something then you basically have to make sure that the vertex is 2 and 3 get mapped to the vertexes of the target edge so for instance if you map 3 to 2 then you cannot map 2 to 3 to 4 to 1 because in that case you are losing the correspondence between the source and the target of the edge I think I need a much simpler example let's take let's start off with something much more trivial which I think is is let's say I have a path graph ok so um ok there's my first graph yes let's say and now ok and then I have another one of these let's say I have 5 edges in that one yes ok now what does it mean to do a mapping from one to another well in this case it means that you can map every number in the first one to the same number or bigger in the second one so for instance if you if you map 1 2 1 2 2 2 3 2 3 & 4 2 4 and you know all the edges to the edges between 1 2 2 & 3 3 & 4 and that's about it nothing but for instance if you map 1 2 1 & 2 2 2 then you cannot map the edge that goes from 1 to 2 to the edge that goes from 4 to 5 because you are losing the endpoints but let me see if I understand the context of this so in traditional and category theory if one thinks about I mean let's just do an example of this I mean talking about this in terms of these this is some morphism if I understand correctly mapping example what so in this case what we are doing or we are defining a category of graphs so actually graphs will be the objects of our categories and the mapping I'm talking about are the right kind of structure preserving morphism you want to pick so the idea is if you want to map a graph to another graph what is the relevant structure that you you want this mapping to preserve so for instance in the case of a group then we know that a mapping has to be a normal morphism because the relevant structure of the group is an operation it's like the group multiplication and inverse and we want mappings that preserve these these operations otherwise they do make sense from the perspective of groups so in this case what is the relevant structure of the graph well the relevant structure of the of a graph is just that each Edge has a beginning and an end that our vertex is source and a target ok but the whole long side there's two different levels of what's going on here I mean there's the you know there's the objects that exist in this category and there's actual sort of category theoretic layer and then maybe higher order category theoretic layers that correspond to the the the the I think we need to okay let me let me ask maybe Jonathan who understands more about what I at least understand to if he can comment on this because I'm getting super confused already um what what level of stuff we're talking about here is I think we're talking about the construction of a category that is being constructed out of gras as a category of grafts yes yet it seems like a lot of the structure of category theory operates at the level of talking about transformations within categories between categories and so on which themselves are represented as graphs so yeah exactly there are two things that there's there's the category graph which is that which is the category that Fabricio has been defining there are also notions like the concept of a string diagram which give you a combinatorial way of representing a category in which you see two so with primitive correct me if I'm wrong but it's a string diagram each vertex is a morphism each edge is an object and so it gives you a wake you know given some arbitrary category it gives you a way to it gives you a combinatorial representation of the internet yeah basically yes in diagram is like you are dual izing things so let's say that points become lines and lines become points so yes like a mathematical example in the case of groups and the case of if you really want algebraic topology but it will be better if it was something less if you take that directed graph you generated above and you treat that as you know that's some some category this thing here well I mean any of them right any of the ones that we generates it to be cut that's not a category that's an object in a category I mean the category the thing above sorry this this thing we're talking about is an object in a category right yeah but but above you generated a thing that was supposed to be the cut of the record yes exactly which was the with how which had the identities and how's the transitive closure so if you take that object and you construct its dual do you have vertices for where the morphisms are and you have edges worthy where the objects are that would be a string diagram all right let's okay to help me not get just irreducibly confused can we talk about categories of things other than graphs but but the thing you constructed above we that's we don't know what that's a kateri off that's just a category of objects yes and this is represented so tell me so you can construct the string diagram of that so what I'm what I was trying to say before is that these that thing here that we generated that comes from a graph now the point is that this thing doesn't just come from a graph the point is that there is a relevant notion of transformation between graphs that will be transported to a relevant notion of transformation between categories so a functor and this thing is itself factorial so what I was trying to say is that the category graph as a factor that goes to the category cat where objects are categories and morphisms are factors so in the end these from the categorical point of view say is that yeah there is a very nice canonical way of building categories out of graphs and this canonical way behaves well with respect to how you transform graphs that's basically okay and let's let's come back the again sorry for the question yeah this this translate did this one toriel transformation between graphs and and the category of graphs is did you say that was an adjoint there is an adjoint from graph to cat basically okay and from graph to cut you just create to feel the free category out of each graph and in the other way there are way around you just forget that the categories are graphs you take category and you just consider it I wouldn't I mean how does the category of categories is that they are yes yes correct so we're already really in a little bit of deep water here by the time we can we start off with let's just take them for example talking about let's say functional programming or something like that can we talk about a really elementary example yes we can represent morphisms functors things like that in terms of in concrete so easy example would be you can have a category where your objects are types in your functional programming language and your morphism actually my life we have a Titleist language so okay let's assume we have types yes category is deeply connected to type theory so basically everything we do is tight so let's say we have a type we have type of integers and we might have a type that is something like an array constructor type we have presumably we have a base type and we might have some constructor of types is that right yes the Constructors do will be characterized as some other categorical things so I would leave them out for now because we've got okay so we got a strike like integer now what do we do then you can have for instance list int so lists of integers were way we were then I have a constructor so that's that's the point list int is a type list is a constructor so listing is the constructor applied to the type but if you want to describe a list then we'll need to talk about monads and and that's probably the left the next step so yes we have we have a type like that and we might have a type that's presumably list of list event yes exactly and then basically the idea is that you know you also you are functions between these types and these are your morphisms in this so for example I might have a function of an integer that returns an integer yes exactly I might have a function G of an integer that returns a list of integers yes and these will be of type the first one will go from int to int and the second one will go from int to listing okay so this one here is characterized as having type int arrow int yes okay yes and that okay so we've got two constructors here we've got the the the arrow constructor basically and we've got the list constructor yes so I understand why you say that arrow is a constructor but again it depends at what level you look things you look at things because you can say that F is just a morphism from int to int and then you are basically saying actually int to int is a type and that's oh that's true obviously but that depends on the fact that this particular category has a lot of nice machinery in it so in particular the fact that in twinkies itself type comes from the fact that the categories called monoidal closed but what it means is that basically you can consider that the morphisms between two objects in your category are themselves okay so in this this mapping a function returns something that's the morphisms are the arrows is that correct here yeah the morph isn't like yes so the idea is that yeah the morphisms are the arrows from a type to another type yes okay and then you agree that on each type you have an identity arrow that is basically the de morphine's minh that does nothing so for instance you can go from int to int and you just return what you got so there's an identity morphism for each type which is which would be have the property that it is basically the identity you know it's it's essentially something that just takes any type and returns that's it takes anything of that type that correct takes anything of that you have to think yes yes it for each type you will have a particular identity morphism this is the equivalent of the loops we will put in oh and it's time so give me a practical example of that so it for an integer for example is the identity morphism the integer comes back as the integer yes precisely yes okay so it is in fact an identity operation is that correct it's not just that an integer comes back as another integer it's the exact comes back as the same integer perfect yes okay yes absolutely and then you see that we also have a notion of composition namely if you have a function from A to B and one from B to C you can just pipe one into the other and get a function from A to C okay so hold on hold on hold on so let me just understand that so so what you're saying is if F Maps if F event returns an int yes G event returns a list event then I can perfectly well say the you know F of G of int returns something which is a in that particular case it's a list of int a way no should be G of F right if G returns a list of image then you can't apply F to it fine so that's a list of a well I haven't addthis very well but I understand that that that thing's type signature is int goes to in those two yes and when you compose your basically let's say forgetting what's in the middle then you're just saying that this goes from int to list of int yes yeah so in this case you see types are used to because they prevent you to compose April's apples and oranges basically you can compose I'm the wrong person to try and cell type - but yes I understand the anger I I mean I understand that types can get in the way especially when you want to do like fast prototyping or development it isn't that we don't need to the you know the idea of types I understand the idea of types the kind of the calculus of types you know we touch for experiments with this it's it's not I mean we can argue about whether that's useful but I don't think that's the main point here and I I want to understand maybe you can finally explain more clearly than I've understood before things like the Haskell what is it the courier what is it how well carry Howard Howard buy some more fission yes right okay so what I'm understanding here is that this is each one to tell me the terms here so this is how would you describe this this thing here that thing I would just not describe it at the moment because as I said to be able to speak about that thing categorically you need more machinery you have to say that the category is closed and this means that if your category is closed and I would say oh that's just a type which is the case for type theories usually but the point is that in general let me give you this example suppose I have two topological spaces okay and I have continuous functions between them you're some I don't know if this is the right example but maybe just the category of sets would be no because say I'm trying to find the non closed category that's exactly the point so I don't know if from this getting stuck on that it is not two functions right but yeah but like is top closed no okay so the idea is that if I have two topological spaces and I have continuous functions between them the set of continuous functions between these topological spaces is not itself a topological space indeed indeed so that but I understand that if you just talk about integers the set of functions between integers is not itself an integer exactly is not itself an integer but if you are looking at it from the point of view of sets then it is a set you can always say that function is let me understand that let me understand what you're saying so if I say integers mapped to integers right yes then that mapping in it sort in and of itself is not an integer I mean of course you could girdle number it and then it would be an integer yes I don't know how that relates to anything but you know assuming you're not doing computation theory then that thing is an integer but now if you say this is a mapping from sets to sets then you have a way to speak about an object you can even do into it the point is your context if those int R represent if you're working in the category of sets then you can say int is a set int is a set and the set of all functions between them is a set so the point is that within the category of sets you have a way to represent that arrow as an object while if your category is not the category of set that arrow may not represent anything in category so if we believe that the universe is computational we essentially have a category in which we can represent everything that is if if everything is a you know both the transformations and the objects can be represented computationally I mean in other words even if we could I mean basically with girdle numbering we could represent that function from integers to integers as itself an integer yes the the point of gittle numbering and the reason why this wouldn't precisely work in category theory is that these properties are always defined category theoretically as universal so you want to say that there is one and only one way to do things like category theory works up to canonical kind of stuff and the good ol numbering is not canonical at you you can choose to do the good ol numbering in another way I'm a little confused by that because use in the case of sets the the kind of the representation of a set your claim is that that sort of as soon as I'm saying it's a set that obeys the axioms of set theory then there's only one way to represent this collection of things as a set is that the claim up to isomorphism okay alright so you can real able the elements and things like that but there's but and you will always have a by action between your representations yes okay okay so um by the way I did notice that we had Matthew on this Matthew still here does he wanted to make some comment about some the how this relates to him because he's thought about all kinds of numbering and pairing functions and so on Matthew here the automated comment maybe not they've um okay alright so I am here okay did you want to make a comment on on the statement that there's no canonical pairing function which is basically what four bits here just said um no no III actually do not want to make a statement okay all right um okay but so I'm understanding that the this notion of a closed category is something where all the things that you're operating on and this whole these mappings are themselves representable in the category precisely so like in general in category theory you can always say I consider the set of morphisms between two objects if your category is as called an internal object or closed then you can actually say there is an object within my category that represents this set okay so you're saying that the main thing is there's a set of morphisms between objects and the question is can you represent can you represent those more prisons and that set can you represent that set as itself a member of the category exactly so an example of this would be vector spaces because linear applications between two vector spaces form themselves a vector space okay but so women that that's that is saying vector spaces with particular operations mapping back to spaces to vector spaces right your categories vector spaces as objects and linear functions as morphisms between them so you think those linear functions can themselves be represented as vector spaces yeah you can always send out them with a notion with a vector space structure in a quite canonical way because you can say the sum of these functions is defined by doing the some point wise in the target vector space so just to understand my my world of transformations between symbolic expressions so in my world you know expose expressions are have some structure they are their objects and you can think of them as being in some category now meanwhile the transformations between symbolic expressions are themselves symbolic expressions so I can have you know F of G of whatever so your category will be most likely closed or if you want to category Phi this you want to aim to have a closed category so this is an expression and this transformation rule is also an expression yes okay okay all right so what okay so I have these categories some of them are closed some of them are not closed you're saying the interesting ones tend to be closed is that true necessarily there are like for instance being closed when you do topological kind of stuff geometric kind of stuff is not that common that's the statement that in mathematics the I mean you know in a symbolic language functions you know programs and data are the same kind of thing I mean you're saying being closed is basically a programs and data at the same kind of yeah that's that's why this is at the heart of the heart of the curry our lung back isomorphism yes precisely okay it's because yeah you you can always consider like all the programs that carry you from A to B as a piece of data and and yet there is discourse on this okay all right so that's the notion of a closed category so in the in the case of for example graphs just to do the exercise when you're talking about mapping between graphs that mapping is probably itself represented as a graph right graph should be closed maybe matter can correct me yes so so for graphs when you say we have a mapping between graphs we're saying basically we've got a graph one of those graphs I had above you've got another graph and the mapping between graphs takes vertices to vertices for example yes itself can be represented as a graph just saying vertex a and the first graph goes to vertex two in the second graph yes basically I didn't work out the details but yeah the idea is that there is another graph that let's say faithfully represents this mapping between graphs yes right okay so so in or actually not a graph kind of mapping you have if you're saying like oh hey I was I was saying that the graph representing and mapping with ingre between graph is the graph you get by like first multiplying the two graphs together so that now you have vertices which are pairs of vertices the first one is the survivors from the first graph and the second one is directors from the second graph and and so on the unique stuff that gets sent to stuff so it's very well I'm not comply I can see that there's a way of okay within reach to say that what this graph category is closed it's obviously not within reach you're telling me it's not within reach to say that the integer category the category of integers and functions on integers is closed because you're not allowing gödel numbering for reasons I'm or or less understand though yes in other words the medium I mean you know programs equals data is clearly much more general than the things you normally think of as being data that represents programs but we're not we're not allowing that okay so now I think I understand I hope I understand so we've got the category of category of some kind of thing and we've got certain morphisms which are mappings from between objects in this category yes okay correct statement and I think that the most important thing that needs to be said is that the same kind of thing can be category five in different ways the real question we should ask is if I want to study for instance groups what is the relevant kind of transformation between these groups what what group like properties we want to preserve this gives us a notion of morphism and these gives us a definition of category but n the idea is that I that there are examples of of categories that I'm actually the same objects one one example for instance is topological spaces I can say that I have a category where my objects are topological spaces and my morphisms are continuous functions but I could also say no actually my objects are topological spaces but my functions are about okie equivalent equivalent classes of continuous functions so I am considering deformations up to Amata P and these will give me two very different categories even if the objects are the same and the reason is that I am focusing on different kind of transformations so that's the real power of category theory is being able to say to isolate the kind of property you care about so for instance each group is trivially also set you know just like you throw away the group operations and the underlying thing to the group it's a set and a group homomorphism is always a function between sets so you can also say that well actually I can I can see groups as a subcategory of sets and study them there but in doing that obviously you are losing the group like properties so the whole point of category theory is basically this is to being able to find the right definitions that you know represent the things you care about and in fact in our work is like 80 percent of the time you you use it just to define things and 20 percent of the time you use it to prove things because when your definitions are the right ones the proofs they will just follow because you know they basically follow canonically from the definition is is actually quite rare to to have a really hard right that's why that's why people don't use I mean people have written category Theory packages for Mathematica but they are mostly structural it's not like you're doing it's not like traditionally at my understanding at least they're in category theory that you're doing you know non-trivial country computations to figure things out is that a fair statement no sorry crunchy computations that that once you know your statement is once you can write the thing in the formalism once you can write some down in the formalism everything is sort of obvious yes basically that's I think that's the whole purpose of category theory yes okay so I will claim that that right there is telling you that there's a great depth because you know basically you're saying there's there's nothing computationally irreducible that ever gets done in category theory everything is on the surface of things that are essentially structural and that mean yes and even more importantly the more you study category theory the more you see that everything is everything else this is a famous statement in category theory basically in category theory all the categorical tools we develop are amount just to reframe the same stuff under a different point of view and so in the end you say okay I have a set what is a set where it's a set and it's a category and it's also a noun functor and it's also an internal object and say what and that's what is super confusing especially in the beginning that literally everything is everything else you say I don't like I defined limits which are an important category of the concept they say well actually limits are junctions and actually junctions are limits and and people you know they do start freaking out I know that you know if it feels like nothing is ever fixed but the point is that every time you're just developing a new point pretty much everything you already did up to that point okay so so let's let's try to take let's take a couple of examples let's talk about groups for a second so groups have elements they can be defined in terms of you know they have the elements can be represented as products of generators but there are different choices of generators that you can make for a group still maintaining the particular relations you know and with different generators you have different relations but it still the same group as you can determine by looking at how more morphisms between between these groups you know how do I think about that in other words in category theory if I want to have a particular group the group a four or something right if have that particular group is that something that I talk about in category theory or do I only talk about the set of all groups you can do it so there are two main ways to think about groups in category theory the first thing is a group is itself a category and you can see a group as a category with only one object and each morphism is a basically a loop error on this object and each one of these morphism represents a group element and then basically you require that for each one of these arrows there is also an inverse that goes there our way around and that compose what it gives you the identity advice okay naive question why isn't this calligraph a thing that represents that that corresponds what why can't I think of these things as objects these are elements of the group right and these these arrows that correspond to the you know multiplication by generators why can't those be thought of as morphisms multiplication of generators well you have to define composition though well you to defined composition composition as you multiply by this generator then you multiply by this generator and you get from that element to that element yeah but you don't have an arrow between those two elements so you're saying if I and I said yes so if I take that graph and I make the very very messy transitive closure graph there effect yes then what the heck am I doing here I mean this is this is saying so from any element by the structure of the group I can get to any other element because by definition by multiplying by enough generators I can get to any other element can't i yes there should be correct yes right so this is a complete graph here okay although the particular sequence of generators that I need to multiply by to get I mean you know the word problem is is like you know is there a particular sequence of generators yes and that will give you different arrows in that thing right but so so in what sense I mean just to understand is this like is there anything can category theories say anything useful about what I just constructed or is this just a sort of degenerate case of something that one might think about in category theory I don't think in this case I mean on the nose you can say anything particularly useful but again like the point is always coming up with a clever definition usually if you can't say something useful it's because we didn't define the category in the right way it's actually very difficult to come up with meaningful examples on the spot that can you know okay let's let's talk about a case that I you know the curry Howard business because you know we have so for example in in our language we would have something where we can make a proof right so we've got I don't know well let's let's do this let's do a very simple case what's a good example let's pull up a random actually I might have an example here see let's so let's do let's do group Group theory okay so this is this would be the axioms of group theory okay so I've got so I don't know how we think about this categorically but I could say perfectly well you know I could say there's so maybe you can explain to me so that this now would be a representation of a proof in so this is this is a representation of group theory this is a representation of a proof in group theory so okay is there a way of understanding so so one thing I can think about is each one of these of these pieces here well maybe Jonathan who wrote this code well yeah I mean the curry Howard isomorphism in the context of fine equational proof is just stating that every proof has an Associated proof function and every proof function can be interpreted in the proof so if you call fine equational proof that instead of requesting the proof graph you get proof function you get a symbolic piece of Wolfram language code that we can run okay so let's take a look at this I'm trying to understand this okay so there's a proof function so then you can run that what happens if I run it do I just say it should I so true I just apply it to nothing yep that wasn't a very exciting function it's a pretty exciting function because it verifies that that proof was actually correct yeah so but so my point is that my point is the okay direct find equation or proof interpretation of the curry Howard isomorphism is that every symbolic proof has an Associated proof function and that and moreover the more surprising Direction that every symbolic piece of Wolfram language code can it has a interpretation as a proof as a proof object is that the code itself or is it the execution of the code somehow no it's the code itself so you're saying I could imagine something where I mean this is where I get really confused so let's say I write down something like this what is its associated proof object I mean that thing just sits there right so so in that case you can you can treat that as being a proof that that particular can be associated computation halts that's a trivial interpretation of it the evaluation F of G of X Y a comma Z is at that evaluation terminates and that expression that you just output is is the proof of that that is true so if I type in something like this let's say I type 2 to the 2 plus 3 to the 4 okay let me do something in less trivial um / oh I don't know x 1 + 6 x 7 okay so that trace will show me the sequence of operations that took place to get to the result is that relevant to anything should I think of that as I mean is that the is that what you mean by yeah that so those would be you know you could interpret those as being intermediate steps you know each one of those is it can be treated as in the cut again in the language of fine equation or proof each one of those could be treated as the statement of a substitution lemma with the particular symbolic transformation from one to the other being the application of a rewrite operation and so that is a sequence of substitute of substitution lemmers that constitutes the proof that that particular evaluation terminated okay so what is the Curie Howard statement about all of this like I said I mean it in the fabbrizio probably has a more general interpret I mean that there's there all kinds of formulations in terms of dependent type theory and so on but the the direct fine equation of a proof formulation is exactly that that every proof object has an Associated proof function and that every piece of code can be interpreted this as a proof object every piece of code can be interpreted as a proof object so that proof is the proof that so women the every piece of code the proof women every piece of code will have an input and will have an output I say two plus six and it whoops I do it if it was an input cell I could say something like two plus two it will come out as four so are you saying that when you say a piece of code you mean the code two plus two has the sort of proof two plus two is four is that right right right okay so then you're saying in the language of sort of some category theory thing you might be saying two plus two is transformed to four somehow is that right is that Islam is there there's a reason why it's difficult to understand these ways because you are thinking about terms without thinking about types so yeah so thinking in terms of like a typed programming language would be much I think much clearer yes okay so Tali can you give an example I mean I'm not claiming to the particular particular so mine and I think there are different ways of looking at it but my understanding is that if you can cut a compiler run the program then the fact that you're able to do that is sort of like a witness to the types making sense and that corresponds in a way to proof about the types that roughly right guys I'm not an expert but that was my intuition for it well so if you're proving some arbitrary theorem the statement is that the proof of that theorem is equivalent to the statement that the execution of a program yields a result of a particular type in the case of a proof function here that's why why I gave the example of a proof function you can think of this is you know the possible outcomes of a proof function have two types so just be human though then I'll take a true and false let's say that if you want to prevent Ihram okay so you you have you say basically what you have is a statement that says type of hypothesis implies type of thesis and the idea is that basically this implication is telling you daz as soon as you can produce something of type hypothesis then you can produce something of type thesis and curry are saying that these corresponds to a function or a proper functional program that goes from hypothesis to thesis and now i potus's and this is correspond to data structures so yeah but so this is very abstract way of putting it maybe we could say something like you can embed a a sort of proof in a program in a particular way such as if you're able to run the program you'd kind of verified the proof is that correct was that not right well I mean correspondence yeah if you have a program that proves something and that compiles then you can say that that is it proof that we need to understand is that when you are speaking about proving in this context it's kind of a different way from the standard way of proving things that maybe we learn how to prove things in the classical way but the Chi Howard isomorphism really works when you're reasoning in a constructive way so the proving something means to construct a witness of the truth of that statement right exactly you're demonstrating that a particular life is inhabited but in this particular case yes if you if you cut if you interpret true and false is being elementary type recites it with respect to this true function function then the output Li on the outcome of this proof function is exactly demonstrating the particular type in this case true is it is inhabited yes you can add even more complex like a call types yeah right but we're held back by the fact that we don't have you know a natural typographic structure and the Wolfram language something like that the trace functions you its oriented out 204 that's something actually really close to this curry Howard way of thinking because also something is that is really integral to this interpretation the concept of normalization of terms so the computation is really normalization of terms which means that like from a logical standpoint you have terms which are like syntactical expressions and you want to show that two things are equal like that your long statement of the theorem is equal to true for example and the way you do this is to actually construct the proof tree like with some practical rules and these things are actually what we call the normalization of this term right which is which is worth saying is exactly how fine equational proof works internally so so what it's doing is it's taking some arbitrary abstract rewriting system it's applying a kinetics completion procedure to it and then it's just as and then it's applying those completed rules to the left and right hand sides of the input expression you know I didn't finish them until until both sides Terminator to normal form and then it does the trivial kind of test of equivalence between the normal forms so helpful would it be so helpful for me and maybe Stephen here in the same poet it's like just a real simple example that would illustrate this correspondence in action like you know this this function from integers from two an argument of a list of integers and an integer to this other thing like the fact that you can compile and run this and you can find an inhabitant of that type isn't is a exercise of the proof or verification of a proof about something else just like one example would be really helpful because in a way the abstraction is not that interesting to me unless it can kind of like be grounded in an intuitive example why is the proof function example not not a reasonable example in that case well let's have a simpler version of that can we have a really simple version of that so we can just do it you can do like find equational proof a equals C from like a equals B B equals C okay find a presence improves on a lot of yo case of like a equals equals C you have given the list a equals equals B B equals equals C it's the simplex example I can think of and then what I say I want what I want for that is the proof function for that yes what the heck is all that so so ignore the variables those are kind of ugly right so we're starting from axioms 1 & 2 so we have a equals B B equals C and we have a hypothesis a equals C and then we're doing a map hat replace B goes to a can you slow down a bit sorry okay sorry so we have two axioms a equals B B equals C that are represented there there's the first two lines right and we have the hypothesis the thing that we're trying to prove which is a equals C and then to do this is a function of no arguments just just before we get to that yes yeah exactly all proof functions are completely argument free okay and then I mean you you could treat the hypothesis as being an argument if you wanted to but it's just that's not how we represent it can you can you Orient can you Orient how are we supposed to interpret this function like what what are you leading us towards in understanding this particular function so okay so if you if you take the proof object here and you request its data if you could request the proof data set okay okay say there's a data set representation of that proof so get so here you can see we're starting from those two axioms a equals B P equals C trying to prove this hypothesis that a equals C so then there's only one non-trivial step here which is that you have to do I say non-trivial in a generalized sense so to deduce the a equals C you take the input vaccine 2 and at position 1 you apply axiom 1 which cut and then if you expand out that that little proof first even then you can see that the axiom 1 in orientation 1 which means left to right becomes the replacement operation B goes to a because the axiom 1 was B equals equals a and so then you get the output is off applying that transformation you get the output expression a equals equals see the point of the proof function is you don't have to take finding equational proofs word for it if you don't want to you can just you can actually refer you can represent that purely in terms of matpat replace operations and then just run the proof and see that you do indeed get a tautology so let me just frame this in a certain way so what this is trying to prove this is trying to say that you can deduce a equals C just by using these axioms that there exists a purely substitutional way of getting a equals C by just substituting with these axioms you don't have to do any you don't have to know Fermat's Last Theorem never know anything like that all you have to know is structurally how do we place one thing by another yeah mainly yes but in the context of Korea word you are also allowed to do things like taking pairs and other very Elementary constructed kind of things but yeah you are basically so by constructive you mean okay so to my mind what you're doing is you're literal izing pattern variables you know you're taking something which would be a pattern variable a you know a bound variable some in some lambda or something like that or a pattern variable in our world and you're saying you're you're turning you're saying that pattern variable is now equal to such-and-such a particular thing that's one operation you're doing and you're doing the purely so that's sort of a substitution operation now what other operations are you are you allowed to do you're allowed to do all the operations of the lambda calculus basically so like taking pairs of to two objects so if you have X and y you can consider a pairing of x and y by pairing you mean lambda X lambda Y what what do you mean by pairing I mean like forensics comma Y parenthesis yes how do you construct that I mean the data structure like a double or yes making tuples as a data structure yes but but how do you do that with lambdas so are you doing that with lambdas by saying something like this if I write if if again using typed lambda calculus in untyped lambda calculus it would basically be yes what is it what exactly is it so an untyped lambda calculus you would have how do you make okay this is a Mathieu question for nobody else how do you make tuples in the in lambda calculus I don't think you can there are actually many ways to make tuples in lambda calculus one of what is one of them so the basic idea in untyped lambda calculus is you simply use a function that takes an input that they're basically chooses between two different things so the function then count count it's basically the idea of like a conditional so you have something like a conditional and then you feed it in input the input chooses between one of those two things so you can think of that conditional expression and as being a tuple well but so it's not purely structural it actually has to compute something well yeah in lambda calculus right in land college calculus everything is a function so the tuple is a function yes so I go in lambda calculus the only on one type right so obviously like if you if you take tuples the tuples will have to be of that type and so yeah you can create it in in this way but the reason why I say there isn't a real way to do so is because it doesn't even make much sense to consider them i think i plumb the carcass everything as a type and so the idea is that if I have something of type a and something of type B I want to be able to consider a something you know they're pairing as having type a times B but if by everything that's a specific type constructor of making tuples like that right yes how to have that I mean that's for each of the base types you need to have this or each possible couple of types yes you are in a type can you know in type you know construction of Titan the typed lambda calculus you both have the idea that a particular lambda of one type can return a Lander of some other type and you have this idea of making tuples is that right yes that's correct you have any other ideas I mean yeah you also require two basic types which are the unit type which is the type with only one term in it basically it's like true and I think you're also required to have the type false which is the type that is not inhabited - this doesn't have anything when it when you say the type true is inhabited you're saying that that type is just that something exists there is that right is that is that what the the type is just a type that says this is an inhabited type as in something exists of this type is that right yeah that type true as exactly one term that is true that basically means the truth there is no other way to like it it's a type with only one thing in it okay sorry just about your previous question isn't the Cartesian product in lambda calculus isn't it just lambda a B function dot function a B yes can you translate that into orphan language I don't know what the dot what is that what would that be function it just the dot and lambda calculus I mean you mean which is just that I mean the dot is the syntactic form that that you know separates the bound variables from the body right right exactly okay but so so what is that in our case is it is are you saying that the thing would be function of X function of Y what constant but that's a tation of I don't understand this I don't understand that's got two variables but only one body and in lambda calculus that would be lambda lambda a lambda B dot what I mean the point is that the pair doesn't really make sense if you don't give a way to extract the two components of your pair so usually no matter how you find a way to encode a pair that I think it's pretty much suggested and then under the projections and then to access the first of the second term of the pair you use the projections yeah you can't cut the con you just do like lambda pair of lambda a B dot whatever dot whichever one you want you mean you have a explicit function do they work this that wrong I'm pretty sure that's hang on to me but pretty sure that's the Cartesian product it just just to kind of get some flow here I mean I think one of the things I mean we thought we'd figured out a little bit about how our physics models might relate to category theory but I think we're still here worrying about you know getting a framing of what how you guys think about category theory how one should think about category theory um and that some which i think is still charming go ahead can i can i present so this is from someone who's not really like a practice thinking I mean I'm interested in category theory and I learnt a little bit about it but my kind of sense of what the value of category theory is not so much in producing any kind of particular calculational result or sort of like tell you something deepen and interesting about a subject that a very detailed area of mathematics that you really knew well it was rather the kind of like the sort of setting to notice and understand that a lot of the kinds of processes that go on in one area of mathematics are the same kind of person is that gone on how they are it's mathematics if you choose the right abstractions so in other words there's sort of like metaphorical things going on all over different areas of math but when set in the right language are identical and it's not just that they're like each other but there's a very precise sense in which they're the same and every three brings out that latent structure that is there everywhere and so it's a sense and it's in a sense it's an abstraction it's a kind of like effort to bring formalize sort of abstract procedures that are being used in different places and kind of bring them to a create a common language to understand them and think about them and point out in all the different areas where they happen and there might be many ways that you could do that so one is that like you can talk in a way that people will know what you mean you can talk about this abstract procedure like a coda mental something people will know what that is independent of the particular instantiation of that in an area of mathematics so that's one thing that you can do it category very another thing that you can do is that you can be inspired to try new things in a particular area because they're kind of like natural things to try when you've been educated and all the sort of categorical tricks that people use in different areas so it's a kind of tool for thought it's a frame to look at the preneur ease of mathematics to unify certain parts of them to think precisely about structure algebraic structures and other structures and so in that in that sense it's it's like a it's not quite it might not have its own content really all that does that it's really about abstraction for its own sake and it can be valuable all right look I I that's so my understanding I mean you know to give an analogy in the original invention of logic that could be thought of in the same kind of way people had all these different arguments about you know this could be followed from this and so on and so on and so on and then Aristotle and friends invented essentially this form of all these different specific kinds of arguments about you know going to war or eating different foods or something and said all these kinds of arguments fit into this pattern that corresponds to let's say syllogistic logic or something and what you're saying is that say there's a there's an analogous thing that you're doing for forms of argument or structures of construction or mathematics that affair like products like what is a product I mean it's a very general thing and but it turns out like that all kinds of different products that you'd find in different places with its products of six or you know functions vector spaces whatever but actually if you see them in a categorical sense they're all the same always the same yes very particular structure okay I can give you a very simple example how this works like yeah you can be seen to the products of sets of topological spaces of groups of whatever you want and every time you have to define a way to do it but if you want to abstract you know what what is the the real idea behind a product of a product the essence of a product is that if you give me two objects of any sort the product should have first a couple of projection functions so I should be able to go from the products to the two components in some way and the second essence is that if I give you a function to the first component and a function to the second component then there should be exactly one unique way to take these two things and to go to the product which is what we usually do in set theory by saying we define these things component wise so you know we say F product G is defined on X as f of X G of X but in the essence basically is that I can take these things and package them all together into a diagram that I will show you a second just to write it G and by the way that is a that's the universal phenomena that like a lot of the stuff a lot of the kind of like mental work is just looking at our hands and saying this diagram commutes you see this yes so the idea is that if you give me a and B the product should be an a times B thing so that I have these two projections and more importantly every time I give you an F and a G from some C there is exactly a unique way to lift the to the product and we do this by components component-wise in bugs or insects races but this is this thing is packaged categorically in the notion of limit and at that point I'm able to to say I have a unique tool and I am able to say oh actually this very weird construction in this super weird category is exactly the right notion of the product in this context because it satisfies this diver so in this sense now I'm able to link a very complicated thing in some category with a very simple thing like product of sex by saying these are exactly the same thing in these two different contexts alright okay so let's take an example here that that would be in okay they're two different approaches that I can imagine in our world of thinking about physics and so on so I'm sorry but just before you can ons that can I just state a slight disagreement with the idea that I think the category theory is kind of purely bureaucratic from the point of view of our projects there are at least five areas where I think it might actually have significant things like non-trivial things to say about the nature of that's a lot of areas right um okay I mean so the non-bureaucratic aspect of category theory is the mechanics of these diagrams and so on is that correct you do with these diagrams that are I mean what's the non-bureaucratic aspect of carbon on bureaucratic aspect of category theory is that I can define things in a category I can distill it to abstract things and then I can transfer them over to other categories I think that's them the most important thing because imagine that I have a category that us products and the definition of products is plainly awful is something horrendous you would never ever think about your life I would never go looking for this thing and discover that maybe it's valuable in some way if I didn't have this abstract definition of product first so for example Jonathan I mean you know the fact that we are looking for things like black holes and branch filled space yeah where you know it starts off being looking at black holes and physical space but we have a essentially mathematical structure for branch real space that's similar to our one for physical space so the obvious question is what's an event horizon in branch real space those is that well I mean that's there he has a very simple straightforward example of an obvious lifting from the concept of a spacetime causal graph to the concept of a multi-way causal cross but so for instance what one very general thing that I was interested in asking for Rizzio that was that you know the so okay one of one general problem that we have in the we encountered many many times in the in the study of these formalisms is the notion of going between sort of representations and reality so to speak right so if you have if you take a spacetime causal graph you know our can our idea is that it represents some it's a representation it's a skeletonized version of the conformal structure of some other entity and manifold it you know in the idealized case now category theory has developed this whole machinery of the Tanaka crying duality tanake in formalism this sort of which is this generalized way of you know using the enriched DNA dilemma to go from you know representations of an object to the object itself and back again and you know so one question I think is obviously worth posing is is there a possibility that we can make use of a kind of tonight the form to translate between things like the space-time causal graph and Lorenz er manifolds and if we can then as you as you correctly say that will immediately give us insight into what the continuum limits of something like the multi way causal graph would be so so that so the Penrose differentials of topological techniques that he developed first for studying the Red Sea and manifolds that a combinatorial representation of those of that structure is exactly what the causal network is so so pet Penrose is differential topology methods give you the notion of causal precedents chronological precedents on Horace for any space-time event it turns out you know each of those is just a partial order you can construct the diagram for that and you get a network and and super then so then there's in differential topology there's a business or if there's a technique which allows you to go from that combinatorial structure to the actual Lorentzian manifold and back again and so what one obvious question is can we represent that in something a Qian duality and if so can we generalize it to the higher the the right way to do it categorically I think would be that as you said Penrose basically gives you a posit for each manifold and so you are basically I think you get a functor that goes from the category of space times differential manifolds whatever you represent these things to the category of posts what you want is a category that is actually more structure than in category of posts because you want to also include some combinatorial information of some sort you want to make sure that all you care about from your computer point of view is represented in this category in the right way and then what you wanna prove is that you have an adjunctive between the category in which you represent the space times and the category in which these manifolds these this communal structures need and if you have an a junction that basically means that yeah you can go back and forth in in any way you want basically yeah so it's an interesting point it was poly wire about the Junction's earlier so I'm a whether than some of the stuff you've done with with Petri nets right yes this that the fact that you get an injunction between say a Petri net and anis you know symmetric monoidal category that actually haunts you in some ways right that removes some nice categories of the Petri net representation well I mean the problem there is a bit more delicate and it's mainly that a patter net doesn't in a pattern attack transition doesn't really distinguish it the order of inputs you know because transitions are defined as having missing outputs as multi sets so the idea is that if a transition takes took him from a and it took him from me or took him from B and it took em from a is the exact same thing is a graph you can permute the places and nothing happens well in a symmetrical category actually your morphisms distinguish between possible orders of tokens so you know you have to say after it is morphism takes token from me and the token from B and this is different than saying token from be a children's permit in in practice what I'm trying to say is that Packer nets are defined using multi sets which are unordered lists while similar moral categories are defined by using lists strings of things which are ordered and so a lot of people have tried to prove a correspondence between these two things because it really feels like the pet net presents the S&C in some way but because you have this difference that in one case things are not ordered and the other one they are you basically need to do a lot of weird stuff to make it work and by saying by to make it work I mean finding an injunction and the reason yeah this actually harms you when when you look at the practice implementation and stuff but as because you are trying to get an injunction between two things that look like very similar but they are actually not similar enough so that these are Junction does something nice by the way we fix this problem I'm in the process of writing a paper with John Barr as Jade master and Mike Shulman about this so we found the more that a relaxed version of patronage more general version of patronage that as an injunction with symmetric moral categories that works well and it also has a junctions with all the other flavors of Petri Nets that have been considered in the literature so we basically found this missing piece that makes now everything consistent and working in the right way so this poem by the way will I mean I think will publish this thing in a few months but oh cool and so the calories the calories don't have to be strict yes usually again the literature all this stuff the Academy's always strict the reason why they are always strict is because you really don't want to I mean concurrency doesn't you know it doesn't have any order if I say transition tu and the fire at the same time it doesn't make any sense to say U and V fire and then W fires or you know vice versa so in this sense you want fitness to represent currency I think it's probably the only undisputed point at the moment in the whole passionate literature talk about Patrick that sorry Jonathan go yeah I was gonna say this is one of the things that does actually concern me about about this because I'm very enthusiastic about using some kind of tanake and formalism to go from our representations that the actual geometric structure metrical structures that they're supposed to represent one of the things that does concern me is so for instance at a trivial level you know our hypergraph models are they are unordered lists of ordered lists they has they suffer from exactly the problem the old Petri net formalism does and so it does concern me a little bit if we define say in a junction between the hypergraph and some Romanian manifold where they're in exactly the same way as you do in the Petri net case whether you're actually going to be losing some information in doing that and that the you know the the thing we think is the object that it's representing like a Romanian manifold actually isn't quite close enough to the actual object and and I'm so I'm very curious to know kind of what what is that what is the general if you run into a problem of that kind what is the general way of solving it the general way of solving it I don't know if it's general enough but basically one standard trick you can use is encoding the lack of ordering as an action of some sort so you basically say I don't just have a Romanian manifold but I have a Romanian manifold with some action on top of it that somehow permutes stuff and so the idea is that when you link your hypergraph to this thing the action is taking care of you know sorting and doing the bookkeeping about among all the possible orderings without you having to do it the other ways that obviously you can either relax or make more requirements saying like my hypergraphs are actually I progress with something or my manifolds are not exactly Romanian but they are Romanian plus something else these really is the fine-tuning that depends on on your problem but in general you could look at for instance what people have done with nominal sets which is actually I think a similar problem in a way so like you know that in lambda calculus you have alpha equivalents you can always say if I am fresh variable I can rename a variable with this other thing and nothing ever changes the problem is that this is way more difficult to do when you actually do you know formal verification kind of stuff and basically people started thinking about a machinery a type theory that automatically keeps trucking of all these possible substitution business that you can do and so instead of basically saying oh yeah there's a high prevalence but you never explicitly model it in your formalism you actually do it you actually say okay I'm actually considering now not just sets of variables but sets with permutation actions on top of them in a way so that every variable renaming just amounts to you know click press a button apply this option to the set and this thing automatically reverberates to my old theory and everything is consistently taken care of so that that could probably be a solution I don't know your problem in in detail and I'm for sure not expert in differential geometry differential topology and stuff but yes I would say that group actions and actions in general are probably a good way to deal with permuting stuff that you have to keep track of me maybe we could just just for context here talk for a minute about Petri nets okay um and and then I mean because trying to understand correspondence between these different kinds of things because I mean for example in our in our system you know Petri Nets are often thought of as a model of concurrency but obviously we have a you know in our multi way graphs and things we're also dealing with you know what we're dealing with also model of concurrency and I'd like to understand the correspondence between these so for context I mean Petri Nets were originally invented as I understand it as as a kind of mathematical idealization of things like chemical reactions yes so you can have you know various different things coming in and you have you know this type of molecule interacts with this type of molecule to produce this type of molecule all those interactions can happen asynchronously and you're asking the question but you're moving you know a count of this number of you know the a type of molecule the B type of molecule turns into a C type of molecule and so on I mean is is so so then I mean I guess I've always found it difficult to understand me maybe you guys now have a better way to think about what a Petri net actually is but it's always struck me as being this thing that has has too many definitions to sound convincing so to speak it's got too many different different pieces of its structure I mean you know it's not like a you know a finite state machine it's very easy as very easy description of what a finite state machine is a Petri net it's like well you've got these transitions you've got these states you've got these tokens other complication I see your point I spoke with the researcher in Japan a couple of years ago they remember her name and she she was doing research in now da Matta theory and she told me basically what you're telling me now if she really didn't like Petri Nets because the reason would I think she called topological uniformity you have places and transitions there are basically different beasts that you know coexist in in some way while in a final state machine basically everything is topologically the same so you actually can think about transforming state machines as transforming graphs and with patterns is obviously more complicated I think that the main difference what acclimates Petri Nets interesting is that you can see them as a calculus of resources they are really able to like fantastic machine is bit detailed telling you in which state you are in and what you can do in that state while in a pattern at you you actually know how many resources of each type you have so for instance in that page I think it's Wikipedia and one you up there yeah you can interpret this diagram of saying yeah you have a resource of type p12 resources of type P tree and one resource of type P for these can may be P 1 P 3 and T 4 may denote molecules so you can say I have a molecule of water two hydrogen's and whatever and and then these transitions are telling you how all these things are are combined so I may ask a naive question so this is a string rewrite system ok ok and I mean this is a trivial string rewrite system where I'm just replacing B a goes to a B ok thing that occurs to me is if I were to take these string elements if I were to make these strings commutative so these strings are not ordered they just have counts of A's and B's do I actually have a Petri net here that is in other words do I have okay so what we've defined is a thing that says you know in this particular case we're saying B a goes to a B right so we have so I'm trying to understand to what extent are these states there's a question for are these states like the the places in the Petri net and are these events like the transitions in the Petri net I mean in what sense is this difference so this is a string rewrite system let's ask the very basic question how does a string rewrite system differ from a patrick net systems but from a theoretical point of view I think you can identify a family of languages that are parsed by a string revive system right so yes but that's not the most useful thing I mean any language if you have I mean there's a there's a hierarchy of different kinds of string rewritings and if you allow I mean you know if you allow arbitrary string rewrites you can parse any language yes but that's an acceptor that's not what a Petri net is doing is not an acceptor either a Petri net is a transformation not an acceptor I mean language parsing is usually saying there is a set of possible inputs which ones give true they parse some which ones gives well so they don't but you can also phrase Petri Nets in terms of parsed languages and what you will get is something that is more powerful than the language is parsed by finest state machines and less powerful than a Turing machine so if you can parse every language with a string system then it's but we're not thinking of this as a puzzle we're thinking this is a generator much more like a Petri net we're saying you feed in three B's and two A's okay and in this particular case and Jonathan or somebody maybe we can figure out how to do something where it only matters what the number of A's and B's is it's probably an easy way to do that well I mean without having global events I don't think there's a way to do that right you mean sort you you can't know how many A's and B's there are in the whole string unless your event takes up the whole string fair enough but there's there's undoubtedly a way to think about I mean if it isn't a string right system it's something else that can can do this thing with counters basically what why couldn't we have a multi-way system that does exactly what this Petri net thing does we absolutely could it would just be so right now our threshold for an event application is pattern matching but if we also had a threshold that was effectively pattern matching plus a you know plus a minimum number of tokens having been accumulated at a particular region then then you know that that would be fairly straightforward to set up why are we thinking that imagine why isn't it not just this thing I'm just trying to understand because because the difference one big difference between the systems we're dealing with and systems you know a lot of systems people have talked about is in our systems you know we say well there are these string rewrites and so on but we say this happens 10 to the 100 times whereas you know somebody's drawing a Petri net that's representing some you know particular thing that's happening in a block chain somewhere or some such other thing and you say this is a representation where every every node in that diagram means something whereas what we're saying is there might be 10 to the hundred nodes and all they mean is they're different atoms of space so to speak they're not they don't each one doesn't have its own you know life and times if that made any sense well as I think in Petri Nets I mean okay when you use Petri Nets do you use them in bulk like do you have a Petri net with a million entries in it or do you is that not the kind of thing you think about no especially in state books at the moment we are not thinking about them in this way this is what people in chemistry do and and you you get very quickly to what are called stochastic Petri Nets so what you can do is if you're imagining out of that net and you know you have a lot of tokens like millions of tokens and you are not really interested anymore in one precise marking so what you do is that instead of talking about tokens you actually give concentrations to places so you turn real numbers I mean these turn these into real numbers and then basically a patch net will give you some sort of dynamical systems it's just a differential equation I mean it's either an iterative map or a differential equation yes exactly well what we do in in in state books for instance is different because we are actually representing way more deterministic processes so for instance our Peck net may represent the ticketing process that someone has to go through so you know there will be a starting place where there's a token that means nothing happened yet and then there is a transition of these by ticket and then maybe another want to say it's very good and whatever and then the idea is that for each new user you just instantiate a new Petri net which will keep track of the status of the ticket for a user so for instance while working with this ticketing company the idea is that we define a Petra net that represents the lifecycle of one ticket and then if they have to sell it say 50,000 thicker then they literally create 50,000 instances of these spatulas right and each one represents the stage that particular unit is right right I mean it's it's a modern version it's it's one of a variety of kinds of you know systems that you can use to represent these kinds of processes that happen and presumably the importance is you can potentially make proofs on the basis of that Petri net structure yeah the advantage is that at least this company uses our system as a filter so the idea is that if your ticket is in the status used it cannot be resolved for instance and and when I say it cannot be resold is because literally there isn't any transition out of the burnt place so in this sense this gives you a very disciplined way of knowing which actions are possible in each state I get it but let's imagine that you had something like a petri net that represented the post set of all events that happen in the physical history of the universe okay yet which is not the kind of posit because in your post sets and and by the way I want to say that I think conceptually this is very similar to what happened in the creation of our general model for physics okay so I think in your Petri Nets when you think about Petri Nets every place every transition in Petri net has a name that is it's doing something meaningful for you it's a ticket as being shredded or a person is you know getting on the train or whatever else it is right yes it means something okay so similarly for me thinking about symbolic expressions when I write down a symbolic expression I expect that every piece of that symbolic expression means something it's a it's not just an arbitrary F it's an F that way it's even just a thing with name F but it could be a plus it could be a this it could be that it means something right yes so the main feature of this model of physics is that we are using the structure of essentially symbolic expressions but they mean absolutely nothing in other words every piece of you know every element in the expression that represents the universe it's just an atom of space and there might be 10 to the 400 of those and they don't mean anything as such right but nevertheless we've got you know we're thinking about the the same kinds of mathematical structures or post sets where we're saying you know this atom of space has to be created before the Saturn of space those kinds of things but the atoms of space don't have you know it's not the case that one of them is the I don't know the the place where Bob lives and another one is the place where Jim lives or something there they're just arbitrary atoms of space right so in other words and I think I mean the thing that I'm curious about okay so my claim I may be completely incorrect and and and perhaps some both with respect to something like Petri Nets and with respect to category theory actually that the potential use that what what our model is doing is taking the structure of one of these things in a way that is completely devoid of meaning so for example when you write down one of your you know sequences of morphisms and a category right every morphism means something you you know you're not just saying it's an arbitrary structural morphism you're saying this morphism is a mapping from vector spaces to vector spaces that is it's not just you know that they're not disembodied things but good once you have once you have the category then that category can be used as a definition of those morphisms can it not yes like so I think it's actually the same as what we're dealing with right it's the same with Petri Nets right so as long as you know if you know the arcs if you know the places and you know the flow relations then it doesn't actually matter what the individual objects are called what matters is the combinatorial structure of the Petri net I guess but as a practical matter when people are thinking about this the Petri net the fact that they put things like p1 p1 p2 and so on on them shouldn't I know but that's that that's the use case right I mean it's just like if you've said to me just imagine in Wolfram language that you're dealing with expressions that mean absolutely nothing you're just structurally throwing around you know disembodied expressions where every function is the function f there doesn't do anything right ok I would have said what use is that it's never gonna be useful for anything right it's because it's just it's but yet that's the basis for our model of physics in other words it might not be when we think about so I'm just trying to get the mindset of thinking about things like category theory as a as a purely structural thing so you're talking about category theory as a way to understand the correspondence between you know something in differential topology and something in you know I think probably one thing we could try to dive into a bit is the great Andy construction is not the easiest thing ever but it's exactly a way to basically take some semantic information and making it purely syntactic so basically you start with things about meaning and somehow you compile and bad these meaning to something into something which is actually purely combinatorial so this may be interesting maybe let's try it let me just try a couple of other things just and then we can perhaps dive into that I mean so so one of the things that we had thought about a little bit is okay let's just go through a few things so this multi-way graph let me just let me just comment on a few bits and pieces here so so this we just draw it yeah obviously totally trivial point but there's a one-to-one correspondence between execution semantics for a Petri net and event selection functions for a multi-way system okay that's interesting right because Petri net by definition is highly trivial point by definition are just not the non-deterministic right because you can have multiple transitions that fire yes right but but in practice people to find execution semantics to prevent the non determinism which is exactly what we do like the collection functions in multi way systems so so okay so 4-bit CEO Matteo just to make sure we understand what a multi-way system is because that's going to be without that we're gonna be lost okay so a multi-way system just says where we have some transformation in this particular case is just a string rewrite transformation Diego's baby okay and all this is saying is you apply that transformation wherever you can okay okay so we can think of this so for example this is a you can also think of this as a proof this is the proof that BBB AAA is equivalent to a a BBB with the rule that ba is equivalent a B there's a proof and the proof we can say a particular proof would be some path through here that leads from the input to the output yes right and so so this is so that's our multi way system and in our world I mean we can talk about how this relates to quantum mechanics and who knows what else but this is this is a structural object in in our world okay and and so what you know one question would be okay so that's one thing next level is the evolution events graph so this is saying this is dual so well this is what this is doing is it's saying for every one of these transitions from this state to this state that happens by virtue of an event that event says this is the BA that we're rewriting as a B in this case there are two bas that we could rewrite as a be there in different places they lead to different outputs sometimes there will be a merging of those outputs and so on okay right so this particular case this is a confluent rewrite system so even though there are many branches we always converge yeah they always convert but that's not always the case that's correct yeah that's correct it's it might be the case in physics it is quite significant if it's the case in physics but um I mean it happens to lead to special relativity and it leads to you know quantum objectivity and all kinds of other important things in physics but that that that's irrelevant to this so the first thing that one might think of is insofar as this picture here could be thought of as related to an actual you know diagram of morphisms and a category i mean that is we can think of these states presumably as a category and we could think about these transitions between states as morphisms in that case yes that's that's correct that that's it's very possible and at the moment if your system is one your cattle will be a poset which means that there is at most one morphism between any two states but obviously if you have more than one way to go from one state to the other and you don't want to let's say identify them then you just have a category okay and the notions like confluence and causal invariants can be interpreted in terms of statements about the existence of coke owns for associated codes things like this and categories yes yeah right I mean the statement of global complements is effectively a statement that for every cone there is an Associated code code what is a cone in the categories that a light cone or is it something completely utterly no no it's something completely different are you sure it's different yes yes I mean I don't see an immediate correspondence between light cones and this kind of stuff my nightmare what is I also think that they're different how do you see cones in in this case they would are the cones in the cocoa ensign well so if you have so four instigate whichi this is this is kind of a bad example in this and I'll see if I can construct one in just a moment I can't I can't speak and do a construction at the same time okay but so yeah my understanding of a cone is you know you have some object N and then you have and you have some family of morphisms that leader yes it's literally a now you have a diagram here in your category and you have another object in the category with a lot of morphism to go to each thing in exactly and so my understanding is a co cone is it's the dual notion of that if you reversal the arrows you get a co code right so yes anytime you get a bifurcation in one of our multi wear systems I think you can represent that in terms of the existence of a cone right because the the predecessor element is the common elements for which to for which you are applying a family of morphisms and then as long as there exists an Associated Co cone then you're saying that eventually that bifurcation will eventually reconverge and what is the difference between that and our friendly entanglement cones isn't it exactly the same thing it's certainly related it's certainly related the main distinction being with an entanglement cone just like with a light cone you have to kick and orientate you have to effectively pick a foliation right you have to pick a direction in which to orient it whereas the where's the category theoretic notion of a cone is in this context is purely combinatorial so it should be so yes you're just going a certain number of morphisms down so where you're going one morphism down the problem in these examples is that I mean I understand you can say every time I have a bifurcation I can represent this as a cone but I don't know if then these cones will compose in the way you want and in particular is difficult for me to see they is like your base category changes all the time you say that what was the base category here not the category of strings well it can be but then like what are the morphisms between strings and how what means it's this function it's this thing that says yeah but Dad I understand but and I don't understand why some other thing has to be taken to be the tip of the cone like I don't really understand how you distinguish cones in this setting question so maybe we shouldn't go to cones but if if I ask the question for this graph right in order to make this a valid category theoretic is it the case that I have to do the transitive closure to make this be a valid category theoretic diagram again it really depends on what you want to capture in this case I feels to me that each arrow in this graph represents just composing with a morphism so actually you don't want to J to drastic closure you want to consider all the possible paths on this graph okay but it won't be the case that the associativity that you normally have in category theory does it apply in this case or not to the most oh yes yes yes why not yes I think right if you if you say instead of it an evolution edge representing a single application of an updating event it represents an update sequence so in other words if you take the reflexive transitive closure of the of the option relation that then you end up with that you end up with a category so so women yours in my relativity paper okay so women walk me through that so you're saying you're saying oh yeah so if you say if you take the reflexive if sorry if you take the if you take the the the symmetric closure of whatever it is the union of the rewrite relation and the identity relation then so effectively if each edge is saying it not just that this it can be directly written to the state but the state can be rewritten to this state by some finite potential e zero rewrite sequence but but isn't that this picture here yes that's the transitive closure picture yeah well I mean I put plus self loops right because you're allowing for rewrite rewrite sequences of length 0 fine okay but so what I was asking I'm not disagreeing yeah ok fine so this is the thing that will be sort of the category theoretic way of representing with the morphism being rewrite above the strings the category of strings and then this would be the representation of that category with its morphisms in category theory is that a fair statement yeah that's what I'm trying to really understand like I understand what you're saying I'm just not sure that this is the most insightful way of category fiying this notion yes that's right so let me just go on because I think there's something potentially interesting that happens so here we've got the dual of this effectively what we're looking at is these these events that correspond to each edge each morphism basically here is being turned into what we're now asking so now we can ask for so if I make the let's see the causal graph though let's see what do I want an evolution causal graph so this will make this rather complex gosh this rather complicated thing and my claim would be this is the higher order category version of that previous category because what's happening here is the morphisms of the previous category are being they get morphisms of their own that map onto other morphisms in that previous category so in other words these causal edges which represent the causal dependence of one event one update event on another I would claim may be wrongly that that's that corresponds to a second-order category from yes called the two category it may be but there are quite a lot of loss we have to check to make sure this is the case that so yeah I mean to achieve Li what you say seems absolutely possible but the verb to check okay so but I want to understand what we get for having those axioms be true so to speak but but also just to understand this in the case of if I thought of this as a proof for example here I you know it's a proof that BBB AAA is equal to AAA BBB right okay then then I can imagine a higher order so the correspondence between proofs between would be a two category that correct yes you may say that you you can say that as two morphism so an i or order morphism between morphisms expresses some kind of relationship between two proofs right like you could say that for instance you have a morphism if one proof is a river of another proof for instance or something sooner right so I mean for us actually that makes me think about Jonathan that makes me think about rural space and the translations in rural space between different between for example different Turing machine paths that for that is is like the rewriting of one proof into another proof I'm not sure if that's correct but but I'm trying to understand so then well any of these things can be interpreted that way it does matter whether it's branching or rule it's just that it once in the rule your case you're allowed an infinite parametric family of axioms as opposed to a countable set of axiom okay finite set vaccine but but then physically the two category is corresponding to causal edges and presumably we I think we talked about this before the three category would correspond to taking these causal edges and asking for a relation between causal edges and that corresponds to a foliation of the space so it seems like in our models what's happening is the raw evolution of states is like a one category situation the causal graphs are like a two category situation the foliation ZAR like a three category situation I think maybe and so then I'm obviously going to ask the question the analog of the infinity category what what might that represent I mean how can I think about for example in the case of proofs what is the analog so if I say there's a you know there is a this is a collection of proofs there's now a mapping from one proof to another then I can imagine a mapping between mappings between proofs yes how how do I think about that that infinite hierarchy of things well this is what they do in amo topic type theory basically the idea is that you can think about the proof as a term of a given of an equality type so if I give you a type equals be the terms of this type are proofs that a equals B okay and then you can say morphisms between proofs are proofs that these proofs are equal because for instance yes what I what I'm trying to say is that you know for in a computer in a dear improver you can prove that a equals B by rewriting some things and obviously you can give two different proofs there are two different rewriting orders and most often they're not if you're working like or a trace your compiler will be too stupid to understand that these two truths are proving the same thing like you know they were treated as different and so if at some point you have to prove that these two proof objects are the same then you have to do another rewriting between proofs and you see that you can iterate these up to infinity so you can have proof between proofs proofs between proofs between proofs and and that's why you need an infinity category because right but so so what's the I mean for us here each path through this graph is a proof and so the the statement the the proof of the equivalence of proofs is a statement that you can make a transformation between one of these graphs another but I'm trying to get an intuition for the Infinity category what what does it mean so the proof of you know for us again the one category is actual time evolution the two category is causal connections between pieces of time evolution the three category is the construction of reference frames the construction of affiliation so I'm trying to get an intuition if we went beyond that to the four category five category up to infinity what is that corresponding to what is that what is the potential interpretation it's I think it's the weakest version category fication you can you can you can use because what you what you are having is when you create is a category which is very very granular and it basically allows you to consider every different way of transforming different things as distinct by keeping track of what is equivalent to what without doing any identification so this is what an infinity cut every does usually you you know like you you can basically view for instance one category as a two category where all the two morphisms have been trivialized either you know you identify everything that is a two isomorphic and and then you can say well actually two category is an example of three category where we have identified three morphisms that you can go the way up so basically I mean I am NOT an expert in infinity category theory but what I know is that the reason why they are becoming so relevant now in automated tier improver with your improving is because theorem provers are too dumb to understand if two things are equal unless they are either syntactically equal or you give the prover a way to transform to rewrite one into the other and so that's why you basically want to create work with the type theory that is as weak as possible and allows you to you know keep track of all these equivalences somehow automatically can I give a more topological interpretation of that idea so so the basic concept is if you if you regard your type as a topological space and you regard the terms in that type as being as being points in that space then each proof is effectively a path in that space right it's the part mapping one what one point onto another and then and then as Fabrizio says that then equivalences between proofs are then Hamas appears between those paths right but the idea in homotopy type theory is is to is to go up you know all these different levels of abstraction but of equivalence is between these Hamas appease to construct through an infinity group wide construction this thing called the homotopy type in which there is only one kind of equivalence that we come out of the equivalence and then that Natura because of the nature of we come out to be equivalence that induces all of the lower order equivalence relations right the way down right so all you have to do is one one kind of equivalence checking in this homotopy space generated by the Infinity groupoid and then you're done and then all of the other layers of the hierarchy are already accountable that that's that that's the basic idea that's why that's why hot is as fierce as it is so relevant to kind of to modern ok let me try to understand a little better ok so in our case we have a you know this is our simple model for your you know this is pause in space now I can imagine I'm still a little confused here there's a homotopy we can ask are we asking between these two different paths explain explain the Hama topic statement there yeah so then you you say that those proofs are genuinely equivalent proofs if there exists a homotopy between them and what how we define a hama toppy in this case well so you obviously have to you have to induce some topology and have some notion of continuity but you know basically an elementary notion of homotopy in this in this instance would just be a direct mapping of States onto States edges onto edges that would allow you to transform one path into another what you're saying in that in the continuum limit of the multi-way graph you're saying there should be a genuine homotopy yes if that is that continuum limit exists then there should be a genuine so if you if you genuinely took the you know the the space of the topological space of some particular type the topological space effectively oval of all proofs then yeah then it would be a bonafide homotopy ok but so for us we get to actually have a concrete version of what the topological space of all proofs look like yes absolutely it's the limit which we don't yet understand it's the continuum limit of the multi way graph right so I can so for example with this multi way graph I can make a very very big one and maybe I can think about that as being continuum limit so then your Hama tapas statement is what they're because it's not obvious to me why how you set up topology on I mean you're saying okay can I can I put it in a slightly in a way that's more directly ATP related yeah so right now if you call find equational proof it works with theorem hypotheses and axioms that are pure equivalences between symbolic expressions right but the proof object that you get out is itself a symbolic expression so it could be that we could also call find equational proof with hypotheses and axioms that we're equivalences between proof objects it happens that we don't currently support that although I thought a bit about how you might do it and what you could get out and one thing that I'm interested in potentially implementing would be then you could have a rewrite secret because each step in it in standard proof objects just between you know zero order symbolic expressions is just a rewrite relation and a position yeah but then you can you can then apply a rewrite relation to that rewrite relation right that rewrite later relation has two paths that has a left and a right and then it has sub expressions within the left and right now you can apply rewrite rules to that and so then you could get a proof of equivalence between pre to proof objects subject to certain axioms of equivalences between proof objects and and so on so then it so then you could construct some higher-order generalization of fine equation or proof and each one of those higher-order pieces can be thought of as being a homotopy between proofs in the lower order okay so let's just think about that for a second so I mean one thing is we are inadequately category fight in some sense in the sense that our programs equals data and not is not quite good enough because our proof objects have a rather different structure from the objects about which we are making proofs right now I mean in other words if we look at a proof object here you know this is a this is a thing which is qualitatively similar but it isn't exactly the same doesn't have exactly the same structure as the actual things that we're making proofs about but let's assume so in this case with this proof could we make what is the proof object the proof object is a path here right yes right right so you're saying that what we're doing is we're saying the original object is a string the proof object is a path we're now asking for correspondences between paths correct right so you can subtract the most deformations of these parts what are what a continuous deformations of these parts mean without a continuum limit we don't have a good notion of continuous them yeah I don't think it makes sense I mean continuous deformation is somehow implying that this thing leaves in some kind of continuous space nice go ahead no I'm just I'm saying like maybe we can attach a topology to this just from there the rules the most meaningful kind of topology you could have touch to this thing is called great and ecology I think where you said Griffin dike what did you say he's a he's a big figure in this whole infinity carrier anything else well as soon as you hear a particular name you know you're going into deep abstraction and gross and because one of those names were where you know what very fascinating ideas but typically very abstract so what what he did is he basically took the axioms of topology so you know finite intersection arbitrary unions and category fight them which basically means that now you can endow a category with a topology called the great anecdote Rapala G in a way so that if would you started from it's just a topological space and you're you have a way to create a Britannic topology that coincides with the one you started from but in this case this is I think particularly relevant because these graphs can be seen as process and so as soon as you start considering the category of paths over these graphs then this thing gives you a nice toolkit to think about topologies over twisting okay I want to understand growth finding topologies this may be a tall order this may be difficult but I want to understand what how's it work so the first thing you have to understand is the concept of seed the idea of a sieve is that you pick one vertex in your graph whatever you want so is this a graph that I could use this might be a and we can use this one no problem if you pick like one one random pick that vertex perfect okay so a sieve is a set of arrows into that vertex which is I'm gonna pick this vertex instead just to give me some more arrows okay no it's into is not from so if you pick that one or less arrows that are going in there all right looking fine okay so you take this one and basically the idea is that every set of arrows that are closed by pre composition for a C so for instance you can generate a sieve by taking the arrow that goes upwards the first one that goes from ba-ba-baby to be baat let's say if you if you go back to the selected vertex which one this vertex here so if you take that vertex here there is only one possible seat on the first vertex which is the empty one because you don't have any arrow going in now if we take the the one two three four the fourth one vertically from the first one one no no okay if you think okay let's pick the one in that case you are enough to increase the size even more let's let's increase one more step the problem is if we increased too much more we want able to see much of a graph okay there we go so if you take B be a be a lumen is the second one okay this one has it up is it no it's the second one from the top this one here oh I think okay yes oh you may have a delay for the mouse yes exactly that's so B ba ba you can have only two possible sieves there the first one is the empty one so you could do not consider any arrow and the second one is the one that goes from BBB AAA to B ba ba okay and now if you go to be a be a B you see that the situation is a bit more various because you can have the empty sieve but then you have two different arrows going into that vertex so you can either consider the sieve that goes from that is generated by the arrow that goes from ba b ba - ba ba ba yup and again if you take desire you have to also take the desire composed with the other one that goes in to be a be BA and the one this one also has to be composed with a BBA a so this downward closed okay so in it so all we're doing here is we're taking the we're going backwards up the arrows the yes precisely what you can do is you take basically you say a sieve is just a set of arrows which is closed with respect to these going backwards kind of thing okay with it you're saying a sieve as an S ieve or something yes see the cursor yes okay in graph theory isn't that just what that does that for us vertex in component nape vertex and components exactly yep right so so this right okay so you're saying it's the vertex the infinite vertex in component of the particular node is the sieve of that node is that correct you can have many seeds because again for instance in the case of bada be I can start by considering only one of these two arrows that go in or none of them at all or both of them right but so what we're saying is there's a vertex in component for B a B a B and we could say for example the one level vertex in component is just that those are the things that will lead into that's the zero if vertex in component the thing itself that's the one that is that pretty image there so to speak in that pre image if I go to the two level vertex in component I'll get that state there I can go to the three level 1 and so on but you're thinking in terms of vertex is now well you should rethink in terms of edges the CV is a set of edges okay fine okay all right so we've got those edges we can we can generate those I'm not quite sure exactly how to do that that's probably the you know the interesting thing is that again many different sieves that you can put on the same thing because after you specify basically a bunch of arrows you have to do the infant-like downward composition with all the other arrows that you have but for instance if I say okay what is the sieve generated on VA EAP by the empty set then this is the empty seat because you know you just don't have any arrows to start with so you don't have to do any sort of composition if you only start with the arrow that goes that starts in Bab ba then you will be up to take care of that sort of fat okay we've got a construction for the sieve now what do we do with the sieve now the point is that this thing can be used to and symmetrize the equivalent of an open covering of a topological space an open covering of topological spaces is just you know a bunch of open sets so that their union covers the entire space topological space and in this case the idea is that for each vertex you want to choose a sieve and you want to do it in a way so that there is some compatibility conditions between different sieves that are listed in the graphic topology page and basically what these gives is abstract axiomatization of open covering which does not need you know to talk about topological spaces and this thing really formally behaves like an open covering in topology so this thing basically allows you to to use a lot of geometric machinery even on spaces that are actually discrete like this one and and then you know after you have a notion of open covering you will automatically if you if you deep dive into this stuff you will obtain an appropriate notion of amo topic equivalence for instance so you may obtain an appropriate notion of continuous function and continuous deformation so the idea is that since this thing doesn't really look naively as a topological space these is the like most abstract way to put a topology on it and that would be the thing I would start from also because may ask a question yes is there some freedom and how you how you attach this topology yes is it sort of like so so we do have some choice here but we could make a topology that somehow compatible with the rules that generated that that's exactly what you want to do that's exactly what you want yes so you can see that there are for instance two they'd say trivial choices of topologies that you can take here the first one is for each vertex you take the biggest sieve you can see just consider literally all the arrows going in that vertex you do this for over X over Texas and the other obvious choice is the to take the empty sieve for each vertex and these two things should both give you two examples of critique topologies but yet there are a lot of possible choices in the middle which yes you should actually tell you in a way that is compatible with your competition rules because in that case then you are obtaining some geometric representation of what you're doing computationally and that is how would we do this this sounds very interesting but what do we actually do here so we're trying to make open sets we're trying to make something which is some kind of growth in D key and analog of an open set yes okay how do we do it like this on impromptu I am not sure I can answer this idea I think it's relevant here to understand that a see if it's a set of ways to get to the specific node of the graph you're considering so in I guess in your model it might be interesting to look at C's as a the causal paths that you can have attached to a surgeon no because that's there's more information there than it's represented in this graph right so they're like exact Euler intricate causal structures being lost here but maybe that's the right source and so so geometrically the way to interpret this is that my right in saying that each each such choice of sort of open subsets to consider part of your sieve corresponds to a different choice of open immersions of this of that open set Joseph of immersions I'm trying to get a geometrical intuition for white how we think about this freedom to choose which family of open subsets to consider part of the sieve is that some freedom of choice of immersion locally around that such that so yeah basically in the topological case in which sieves actually end up corresponding critical topologies and that corresponding to open coverings basically your notes would be the open sets of some topology and hours would be inclusions right right exactly so then the freedom to choose your sieve is exactly the statement that there are there are many different possible sets of open immersions for those opens exactly so yeah maybe I said yeah you're pretty much what we expected I think yes so you're basically saying okay given this open set I'm considering this set of opens that somehow embed into this thing in different ways yes and then you see that since you're free to open said you are considering a lot of other open sets that embed into it you want to do it in a compatible way because you are going to do this or each show pan set so you want to be sure that these inclusions they all behave well with respect to each other basically so I don't like you can I mean I think the most intuitive the notion of topology here is actually in the notion of coverage which is just a choice of arrows we you were to meet as your past arrows okay no no and then you can generate everything to genesis and then you get a proper topology but like when you specify a co-vary for an open set you specify it like a family of stats covering but like true notion of sivir corresponding to that should be only the open sets you choose but also their subsets right I think you get freely you know you just specify the big ones and you say those are the ones I need the chunks of the space that I want to consider separately and you know whatever is inside the chunk gets that's a long and same for the compatibility you add them freely exactly so with the evolution causal graph all of these all of these property I think are satisfied recursively because each of these each each possible choice of open immersion effectively corresponds to a different choice of updating order or a different choice of a space-like hypersurface foliation and so as long as that is consistent with the causal partial order then we know that that is also a valid open immersion for all of the oaken subsets and so then that gives us a valid rock critic topology hold on that's not what I mean let me try to understand that okay so you're saying we look at the evolution causal graph right right so my point is simply you know so to the extent that I understand it each choice of sieve which is a you know a choice of oak immersion around for some open set is really just a choice of updating order in the context of a multi-way system right because it's a it's a choice of a collection of incoming arrows there should be correct yes right so and we have a way of parameterizing that in terms of you know in terms of collections of space like separated updating events that that satisfy the causal partial order so the condition that these things they play nicely with each other is the condition that it's that they're compatible with the causal partial order and then if they're compatible with the cause of partial order then we also know that in order to get to that point they had to been compatible with the previous causal edges and so not only do we get the the validity of the open subsets in that sieve we also get the validity of the emotion of the open subsets in those open subsets and so on so all we need to know is the evolution causal graph I think though you're claiming that these different choices of open sets are different are effectively different foliation of our of our system well that's where I was why I was asking about that was exactly why I asked about immersions because I think that's that's the correct way to think about so you think that the choice of open sets just so I understand so you think the choice of open sets is basically exactly equivalent to the choice of foliation x' make the a slit cord is with another way of looking at this because gratin guilt apologies are actually and instead of our even more general notion of topology with a low V attorney topology right and that's more logical in its interpretation because a low V attorney topology is defined as a kind of a modal operator on the logic order to this but the point is that you can consider choosing these open sets as a way to choose in which way you can assess the truth of a statement in that point all right so I guess that it's really supporting the affiliation interpretations is I mean I can get to this point in many ways but as a server there I have this set of things that I look at that if I want to assess the truthful statement here exactly exactly kind of doing that so the most money my question is my point is the cell this type of I didn't get what they spell this type of Capone say the Latvia TN e is that how yeah of your journey yeah both how la WEA re I will be re TI er any why I think but if there's a there's a - there's no K okay I vote yes yeah but I'm just trying to decode tourney or something is that right yes okay and so that this is a explain what this is again I mean this is the fine in the context of tapas theory which is like a really big subject to catch now that anyway in any category as a notion of logic which is internal to the category it's like a language I can associate to a category to speak about the objects of the alright and stupid example if your category has a product then logically these means that in your category you have a notion of taking pairs of things yes or for example the closer structure we were talking about yeah which was the hair oh that's something you can use in your logic internal logic to make function types okay right there was a pretty big Johnson can you explain yes right right so so whereas before you know okay in the context of what we were discussing earlier right we had we were discussing these notions of like a type theoretic interpretation of true and false right yeah there's a brilliant idea that you know this type true which has a single element you have a type false which has no elements and then and then you can say a statement is true or false depending on whether the type true or false is inhabited for that statement right the notion of a lower tierney topology again to the extent that I understand it is that it gives you a way of generalizing that idea so you can speak of local truth right so you can say that you can say that a type that the truth truth type is locally inhabited with respect to the top loss even if it isn't globally inhabited so in the context of like I'm out to be type theory that allows you to say that certain theorems are are kind of correct locally within the region of that of that of that term but not the main be globally true exactly and the one way to see this is that basically you are it's not really the proper from a word but enriching your crude values so instead of for instance you say a logical formula in set is something that goes you know to zero one so you can say you have an evaluation function that takes a formula and maps it to zero or to one if the formula is true or false and instead what you have in this case is that your topology of the underlying space will give you the structure of the truth values in your category so you don't have any more true or false but you are true at give them a kind of it's give a homotopy type theory find equational proof interpretation of that you know so if you consider if you consider the topological space that corresponds to you know in homotopy type theory to the type that is you know all all all theorems that you can prove using fine equation or proof right you can pick a particular term that corresponds say to the statement of commutativity and you can say that that associated proposition is true locally if by locally you mean kind of in the context of like abelian group theory or something even though it isn't true globally in this in the context of you know none of these intuitively and in principle true but you are treading a very difficult field because you are basically considering at the same time an infinitely category and a top of structure where a tapas is basically the kind of place where you know you can talk about this internal logic or take the right way the problem is that the Infinity promises are not exactly the simplest thing ever actually this is the actual frontier I think of algebraic geometry P I think people have figured out stuff probably up to infinity to top assist but in general these are very complicated and I think there are some sort of conjectures that basically postulates or proved that the internal logic of an infinity tapas is actually a motivic theory or some flavor of a theory but this is this is for sure something I'm not versed in but it's also something that is still very being like researched on I there's definitely approved correspondence between I think I must be typed theory and Olivia technique topologies for some very restricted case I I forget it was listening like pre sheaf top or something but I definitely seem seen results in that area but I want to come back to this corresponds between open sets and foliation z-- okay what do we learn for the correspondence what's that maybe even a limited then what's the corresponding open sets you're saying a whole thing sounded like something really yeah so an open set would obviously just be a vertex and then the open immersion would be the collection of updating events that led to that vertex over the collection of causal edges between updating events that led to that vertex but what kind of vertex here state vertex is an open set I think you can treat it as one yes so the idea is that formally you you see it as an open set so Justin - okay let me let me just digress for a second are you familiar with the idea of pointless topology I don't think I am I think I understood got as far as point-set topology but no yeah so that's basically imagine this we know that topological if you take the set of open sets of a topological space they form a complete distributive lattice you know you can take arbitrary unions finite intersections so at some point someone said well but I mean the interesting topological properties actually come from factor of the human says and no one really cares about the points so why don't we instead study complete distributive lattices and try to generalize topological statements to properties of these lattices and that's more or less what we are doing here this is not anymore a topology in that strictly geometric sense but the idea is thanks to the grid in the topology we can imagine that these state vertexes are our open sets even if they don't have any actual semantic meaning does anything to do with geometry you know and but sorry Steven can I just mention one thing which is that you you actually do know about this because we discussed it in the context of the multi way continuum limit and projective Hilbert spaces right you remember when you found this this notion of continuous geometry that you know that there's von Neumann construction of the projective like a projective Hilbert space purely in terms of a modular lattice and this is exactly that idea right so the sense in which you have a correspondence between a modular lattice and a projective Hilbert space is exactly the sense that forbid Co said the combinatorial structure of the modular lattice tells you about the relationships between the subsets of the Hilbert space without actually having to tell you about the individual vectors in their Hubbert's days ok ok so wait a minute so this is you're saying you can map out I mean when you're talking about sets it's a sort of a discrete almost combinatorial thing and you're saying you can talk about relationships between sets without ever thinking about the underlying so I mean what's interesting about that and maybe that's what you were basically saying is what we have in our systems is that description of the relationship between what you're describing is being like open sets and so then the question is does that sit on top of some continuum thing I mean that you're saying there could be a continuum thing of which our system is the open set description so to speak yes exactly so what I'm saying is yes is is there sufficient the generalized notion of topology for which these things behave like they were the open sets and we have a notion I mean after you have a topology then you can define the notion of continued mapping continuum function continuous function over these topological space okay so what what is for us given this idea that the open sets are the nodes of this graph what is the notion of continuity then well the point is thinking about open sets strictly is a bit misleading because what the great Annique topology does for you is that it states things in terms of open coverings so all these choice of sieves and stuff gives you the equivalent of an open covering for a bunch of space so the first thing to do would be less describe continuous functions in terms of open coverings and not in terms of open sets that would be the first step I'm sure this is a function on this multi-way graph a function means you assign a value for example to every node in the multi-layer graph yes we way are mapping these these vertices to something basic right so we assign a value to every vertex yeah so then a continuous function might be well what would be an example of how we might define a continuous function if we're doing that what is a continuous function then use the definition which says that the continuous function pulls back open sets to open sets that's actually nice yes so if you have two of these graphs like the one I'm seeing right now on the screen and you have a mapping sending vertices of one to another one and if we think of the vertices s open sets that you want to pull back well actually here the correct notion of open sets would be not a single vertex but the whole set of vertices and edges going and arriving to the set she's there for closure of that vertex right this D is the continuing motivation arrangement sorry the motivation we started with was to try to think of of Mata P in this context so it was like what are continuous deformations of paths look like alright are we at a point where we can think about that or because because that's something of genuine I think it was like a super interesting like what you know what what what two paths are close to eternal and which paths are close to each other which aren't can we answer that question actually I want to make my suggestion here so we've got this idea of branch hill graphs which is a way of deciding which that's a way of deciding which nodes are close to which nodes we could imagine a similar kind of thing that is asking for the paths which path is close to which other paths in the same kind of construction so a branch of golf is constructed by taking the each I mean like I could could take the branch hill graph here by saying which which nodes here are related by being the successors of a common ancestor okay so I would say that the the analogous thing would be if you want to know which paths are nearby we could imagine doing the same thing for pods we could imagine making a branch hill graph with respect to pause and we keep on talking about that Jonathan do you have any comments on is that is that obviously silly I mean in other words we can get a map let me let me take an example that's more interesting than this one what's what's a good example let's see um just just try to get an example of something which would turn into a reasonable branch he'll cough hold on one second I'll pick one up but no I mean I I agree that that's obviously something that's worth constructing because yeah I mean once you have the interpretation I mean that the topological interpretation of a path some parameter as effectively a parameterised family of vertex in components and then you're asking whether those you know whether the open sets on one on once in one such family map on to open sets and the other such family then yep and then you definitely have a notion of being able to define you know path distance so let's talk about that I think this is very interesting okay so let's just explain to folks here what the branch field graph is because it's relevant okay so this is let me this is a multi way system let's see what's let's just draw this multi way system it's kind of silly complicated thing here so we've got a multi-way system this is a very trivial multi way system let's say four steps and let's draw the state's graph here okay so this state's graph now I have to make it wider sorry do that so let's look at the state's graph this is saying um these two states here or let's take these two states here right have a common ancestor here right so that that means so our rule for making a brow gel Graf is join two states in the branch of graph if they have an immediate common ancestor okay so those two states have a common ancestor let's say these two states have a common ancestor these two states have a common ancestor so now let's make the branch shell graph let's make the the one two three four three-step branch shell graph okay so that three branch of golf should be a map basically this level of the multi-way graph okay it's saying how do these states relate to each other those two states they're quadruple a triple B quadruple a triple B relates to triple a b a b b by being joined to that because they have a common ancestor that makes sense mm-hmm okay so this is a way of so now what you guys are saying so there's a way of relating States by looking at their common ancestry now what you effectively seem to be talking about is is there similarly a way to relate cards here to each other right so that's the Homma topic question would be is there what is which path so in this picture we are saying what's the distance between this thing triple that thing and that thing we say it's branch real distance to okay so in quantum mechanics the interpretation of this is this is the map of entanglements between States and this is telling us that the entanglement distance between these two states is two in this case okay so that's the interpret which is gonna cause approximation to the ADN gauge distance okay that was what I was about to ask is what's the physical interpretation okay so let me let me understand what you're saying so the ADM gauge each such path is a choice is a choice of foliation which we can parameterize in ADM right is it a choice of foliation is is that is that enough is it is it big enough to be a each such choice of path limit isn't a foliation of family oh I see each path and the multi way graph is a particular foliation yes you can represent as a particular foliation so then you're asking what is effectively the distance between two foliation z' and so my conjecture is that what you're going to end up with is a course approximation to the to the gauge distance that is the total laps distance and the total shifts distance between those two choices of gauge how do you measure in the IDM formalism how do you measure the distance between okay so a choice of gauge well that mean that's that's what the ADM formulas in it or that's what okay to be more precise that's what my discrete generalization the alien formalism does it tells you you know you have a hypersurface the way you can parametrize how you get to the next type of surface is for it every point on that hyper surface you say what's the time like distance between that point in its corresponding point hey what's the number of causal edges you have to traverse and then what's the space like distance ie what's the combinatorial hypergraph distance between the place where that updating event got applied in the place where the next updating event got applied and so as long as you can find those two quantities for every for every event that completely determines to the foliation of the causal network so then if you're given two foliation x' you can ask about what's the what's the total lapse distance and shift distance i the total time like distance and the total spatial distance in a constructed say as a volume average over that over that entire causal network and that gives you effectively a wave that gives you a metric on the space of possible gauges and then I think basically what we're doing here is constructing a course approximation to that measure okay let's try and unravel this for other people for a second okay so the Adm formalism so we have a differential equation a PDE the Einstein equations let's say and we are effectively trying to solve it as an initial value problem so we're taking one space like hypersurface which is one simultaneous surface and we're trying to figure out what are the values of the you know parameters curvature whatever else on a subsequent space like hypersurface correct right and and then what we're asking is there are many choices of our foliation of the space in terms of space like hyper surfaces and what Jonathan is saying you can parameterize those different sets of choices by at every point giving a lapse function and a shift vector a lapse function being how far how far down in time you're going to get to the next place like hypersurface a shift vector being how far across in space you're going from every point right okay so now we've got this this family of surfaces which is corresponds to one possible ADM sequence so to speak we got another family of surfaces correspond to another ADM family and ADM sequence now you're saying there is a distance metric between those two families but I didn't quite understand how you find that distance mattress well if you take these say the initial hypersurface and family one and the initial hypersurface and family two you can overlay them on top of each other and you can define now of course you're probably your conditions of global hypervelocity but you have in the standard ad game of formalism go away because those types of surfaces obviously will intersect with each other but then you can still define a lapse and a gauge admittedly burlaps might be negative which would obviously not be allowed in the conventional formulation but which we can allow here and so you can take an overall at you can compute the overall lapse and shift distance between those two hyper surfaces that are this of it that they are they are two different hyper surfaces for the same look so what you're saying that's a faux evolution instead of a genuine evolution from hyper surface in model 1 to hyper service in model 2 it's a fake evolution that just says use the same formalism to make the comparison between these two hyper surfaces exactly exactly so or in other words rather than comparing hyper surfaces at two different values of the universal time function you're comparing hyper surfaces for the same value of the universal time production which is different models you compare to do two different foliation yes right aren't you the factor defining a sheaf in doing something similar because it seems to me that we are trying to do is saying I Maps up of these things to some stuff and if they these mappings overlap somewhere I can lift this to a mapping on the union of the two things that overlap did I understand this correctly or that doesn't sound completely wrong it's not the way I think about it but yeah sorry continue yeah go ahead I mean this corresponds with sheaves I've never understood sheaves so so we're I can give you an easy example XI fees let me try to do this trick here I'm trying to switch my camera now you should be seeing my hands oh I'm not technical unfortunately so I'm using a very so at least you're left-handed all the cool people are left-handed thank you yes I am left-handed so imagine that this is my space is literally like a plane and nothing more and now I want to attach some sort of information to regions of the plane so for instance I can have this region here and today's I want to attach a set of things again it doesn't matter what these things are this could be for instance the set of continuous functions the find of this thing yes I told let's do the example with continuous functions this is a nice example I have my space and I take this region here and today's I attach the set of continuous functions on this region okay now you see that I can take a sub region here and attach set up continuous function like this and now what I have is that this thing is included in this thing and here things are counter variant like I can take any continuous function in here and map it to its restriction in this small thing are you following me up to here I think so so the idea is that in category theory this is I am a base category called C which is open sets cold-eeze you call this V for instance ordered by inclusion so for instance I have an inclusion of u into V and this thing is mapped to set contravariant Li which means that if you goes into V then continuous functions on you yessiree continuous functions on V Mach 2 continuous functions on you via restriction cool now what a sheaf tells me is that these assignment is consistent which means basically two things the first thing is that the reason overlapping condition let me change so the overlapping condition says this imagine I have this situation here I have this small region and these big ones now for what we have said since this is included in these two I have two mappings like this okay yeah now the idea is that let me see actually I think any huge yes basically the idea is that if these two things agree on the overlap I can glue them together so from this definition and this definition I can basically see where these two things are sent and then get a unique assignment of this whole thing let me give you one dimensional example because it's probably easier let's imagine that this is the real line and you know I have continuous functions here to each open set I can basically map the continuous functions of the find on this open set now clearly if I have to open overlapping open sets and two continuous functions agree on the overlapping that I can find a big continuous function defined on the Union by just gluing them together yes these are analogous to the kind of selected two charts in an atlas construction for the Minnesota laser in fact all these stuff down in algebraic topology and differential geometry can be recasted in terms of sheets there is actually a correspondence between sheaves and bundles so you know where's the chief so far we've just got correspondences between things like charts where's the sheaf the sheaf is basically this correspondence so given a category C that represents your base space a sheaf is just an assignment to set so again this means that to each region I attach a set of things and every time I have and in an inclusion year this corresponds to a restriction here so that these gluing condition holds and moreover there's a local condition that means that if two assignments agree on each open set of an open covering then they also agree on the whole set they cover so this means that the information is defined locally if two things agree locally everywhere and they have to agree on the whole thing this is not like a super clean and nice way to say it but the idea is that this is a particular kind of sheet in which I am attaching these this is a functor to set and the idea is at which object I'm attaching I'd know continuous functions and two injections I'm mapping restrictions but you know I could I could do things more generally or I could say to these region I literally attach a set of things and the designer region I attach another set of thing and now if I have an inclusion here I will just have a function here of some sort so yeah for instance in algebraic geometry people attach to these things ring or a billion groups or I mean you name it basically any kind of stuff so what corresponds here so Jonathan you you you're talking about the mapping between foliation z-- basically yes and it corresponds to this well I mean it's so fully Asians of a arbitrary space-time can be represented in terms of chief Kamala G classes explain I which part I mean you you have some topological manifold but you can can you can construct say see you can think of a foliation of that manifold as being like a CW complex or something yes and the and and you can define I think you don't even need to use sheep comb ology you can use catch comb ology I think in most cases that if the space is para compact I think they're the same that so at least locally you can define that simplicial econ decomposition in terms of in terms of a sheaf ecology which simplicity of decomposition the one the one where where's there a simplicity composition there's a you you take a manifold you you construct 2cw complex okay and the way you can define that locally is in terms of schuko homology is it probably useful to explain at least the idea behind comb ology thought I understood but you get you're welcome to try to explain it if you have a nice plate yes okay in this case I was telling you imagine that these is an open set view and this is an open covering okay the sheets conditions I was telling about is that basically if I have two assignments from you to something else and they agree on each one of these open sets that cover you they have to agree on the whole you and the other one is that if they agree on all the overlaps if I have basically something defined on all these possible overlaps then I should be able to get a big thing these are called the local condition and the gluon condition for sheaf now I could also have an assignment co-op set which fails to be a sheaf so I don't know maybe you know you don't you can't have a local SEC you you can't probably I don't know glue things together or you know you fail to lift something that is defined locally to something that is defined globally the stupid example I could give is this imagine that I have this kind of space here which is just a thing where I can work on and and to each point of the space I give to assignment of some sort and now I'm saying okay I'm mapping this year this year this year and this year when you express this in shifty erratic terms you see that the gluing condition fails I mean it's not important now to understand precisely why but the idea is that you can have this thing I mean you can intuitively see the mobius strip is a good is a good kind of like thing visual metaphor right consistent assignment case right then should be like more ephemeral staircase yes exactly yes yes like you know you can say you can say yes imagine that imagine that this is a great example imagine that this is actually Asher's stairs you know and which point you're attaching the following information am I going up or am I going down and then you can say okay and going up and going up and going up and going up but wait why am I still where I am so you know you are not able to lift this to a global section as you walk on the on the stairs it always seems like locally everything is going right but when you zoom globally this is an impossible figure now the point of Kamala G is that when is shifting I mean c'mon is a super big field but in this case UK can ask why is this thing failing to be a sheaf and what kamalji does is it gives you a qualitative understanding of what are the obstructions to obtain a sheaf let me give another example the most standard example of comb ology group in a classic setting is you know just the group the fundamental group of a space so imagine that I have a doughnut so a torus basically I'm super bad at throwing this stuff forgive me but I have this thing here that is supposed to be a torus and I can ask can I contract this thing to a ball kept to a point can I contract it to a point and the answer is we know it's not because this thing is not a moat optically equivalent to a sphere what kamalji does is it says I Mac each one of these topological spaces to a group ID actually or if you choose a particular point on the on the space for group and if this group is free meal then I know that this thing doesn't have any like hole or whatever but if the group is not trivial then I know that this thing will not will have some holes in it that will basically not allow me to contract it to a point and so basically the group of where the operation is paths you're taking elements which are paths on the on the space your operation is appending those policies yes exactly and so in this case I can say oh the first common og group of this space is actually the fundamental root and oh if this is trivial then I have no obstructions I can just contract this thing to a point and I'm happy if it's not trivial than I can't but then I can study using group theory what this group tells me about why I can't so cohomology is a weighted with one qualitative analysis of why something that we would like to do fails and in particular in this case yeah I could basically have sheaves and I can say okay I want to test these sheets for some property or I may have some pre sheaves that fail to be sheets and I want to know why and you know I can basically use this bag of techniques that go under the name of karbala G because college is not really one thing to basically associate these things to other algebraic objects so that you know things work out and tell me why so just a question here partly for Jonathon is what is the analog of Co homology for our systems well I mean that's what I was saying right so if you if you think about a choice of foliation as being a co chain complex or something right then then then the class of permissible you know it every choice of lapse function and shift vector is locally fine it's just that some of them globally conflicts because they lead to violations of the causal partial order so you so so that there are certain kinds of Co chains that are simply not permissible because they have non-trivial first comala G or second comala G or whatever and so the way you can kind of parameterize the set of permissible transfer of permissible affiliations of a space in this context is through something like sheaf kamalji okay so that's very interesting by the way so we just just add tonic tits at the point of the point battalion matteo made so if you want to think about the Penrose tripod right so if you consider the group of all I guess the group of all distances from which you could view that all you know the group of all distances from which you could view the tribe are then then the statement that the tribe are is a kind of impossible object corresponds exactly to the statement that it has a non-trivial elements of the the if you consider the como LG of an annulus which is kind of what the tribe R is constructed from right then then the statements of the tribe are can't be globally constructed corresponds to the statement that it has a non-trivial element in its first ecology yeah okay remind me now I'm confused what is the what is the second what's that what's the is it like comet Appa the first and second ecology I should know this the first Kamala G group is if I'm not wrong is basically the fundamental group oh I'm a little confused by something so the description you gave fell of the description of homology rather than Co homology and I know that they related but it wasn't it wasn't clear in the example hard to switch to thinking about ecology because I know it's like oh chain complexes Jonathan you you mentioned that how do we think about this in the context of causal maybe it would be good or so to not be too abstract and to thinking in terms of multi way systems the first column ology group for topological spaces should correspond to the fundamental group of space Zebulon ization of the first degree Tori I'm sorry I was I was not paying attention because somebody sent an interesting thing through on a live stream chat um sorry say the oh is Michael I love Michael Robinson I've met him at least a couple of years ago and he's actually the person that made the sheaves click for me I always thought that was too stupid to understand what a shift was until I saw one of his talks and I will be always grateful to him for this because it really is the guy that made it too thick for me I would be always grateful to you if you can remember what that what the talk is because YouTube could be much appreciated let me see if I can find it but in general the reason why Michael is so nice is because he uses shift theory to do data analysis so it can really give you very practical examples of how how this stuff works I remember it was giving me these examples imagine that you are standing up with a camera and you are taking pictures who are going in circle in like your move circularly you turn around basically you take pictures now imagine that someone when you take the pictures there's someone in one picture but when you are back to that place that someone went away now you can you have all these pictures that you know they overlap perfectly see you early but then you know they spiral out basically and and at some point you have an inconsistency because you are expecting to find a person and to complete as a ring of pictures basically but that person is not there anymore and so now you have two pictures there that are incompatible and then you can use shift theory to make sense of this kind of stuff and how to obtain a global section if you can so it DRD have is I have a base base that is telling me how data are organized and I'm basically organizing data using sheets so that to each point of these base space I have some kind of information and then I can use all these machinery to basically present this data nicely thing in your description you know Microsoft used to have this whole product I can't remember what it was called the thing where they would stitch together pictures to get a better synth I remember that yeah but anyway maybe it became a generic technology but but okay so you're doing your Photosynth thing where you're taking it from all angles and you're trying to reconstruct the the 360 picture but something went wrong in time as you did that so where's the sheaf what what piece of the story is what is the to each point actually in this case you're going in circles so you're topological space is you have your open sets that are the portions of Engl you see okay so you're like and and basically which one of this portion you can attach all the pictures that include that angle of vision in it restricted to it so I'm taking a picture of the wall in front of me my view cone is I don't know 90 degrees so I take this picture now if I take the cone that is 45 degrees I just restrict this picture accordingly and so to each one of these open sets I can attach all the set of all the pictures that include this thing and again when I restrict my view angle view I restrict the pictures accordingly and this is exactly the kind of example I was drawing before with with the circles on the plane in 3d this kind same kind of thing it's just that now my set is not the set of continuous functions but the set of pictures that depict okay the information right so what is there an analog maybe Jonathan what's the analog for us of that story of the earth of what story oh well for example the furthest in this story I think the analog of that is that each possible each picture that was taken is some slice in the foliation somehow well it's a local choice of gauge and the statement that you can't it's like any other comb ology story isn't it's a statement that you have a bunch of local choices of gauge but they may or may not add up to make a complete panorama they may or may not end up being you know corresponding to our valid global choice of gauge okay but so so okay but but but the original question here with respect to ecology of these things is we've got these paths in the multi way graph and we're asking is there some topological obstruction to moving from one path in the multi a graph to another path in the multi way cloth how do you even move between parts what is the deformation of a part I feel like it should be something very simple that just pops out at us if we just think about it a little bit right if it has to be in reference to the rules right so it's a foliation transformation and the topological obstructions are precisely those local choices of gauge the resultant failure of global hyperbole so this is exactly the thing I've been trying to understand for several months now is this thing about the space of foliation z-- I think this this to me seemed like the thing that might come out of you know thinking in category theory ish terms and so on is how do you what what does it mean okay what is the family of possible foliation x' and how do you move between foliation x' and you're saying if we look at the space of all possible foliation x' that there can be i mean in the trivial case right let's look at minkovski space for example in make offski space okay let's say makovski space for we're looking at inertial frames in makovski space we've got a very trivial collection of possible families of foliation x' right and there is no topological obstruction in moving from one inertial frame to another if I'm understanding correctly no but there's a topological obstruction in the sense that well okay in this particular case okay you've picked the one case in which comb ology doesn't help you because look because the local choice of gauge determines the global choice of gauge for an inertial frame that's the definition of an inertial frame but for anything other than an inertial frame just knowing the local choice of gauge doesn't tell you enough right you generally need all of the information about local choices of gauges to determine whether that's a whether that's a globally valid choice of gauge because you need to be able to determine if it's consistent with the causal partial so let's understand what you mean by that by local choice of gauge you mean a coordinate ization a space-time coordinates a ssin basis right a local coordinate patch just as tally was kind of alluding to right okay so we've got for anything other than the trivial case of an inertial frame for anything where there's a non-trivial curvature for example or any coordinate system that isn't just a flat coordinate system we've got all these local choices of coordinates okay so now you're asking as we transform from one and and I'm also confused by another thing what is the what is the in a fiber bundle for example we would also have a local choice of coordinate system and then we have this notion of a connection that tells us different you know how we move from different local patches is that is that but in this case we've just got a bunch of local patches that we are setting up and we've got another bunch of local patches that corresponds to another coordinates for another foliation and you're asking when it's obviously that in in the again details of this are in the general relativity paper but so that our analog of the notion of a connection is a is is a collection of weightings of the hyper edges or causal edges that exist in our networks right so you know the default choice of the leve savita connection that you make and general relativity corresponds to the statement that everything has unit weight and so in particular if you have an edge that's connecting you know vertices U and V then you also have an edge connecting vertex vertices V and u and those have have exactly the same weight but if you relax that condition then you have been allowed for more general types of connections and in particular you can have for torsion metrics and things like that and which page do I go to Jonathan to have give me a chance to oh it's late on hang on let me find it it's somewhere it's it's in the place where I define Riemann curvature on hypergraphs open sets you're talking about open sets here oh yeah okay if you look at page pages 29 to 30 what the heck is this I didn't know you put this is this is this the arbitrary dimensional version of the road some Walker metric yes oh you you told me to put that in yeah well I thought is a good idea I didn't know it anyway sorry okay just 29 to 30 okay so if you look here okay so at the bottom there in the definition of the one bachelor Stein distance so we have this parameter epsilon so the epsilon is a coupling parameter that you can think of as being the elementary weight we are assigning to each hyper edge and so later on I state that we you know work particularly considering the case where where epsilon is U as a value of unity for ever you know for everything yeah in which each hyper edge is assumed correspond effectively a unit of spatial distance but you could have considered so in that case you could have Edge's that had different values go depending on which way you have torsion metric solution so you can actually define it turns out in the continuum limit you can define arbitrary connections this way okay but but so again we're trying to figure out so okay why do we care about this so one reason we care is because what we're talking about is transformations between possible reference frames which I claim although nobody but anybody believes me yet there's going to be important for distributed computing and thinking about that that this idea of of what the possible you know reference frame choices are it's gonna be important but you're saying what is there an obstruction to moving continuously from one choice of one family of reference frames to another what what is that what's the physics what's the general activity version of saying there's a topological obstruction so that that would be the statement that if you you know if you have to space like height you have two levels two possible level sets corresponding to two different choices of universal time function and you want a constructor you want to construct a continuous Defamation from one to the other there will be certain classes of hyper surfaces for which even though the two even of the start and end points the the the initial and final hyper surfaces are both consistent with the with the partial order of the lurancy and manifolds there are intermediate ones which at which are not answered that would correspond to a topological abstract okay but so what is that physically so you're saying I don't have a good answer well let's think about it for a second I mean so you've got you've got two choices of reference frames two choices of them and you're saying I mean as you move between these as you make a defamation of the coordinate system to move between these choices of reference frames you hit something that is not okay is a trivial example right so if you consider imagine a universe with a cosmic event horizon yes you have an observer in one part of the in one side of this cosmic event horizon an observer in the other side right they have different reference frames that are just naturally defined by the expansion of the universe but there is a topological obstruction that prevents you transforming from one to the other that is the cosmic event horizon okay but this is more general so that there's no she's at home Audrey go ahead no I say I'm agreeing I mean it this it's exciting precisely because it you know the cosmic event arising is an obvious topological destruction but there may be very non-obvious topological instructions that we we don't know about and what it means when there's a topological obstruction is that this choice of reference frame which we are thinking is related to these choices that can be thought of as a sheaf a choice of these sheaves that there exists a way of essentially breaking the space of all possible choices of reference frames discretely breaking that because of these topological obstructions so we can essentially classify the sort of equivalence classes or something we sort of continuously deformable groups of reference frames from the other ones so physically gosh what on earth is that physically I mean that is what is that what does it mean when there are two what like for example let's take the up black hole for example are there when you look at different choices of coordinates whether it's you know Crisco coordinate so this coordinator that coordinate do you see things like this happen there is it is it continuously deformable from the original schwa chill coordinates to some more modern coordinate system for the structure black hole well no I mean so firstly if you go from say okay the particular case that I think is probably most illustrative if you attempted to go continuously from the Schwarzschild metric to say the girls front panel every metric then because of the existence of the coordinate singularity there isn't a you know that that's a that's a topological defect in your coordinate system so there isn't a smooth you know obviously if you get rid of the coordinate singularity then then you can make a smooth transition between the two but otherwise you can't because the coordinate single arity has to go somewhere okay so the existence of the coordinate singularity i mean i thought that was a special feature of a bad coordinate system that would have a cool yeah exactly that's why the Schwarzschild coordinate system is not a good one if you're actually interested in black holes so let's take an example on the sphere can we get an example on the sphere where there's I mean there's plenty of coordinate systems on the sphere that have all kinds of crazy singularities so if you're asking for different coordinate systems you're asking weight it's like asking can you can you map from like the already what does the Riemann sphere projection all is that the Merc it's all projection I forget my projection I forget the map projection seven ology but you know it's it's it's a it's a Lambert as a Lambert isn't it okay okay but if you wanted to go from you know a polar coordinate system to something that's like given by projections on the Riemann sphere then you're gonna be in trouble because there's some good so within map projections you're saying that there isn't for some map projections there's a continuous deformation from one map projection to another like so I mean if I take let's just take a random collection let's let's take this is this is a guaranteed dangerous thing to do but let's take a random sample of 10 map projections just for the sake of them I bet half of these are not gonna work but anyway um ah let's say we say something like this is really a horrifying thing to do see this even invading works but but so you're talking about me and just trying to be concrete talking about map projections um Wow why is this so slow maybe I have a bad feeling these spc map projections are something really weird that um some kind of empirical projections their only coordinate charts Oh drat look at that well let's see um let's just try this AG oh that's the wrong thing to 26 I think they're not uh what am I trying to do here um Oh wants to say sorry I just wanna make something where we can actually recognize what's going on you I mean we can see something is happening between these map projections just on that intersection okay here we go okay so here are some map projections all right so what you're saying is there's some pretty funky map projections here but you're saying that some map projections will have the property that we can continuously get from one let's say from that guy to the sky maybe but other map projections like this crazy creature here um we may not so I don't even know what characterize is one we can get from one to another continuously that may be a piece of math I should know but is that what you're talking about basically is when when is it the case that there's a confirmation yeah I I don't know enough about map projections to know the answer to that particular question but so in the case of gr as I say if you want a map say from gold strand pandava coordinates to Schwarzschild coordinates you run into this problem of you know by definition this thing get the coordinates and garetty is a discontinuity and so locally around it in the region where that single out where that coordinate singularity should be appear it should be appearing the mapping from one coordinate system to the other necessarily becomes discontinuous in that neighborhood right the UM right hey we should wrap it's getting really late for everybody um the all right so so what dooming out in trying to summarize a little bit so we I'm still little you know this whole question about how does category theory help us and what is the correspondent in what we're talking about in category theory we're sort of slowly you know circling around getting closer to that question to the answer to that question um and you've raised a number of interesting things about I mean I think I'm beginning to feel a little bit more confident about saying something about this notion of mapping between coordinate but between reference frames um or between between foliation but I don't think we really understand that yet um I think you've mentioned we've talked a little bit about the specifics of things like even Petri nets and their representation of of distributed you know just this the analog of distributed computation I don't know this has been this has been a complicated discussion and I I I also I didn't really get my answer to how do I think about the Infinity category I mean I do I do I have one more chance to try to understand what they're you know how should I think about it I mean it's like you keep on you know like it's an automated theorem proving you keep on talking about the correspondence between the correspondence between okay point of view which may probably help there is a notion of higher category which is called by category there is that in category theory we require that you know composition of morphisms is associative for instance and the identity laws hold up to equality but as soon as you introduce also higher morphism so morphisms between morphisms you see that you can relax this so you can say instead of a circle B Circle C equals a circle P circle C so the associative thing you say actually I want them to be isomorphic and isomorphic in this case means that there are a couple of morphisms between morphisms their one the inverse of the other so that's that's connected to the idea I was telling you before that you can think about higher categories as a weakening of standard category theory we have a standard category and now we have weakened the definition because instead of having an equality we require these to hold up to isomorphism but then I can do the same kind of trick I can consider the composition of morphisms between morphisms and I can ask should this be hold up to quality or up to isomorphism and blah blah blah and that's why if you keep inductively doing this kind of thing then what you get is an infinity category where basically everything is and this is connected to type theory because the real difference in here between having an equality and having like you you draw here isomorphism is that an isomorphism is a kind of constructive kind of thing like you really want to give a function morphism you want to construct it that testifies that these things are this sort of weak associativity so in this sense is like the most proof relevant version of a category you can think about where it you you can't just say oh I go from 8th from F from a be C to a B C but I also have to specify how I go there and if I specify two different ways to do so in two different contexts is then I have to specify a way to go from one to the other all the way up to infinity I don't know if this clarifies things or actually makes it complicated no I I just don't have an intuition I mean to me we very useful to understand you know we've got proofs we've got correspondence between proof and we go on with that process so Steven if imagine imagine you had a version of fine equational proof where you feed in a theorem of the form proof object equals equals proof object yeah all right but those proof objects are themselves proofs of equivalences between proofs and so on that you know that they are there the individual substitution numbers are not substitution numbers on expressions the substitution numbers on rewrite rules the top of themselves proofs of other substitution magazines yep right so the point that probably I think is making is that the the kind of the highest level of generalization of that is one in which proving that the two proof objects are equivalent also proves that the proof objects if each of those proof objects is itself a proof that two proof objects are equivalent proving that the first two proof objects are equivalent also proves that the proof objects contained within them are equivalent and that the proof objects contained in the nose are equivalent and so on so it's it's a great weakening of the other of the otherwise infinite number of equivalence does that you have to prove you just prove one equivalence and then and then all the ones below are the levels below it kind of cascade down this that's the notion of weak I must of the equivalence between between terms in what about mean for I'm still very I mean I I think I and then I know is the model the model for that space is the homotopy type is is the is the infinity category of homotopy type two terms of type a call them P and Q and now I can consider proofs that these two things are equal so where do these proof leave well these will leave in this type here this is the type where are the proofs of these two things cool but then in this thing I can consider W and W 1 and this will be two proofs that these two things are a yep but then again I can consider the type of sure and you see this is already an iron kind of a motor-b type so yeah I get how this is constructed I just don't have an intuition for what I mean this is B and this is Q and a proof equals to say that we can go from one to the other and now this thing means that I can deform this thing into the other and I can have two different ways of the forming these two things so different remote apiece and now this thing will contain proofs that say that actually these two Amata peas are AMA topically equivalent and I can you know I trade this this thing up two infinities it's actually very difficult to visualize right I mean okay but so in the physics case for example this is like saying okay you've got these actual evolution paths we've got the causal causal connections between between events that happen we've got the causal connection we've got the foliation x' that are connections between events and then what do we have beyond that what do we think about well we could also not have anything beyond that like it's perfectly fine if we just have a tree category or a fork category or a nest Amanda but I I'm just curious if there is an interpretation of going to infinity well that's what I mean I think it pretty depends on your model I think that what is worth noticing here is that the way we go to infinity is defining things inductively right from the very beginning there is a convenient inductive way so in in the physics example you make it feels to me that there is a very big difference in how like our zero level things are interpreted how the first level things are interpreted because you say okay the first thing is causal structures and the second thing is equivalencies of casual structures which may not themselves because of structures so I think that the the if we have an Infiniti category structure amounts to ask is there a way to inductively keep going and thinking about relationships and things between things and the answer may as well be no actually I would be way happier if the answer was no because Infiniti category theory is not the easiest thing in the world so if you can avoid that you and as well I have done but okay the the thing for me is that understanding these first three levels you know it's already it's already kind of fun you know we've already it's been already interesting to understand these first three levels and I'm just have the suspicion I don't know it's just maybe it's a piece of aesthetics so to speak that there's something to be understood beyond those levels and maybe maybe it's I mean what what Jonathan is saying is the next level up is the obstruction between defamations between reference frames basically so even maybe that they're improving example was two abstracts but if you want to think about the same statement in terms of multi way systems it would be you know in an ordinary state graph or a multi-layer system if you have two parts through that state's great if you have just specifications of two parts and then you can find a mapping between those two parts that map's vertices on one path diversities on the other edges on one path two edges on the other the fact that you can construct that mapping actually doesn't tell you that those two paths are valid paths in the multi way States graph right what do you mean I thought you said you started with two paths in there yeah so that's how they're generated but suppose I just give you you know I just give you two paths and I say you know these are these are two path graphs and here's a mapping from one to the other from that information you can't then deduce that those two paths are actually valid paths with respect to the original multi-way systems that's correct that's equivalent to saying if I just give you a proof of equivalence between two proofs that does not in itself tell you that the actual expressions that those things are proving are themselves true are themselves equivalent yes right so if there existed an infinity or call into a model for for our observe physics models what it would be would be some ultra generalization of the rulli or multi way graph in which if you could show that there were if you could show equivalence between two paths it would necessarily show equivalences between all paths and all on and all systems of lick enough of lower levels of abstraction including in particular equivalence is between the actual states at the endpoints yes I understand that's the kind of thing I'm looking for right yeah because so this is a non constructed idea right over here if such an object exists that would be its property but we don't yet know well but I know but it but to say that it's a generalization it's the it's the ultimate kind of correspondence between description languages in the rule graph somehow that's what you're basically saying it's some ultimate right it's so it's a correspondence does it will it's a it's a it's a type of equivalence that implies correspondence between equivalent between description languages correspondence between updating orders correspondence between causal affiliations and actually correspondences between individual states as special cases of whatever this more generalized type of equivalence is Right seems worth looking for and that seems like the ultimate sort of category theory prize so to speak in these in these models will be to understand that because that's what you know in the original discussion here about category theory and using it as a pattern to see different kinds of things that seems like the you know to be able to see that everything we're talking about can be put into one framework seems useful I mean it's just like I do think that our correspondence between for example features of physical space features of branch real space features a rule space I mean the challenge I've been continuing to try to understand what's the ok you want it you want to get really weirded out here it's like what's a particle a particle and physical space we kind of understand what it might be topologically what's a particle and branch Hill space and Jonathan here's one we haven't talked about yet what's a particle in rural space I mean that's a that's sort of a yet weirder thing all right anyway we should wrap up here but um no this was this was really interesting and I I'm I haven't quite gotten rid of my fear of category theory but you might make sense it takes I think it takes years to I mean it is by far the most difficult thing I ever had to study and basically when I started my PhD I didn't know anything about category theory and I was forced to learn it because everyone in my research group was speaking category theory so I have no choice but if this wasn't the case I wouldn't have learned it because I find that the most difficult thing in category theory is that it's not enough to understand definitions it really requires a mind shift you have to start asking not anymore who are the elements here and what they do but what are the relationships that this structure has with other structures and you need to embrace this perspective to be able to give the right definitions and it's a very difficult thing to do I got to the point where I was understanding all the definitions and I feel like I felt like I wasn't understanding anything at all because and then at some point he clicks so yeah I think it's not an easy thing to ask more question about this I mean you know in a sense your description given me gives me more sympathy because you know I've been working on symbolic languages for forever right and so there are things there where there are complicated abstract constructions that are you know functions that construct functions that construct them and for me those are pretty easy to understand but you know I've I've known about the most of my life so to speak so you know it makes me more sympathetic to people who find it difficult to understand those things my difficulties I understand a category theory but if I wanted I mean in terms of concrete affine category theory is there I mean one of the great things about symbolic languages is there is you know there's a concrete instantiation of what's going on and you know for category theory I mean is it the case that what you are building with your whole state box thing and so on is that an attempt to make a concrete a vacation of what one can do with category theories yeah in part like obviously being a start-up we are trying in active to build a product before like in for the money runs out yes like our main purpose is basically building a product but yeah we are we think that the categorical perspective will help a lot they say that we are concrete defying category theory up to the point of is useful for us but in general there's a nice book about applied category theory by David speevak and Brendan Fong I think I I think I may even have this book I I've tried to do my homework in this area but but um yes this one and I think it's quite nice there is also a nice book by Emily real you know all these books are very full of examples so okay these categorical gadget can be used to model these say real world kind of thing and by the way we are also with state books giving some category training courses for business and and that's also the perspective we embrace like we present an argument and shortly after we present examples I think is the only reasonable way to to understand category theory especially for applied people for pure mathematicians my own suggestion is still to study from the McLane's book which is an hard book for sure but at least that it doesn't fool you like I remember that one of my of the most disappointing things that happened to me in the beginning is that I started studying category theory on this book which was very easy and you know it would give you a lot of examples that seemed reasonable but actually the book was that they just indulging on my set theoretic understanding of things so every time I was like oh yeah okay I get this nice oh yeah I got this and then at page like 200 it finally introduces at junctions that are really not easily understandable from a set theoretic point of view and at that point I realized I didn't understand like literally I just wasted one month of my life thinking it was understanding suffering I didn't anything at least my claim is honest like it may take one week to go through ten pages but when you go through them then you really understand what's going on so it's really slow and incremental progress and everyone's let's see whether I can fit it into a lifetime so to speak understanding how category theory works [Music] categorical way is the you know right well we should wrap up here well thank you very much and um thank you that's yeah okay

Channel: Wolfram

Views: 145,169

Keywords: Wolfram, Physics, Wolfram Physics, Wolfram Physics Project, Stephen Wolfram, Science, Technology, Wolfram Language, Mathematica, Programming, Engineering, Math, Mathematics, Nature, A New Kind of Science, NKS, Computer Science, Philosophy

Id: 0LAtNXo9rbE

Length: 234min 12sec (14052 seconds)

Published: Tue Jun 02 2020