After a short introduction to the functorial approach to logical proofs and programs initiated by Lambek in the late 1960s, based on the notion of free cartesian closed category, we will describe a recent convergence with the notion of ribbon category introduced in 1990 by Reshetikhin and Turaev in their functorial study of quantum groups and knot invariants. The connection between proof theory and knot theory relies on the notion of ribbon dialogue category, defined by relaxing the traditional assumption that duality is involutive in a ribbon category. We will explain first how to construct the free such dialogue category using a logic of tensor and negation inspired by the work by Girard on linear logic. A coherence theorem for ribbon dialogue categories will be then established, which ensures that two tensorial proofs are equal precisely when their underlying ribbon tangles are equivalent modulo deformation. At the end of the talk, we will show how to understand these ribbon tangles as interactive Opponent/Player strategies tracking the flow of negation functors in dialogue games. The resulting diagrammatic description of tensorial proofs as interactive strategies is performed in the 3-dimensional language of string diagrams for monoidal 2-categories (or more generally weak 3-categories) initiated in the mid 1990s by Street and Verity, McIntyre and Trimble.
 Well, I'm very grateful for this invitation to speak a little bit about this connection between proofs and nuts. And I think there is a lot to explore still, so I will just explain a little bit the basic ideas. And I love this picture that summarizes the talk. So it's about how a proof can be seen as some kind of naughty structure which has to do with the structure of dialogue. And so it's a long question about what is a logical proof, how should we should represent it, describe it, and how we could have a properly mathematical notation for proofs. And my starting point in this talk is the idea of game semantics. So the idea is that every proof of a formula A initiates a dialogue where proponent tries to convince opponent and opponent tries to refute proponent. And this is really a nice interactive understanding of proofs. And so here is a typical proof in, let's say, some kind of Genson notation, traditional notation. It's a little bit cryptic, a bit difficult to understand what's behind. So, but what it proves is so-called drinkers formula, which says that in any open café in Paris, with at least, so we need one drink, I mean one customer, so in the café, so there exists a specific customer Y, which is so sober, it's very sober customer Y, such that if A of Y, which means that Y is drinking, then all the other customers in the café are also drinking. And clearly this is counter-intuitive, but this is proved by this short proof in classical logic. Okay, this property is not true, is not valid in intuitionistic logic or constructive logic, but it is valid in classical logic. And here is the proof. And I said that a proof gives a strategy, some interactive strategy to convince you. So we could, I mean, I could play it with you. So okay, imagine I want to convince you of this property, which you think is a little bit strange. Well, we open, I mean, we enter together in the café. And then I say, okay, I know the customer was, I mean, was very sober, so I could pick someone. So for instance, I don't know, Gerard, if you allow me, I would say, okay, Gerard, you're very sober. So I know that, okay, if ever you drink, everybody else will be drinking in the café. And then the point is, well, I may be wrong. Okay. So you may be drinking Gerard, but then someone else in the café is not drinking. And so my opponent will refute me and say, come on, Paul, you're just wrong. This customer, so I don't know, Nicolas, you're allowed to be, you know, the counter-witness. So okay, say, okay, come on. You know, here, I see Nicolas is not, I mean, he's not, so he's a counter-example to your claim. And so the proof what he does interactively is to allow me to backtrack. And so this is a little bit hidden here in the fact that there is two existential here introductions in the rules. It allows me as, you know, prover to backtrack and say, oh, sorry, I was wrong. I shouldn't have picked, you know, Gerard at the beginning, I should have picked Nicolas. Okay. And so the idea is that the fact, I mean, the reason why the existential here is not constructive. Okay. It has to do with the fact that I did use the witness from the interaction I have with the, with the opponent. Okay. So in a way, I cheat. Okay. But this is exactly the way classical logic works interactively. And I mean, you can, you know, instead of speaking about the drinker formula, you can say that this formula says that every, every, you know, proposition is either true or as a counter-example. I mean, you can think of the way here as a counter-example. And of, I mean, and clearly, you know, before a property is proved, well, this, still this property holds because if someone finds a counter-example, then we have the counter-example. I mean, this is the same story I've told you here. Okay. And so in a way, this syntax is a little bit, you know, difficult to understand while the game semantics gives a more, much more intuitive understanding of it. And so let me speak briefly about, you know, the way, you know, game semantics and algebra are connected. So this is through linear logic and a number of connectives, which in fact are really adapted or are really consistent with linear, linear algebra. Okay. And so here we have negation, which is really like a dual in, and I will come back to that in linear algebra between the game A played by, you know, the player and the game, not a same game, but played now seen from the point of view of the opponent. And so negation peruse the whole of opponent and proponent. The sum here is what it does. It says, okay, let's start with two games. So there is a game A and a game B, there are some. So imagine this is chess and poker, for instance. Okay. So some of the game is the game where I as a player decides whether I want to play chess or I want to play poker. And then once he's decided, we carry on. We never come back to the other board. Okay. And so this is understood as here is this, this junction. Okay. It's a choice I do as a player, but there is a dual connective, which is just the same, but where opponent makes the choice. And this is understood has a form of conjunction because if I let the opponent, you know, the environment choose, then clearly I should be a master in chess, but also a master in poker if I want to, to, you know, win the game, because I don't know what the opponent will choose. And so this is really some, a notion of constructive, you know, conjunction. It's an ant. Okay. So this is a little symbol used for ant. But there is also a tensor product where the two games are played in parallel, but only opponent is allowed to switchboard. Okay. And so player will just play where opponent has just played. And this is understood as a classical conjunction when I say classical, I mean, in the sense of classical logic. And there is a dual where it's same, but now player is allowed to switchboard. Okay, and the nice thing is that this is can be understood as a form of classical disjunction. And so I will show you how to establish the fact that for every formula, so for every game. So here, for instance, let's, let's take a data mind, you know, version of chess. Well, we have the property that a, let's call it the chess is called property a, or here, not a. Remember, it's just you swap the board. And so I will give you an interactive strategy which wins in that game. And so really the idea is that we are playing, I mean, I am playing two boards here in parallel and here in front of me, there is a tensor product and the tensor product can be seen of a strategy or counter strategy of type tensor can be seen as a pair of strategies. So let's say I'm playing against two, you know, famous Russian chess masters. And I will show you how I can win by playing here white and here playing black. Okay. And of course, I mean, winning, you know, I'm not crazy. I cannot win against both. Or if I want to win against both, I need to be a very strong master myself. But here is by pure logic. So there is no, I mean, it's just by some kind of logical, let's say manipulations or logical, you know, truth. Okay. So I want to prove that a or not a and the strategy to do that is just to let it's very simple and it's like cheating really. So it's to let course noise start here. And so course noise plays a move like this or here. And then copycat what course noise has done on this board. And I can do that because as because this connective, you know, enables me to play, I mean, to switch board when because whenever a move has been playing on one board, I'm allowed to move to the other board like this. Okay. And so I've copycat the move by course noise, carp of answers. And then I move to the other board and I play like carp of. Okay. And then course noise answers and then I just move like course noise has just moved. And in that way, I just by copy, you know, some kind of copycat strategy. I mean, carp of really believes is playing against course noise and course noise is really believes is playing against carp of and in the end, one of the two wins. And so that means that I will lose maybe carp of wins. So I lose on this board, but I win on this board. And after I want to prove that they are not a. And so that means that I only need to win on one of the two boards. Okay. So the idea is that we that, you know, we can understand, you know, the fact that the properties through or its negation, something purely interactive and purely linguistic, which doesn't have to do with the, you know, outside world. It's not about whether today it's, you know, cold or hot weather. It's really about just pure linguistic phenomena. Okay. And so I mentioned that there is also this exponential modality, which is very nice. I will not speak about it anymore in this talk, but it's nice to know that there is something which enables opponent to reopen to reopen balls whenever the opponent is embarrassed. And this is what happened in the drinker formula thing. At some point I was embarrassed as a player. So I reopened a new board and I won on the new board on the second board using information I knew from the first, the fact that I mean, Nicola was the good witness and not Gerard. Okay. So this I learned on the first board and then I use this information on the second board. And so, and by the way, this, I mean, maybe I will have the time to mention it, but this has to do with co free constructions of co-algebras or commutative co-algebras in vector spaces. And okay, I try to come back to this, but now what I will try to show you is that there are connections between these ideas of, you know, game semantics and ideas coming from linear algebra and representation theory. So okay, I will, I will move that. Okay. And so, but before I do that, there is this important, let's say tool coming from categories and ideas by Lombak in particular, which is to give a factorial approach to proof invariance in the same way that we will see there is a functional approach to not invariance. Okay. So, so I will speak about the, in particular, I will start from this idea coming from Brewer, Haytman, Kolmogorov, that a proof of a conjunction. Okay. So, there really is a pair consisting of a proof of a and a proof of B. Okay. So, and the idea is that, I mean, from the game semantics point of view is that someone, you know, if I claim a and B, my environment, my opponent could attack me on a or on B. So I need to be able to prove a and to prove B. So I should have a proof of a and a proof of B. Okay. So this is fine. And we will see that this will be interpreted by the existence of a Cartesian product in categories. But then there is this more mysterious description of a proof of a formula from A to B in logic as an algorithm, which is able to turn any proof of A, Phi, into a proof of B. Psi of Phi. So this algorithm Phi, the question is what does, I mean, what does it mean, an algorithm? And this was, I mean, this is still a question that people, I mean, it's not so clear. Whereas here it's quite clear what it means. Okay. A pair is a pair. But an algorithm is something like saying, okay, I have a notion of algorithm somewhere in the air, but I don't know exactly what it means. And so the notion of Cartesian close category is an attempt to answer that question by saying, come on. Okay, an algorithm will be a map in a specific category. But this category should be Cartesian. So it should have a Cartesian product. And it should be closed in the sense that we should have a family of adjunctions between the function A times and the function A implies. And what this means is that we have a natural bijection between the set of maps from A times B to C and the set of maps from B to A implies C. And we can think of this as some kind of implication. So clearly a basic example is the category of sets and functions. Okay, but there are many, many other examples. And we spend a lot of time, you know, when we study proofs to construct Cartesian close categories of many shapes. Okay. And so, I mean, just, I mean, a typical example is every topos is such, you know, every, every, every category of shapes is such. And there are many, many other examples that we can analyze. It's a very rich and interesting topic. But here I want to focus on the free construction. Okay. And so, and you will see it's very symbolic. And so if you want to say, okay, I know I start from a category. Now I want to construct the free Cartesian close category. And you think about it, you say, okay, I should start by the objects and the objects, they should be constructed from the objects of the original category. And then the products and the implications. Okay. So there should be this grammar of objects. And so the objects of the category of the free Cartesian close category are constructed by this grammar. Okay. So you can think of them as formulas or as types constructed by this, this, this very simple grammar with Cartesian product and implication. And here, again, Cartesian product is some, you can understand it as some kind of conjunction and implication here. Okay. And so the, the, the, now the morphisms in this category, they are not as, I mean, there are a bit subtle to define, to describe. And I will just say a word about them. So they are lambda terms. And so just to say a little bit, you know, a word about lambda terms. So lambda, lambda terms are terms in a calculus, which is a pure calculus of functions. Okay. And I will say a word on that now more. But then these terms of this calculus should be considered modulo some, some notion of beta, eta conversion. And what I claim here is that the situation is very similar to what we have in nut theory, where we have like this tango diagrams. Okay. And then up to deformation of diagrams. Okay. Typically, write the master moves. So, so how is the lambda calculus defined? I mean, there is some kind of, I mean, some kind of calculus where you describe functions in a given context. So typically you said that there is, for instance, a function x. Okay. This is just a variable in a context where x is of type a, and then x will be here. This term will be of type a. And the most important two rules is the abstraction rule, which says that if you have a term p of type b, okay, in a given context where the variable has been declared of type a, then you will construct the function, which is written lambda x dot p. And the function here, you can think of it as the function which to x associates p of x. And so this is the notation here. And this type is the type of functions from a to b. And so I said implication, but you can also think of it as description of some kind of function, function space. Okay. All the functions from a to b. Okay. And since the variable here is of type a, and the output is of type b, then lambda x dot x, this function is of type from, I mean, a implies b. And once we have constructed such a function from a to b, we can apply it to an argument. So this is the notation. So p is applied to the argument to get something of type b. So the argument is of type a, applied, I mean, we apply the function of type a implies b, or a to b, and then we get something. And then there are three basic rules here that organize, I mean, that deal with the context. And so then what are the beta and eta rules? So they're very cute rules. I mean, they are very beautiful and powerful. So the first one says, okay, if I have constructed the function, which to x associates p of x, and then I apply it to an argument, then I will get, I mean, I can rewrite it into the same, I mean, the p, but now it's p of q. And this is the way it's written here. So because it's a pure calculus of functions, we have variables x appearing in p. And so we can then substitute them by q. Okay, similarly here, there is a rule which says that every term of this calculus can be seen as a function lambda x, which to x associates the term applied to the argument x. Okay. And this is completely formal, completely symbolic. But at the same time, it's known to be deeply connected to a language, I mean, a language of proofs. And so this lambda terms here, this lambda terms in red, they can be seen as proofs of some propositions which are written with implication here and conjunction. So there were these, you know, little logic calculus here of, which you can see, think also as a calculus of formulas and here, this is the description of the proofs of these formulas. But what is important, I mean, okay, I don't ask you to understand all these details about proofs and formulas. But what I want to stress is that there is a completely algebraic construction of the free Cartesian closed category. And what this means is that whenever I take a category C here, and I have a functor into a Cartesian closed category D, I can lift this functor to the because this is Cartesian closed, I can lift this functor from C to D to a functor which preserves up to coherent isomorphism Cartesian product and the implication arrow, okay, from this free Cartesian closed category into D. And so this gives, so this construction is extremely important in the construction of what we call proof invariance. And I mean, you know, I work in a, in a, in a like computer science lab. And the reason is that in fact, this lambda calculus can be seen also as a language of programs. So there is a nice correspondence between proofs here and programs. So you can think of it as a very simple programming language here. If you like that you transport, you interpret all the, so the morphisms are programs and you interpret them into some category. And so here, the category typically will be, could be a category like the category of sets and functions could be a, you know, a pre-shift, a pre-shift or a shift category or a topos or whatever. As long as it is Cartesian closed category, we have this beautiful little functor, okay. And the, okay, this is the story for, for, you know, what, what, what I would do, you know, all my day, okay, constructed this kind of things. But then people in, I mean, studying not invariance, and this is the connection with, with nuts, they do something extremely similar where instead of constructing, so, so they start from the functors, let's say, I mean, it's one way to think about. The construction of nut invariance, there are many ways to construct nut invariance, but here I will describe the functorial approach, which is to say, okay, if I'm able to, to, to associate to every color, you know, an interpretation in a ribbon category, and I will explain briefly how to construct such ribbon categories using representation theory of quantum groups. So when we have such a ribbon category and a functor into, into that, we can leave the functor to a functor which preserves the structure of ribbon categories. But this, I mean, this free ribbon category is a, is a category where the morphisms are frame tangles. So in particular, we can study like ribbon nuts and we can associate invariance to each ribbon nut because this category is, is, is typically the morphisms from the unit object to, to, to itself are, are ribbon, I mean, ribbon diagrams which are closed and so they are, they are really like ribbon nuts. And so you see there is this very, I mean, kind of fascinating analogy between what we do with proofs in the functorial semantics of proofs and the functorial, you know, invariance of, of nuts. And so I will try to explain the connection. So I will go very briefly just to explain this ribbon categories on string diagrams. So it's a notation for monoidal categories. So the idea is that a morphism from A tensor B tensor C to D tensor E will be described as some diagram with three inputs and two outputs. Okay. So ABC here as input and DE as output. So, so the flow, I mean, goes in that direction from, from the bottom to top. Okay. So this is the arrow here. And so composition is described by vertical composition. So the composition in the category and the tensor product as horizontal, I mean, putting side by side F and G. So typically here is an example where F tensor identity. So F here identity here and then F tensor identity composed with identity tensor J. Okay. So, I mean, if you, I mean, if you interpret this morphism here in the string diagram notation, you get this picture, but then if you interpret this other morphism, you get this picture where you see here F and G have been kind of, I mean, we play with the order in which they appear here. And the point is that in a, in a monoidal category, these two morphisms are equal. So really we can be, I mean, we can trust our eyes up to the formation of diagrams. And indeed this diagram here and this diagram here describe the same morphism. Okay. And this is really the beginning of a beautiful story where you try to make, you know, this topological intuition valid up to the point where you can say, okay, I have a nut and I described as a morphism in a specific category. And the morphism is invariant up to deformation. Okay. So this is what I will explain now. Okay. So a braided category or monoidal category is just a monoidal category equipped with a braiding. So it's a family of isomorphisms from A tensor B to B tensor A. So, and this is the way I will draw them. Okay. I think many people here know this, all the story, but I felt that it's good to tell it again anyway. So this is the way the braiding is described, but of course there is an inverse which is described as a negative braiding whereas here it's a positive braiding. And our coherence diagrams. So this one, for instance, says that these two sequences of arrows are equal in the braided monoidal category. And diagrammatically it says this, okay, that if we permute A with B tensor C is the same as permuting A with B and then permuting A with C. Okay. Another diagram which is essentially saying the same, but for the other configuration. And so this is like braided monoidal category, but then we can define, and I will be very much interested in the notion of balanced monoidal category. So it's just a braided monoidal category with a twist, which is defined as a family of isomorphisms and which I will depict as a twist like this. Okay. So there is a little like we twist the ribbon and this is why I work with ribbons rather than just strings. Okay. So we can see this little action here on the ribbon. And so it should satisfy that theta i equals the identity. So when we twist the unit, we just do nothing and then this very nice equation, we say that when we twist the tensor, so when we twist the tensor, it's the same as braiding, twisting, braiding. Okay. And so this is the way to sit. So if you want, so A tensor B is really A and B in parallel. So if you twist A tensor B, this is what you get. You need to twist A and B independently, but also braids them twice. Okay. So you see this is a typical example where purely algebraic, you know, coherence property, which says that this map should be equal to this sequence of three maps, coincides with a very topological intuition about how we twist ribbons. Okay. And so now I carry on, you know, what I'm trying to do now is really to build what I will call a ribbon category. So we have, we need a notion of duality. So a dual pair between an object and A and an object B, where we say that A is left dual to B, is defined as a pair of morphisms. So one morphism from the unit object to A tensor B, and the other morphism from B tensor A to the unit. So you can think of it as some kind of identity here that we are building. And here are some evaluations. So this is sometimes called co-evaluation map and evaluation map. Okay. So typically we have that when A, imagine that A is a finite dimensional vector space and this is B is the vector space of its, I mean, it's dual vector space of forms. Okay. So like this is V and V star. Okay. And so we ask that these equations are the exact equalities are satisfied, okay, which are represented like this. And we said that, yes, so in that case, we said that A is the right dual of B. And yes. So anyway, a ribbon category is simply defined now as a balance category. So if you remember, it means braiding, twisting, okay. But moreover, every object A has a right dual. And there is this further requirement that when I take A star tensor A and I twist A and then I evaluate, so I get this map from A star tensor A into I, or I twist A star and then I evaluate, I should get the same. Okay. And the nice thing is that once we, I mean, in any ribbon category, the object A star is also left dual to A. And so you can use the twisting and the braiding to build, I mean, a unit, so a co-evaluation map and an evaluation map, but where you see A star is on the right now. Okay. Oh, yes, so here. So A star is not anymore just a right dual, it's also a left dual, thanks to this structure of twist and this equation. Okay. And so in particular, we have this nice equation satisfied in every ribbon category. That twisting is the same as braiding and then doing this, you know, playing between the here, co-evaluation and co-evaluation, but this is the original evaluation and then this is the one that we deduce from the twist. But we can also define the twist from that fact that A star is at the same time a right dual and a left dual of A. Okay. And I will come back to that later because we see the similar phenomena appearing in logic and I claim that this is of course topology, but in fact, and this is really the purpose of, you know, I mean, my work, but also this talk, okay, is to show that this kind of phenomena can also, I mean, it's interesting to look at them from a logical point of view. And there are some kind of maybe projections of some more, I mean, like let's say, people say purely logical structures about negations. Okay. Because of course, when I say duality, I have in mind some kind of negations and we will see that these dualities can be seen as particular instances, extremely interesting and rich, but instances of a more general pattern where negation is not involutive anymore. So something important here in this ribbon category is that when we dualize twice an object, we come back to the original object, which is true for instance for finite dimensional vector spaces, or we see representations, which is not true anymore for general vector spaces because typically the map from V to V is double negation or is by dual is not an isomorphism. And so, I mean, what we see here, this phenomena, okay, I mean, this kind of very nice, typically here reconstruction of the, I mean, the twist here from dualities. So you know, these equations can be also played and I will come back to that as a logical level and I will explain how to do that. Okay, anyway, we have this free ribbon category. So there is this beautiful theorem by Schum, which says that the free ribbon category can be constructed and it has, okay, so it's a free ribbon category generated by a given category. So the objects are sine sequences of objects of C. So sine means that epsilon 1, epsilon k are plus or minus to indicate the direction of the links. And the morphisms are frame tangles. So frame tangles means they are ribbon, you can draw them with ribbons with links labeled by maps in C. So this is a typical example. So this is a map from A plus to B plus C minus D plus. And so you see A plus, this is the input. So the map goes in that direction and the output is B plus, I mean, I could say B plus tensor C minus tensor D plus and the C minus here, the minus means that the flow of, you know, of the computation goes in that direction. Okay, so this is typically a map in this free ribbon category. Okay, and so clearly I want to, you remember that in the free Cartesian close category, the maps were proofs, they were lambda terms, they were very symbolic objects, whereas here is purely topological. And so my purpose in the next 15 minutes is to show you that there is a way to think about lambda terms, at least in good situations where the lambda terms are linear. I will explain that. Okay, and you can think of this, you know, in connection to the next talk by Noam Zeilberger. So when the lambda terms are linear, then we get a very, I mean, slightly mysterious, but also very natural, I mean, the two connections between proofs and nuts. And so as I was saying, okay, this category here for the free ribbon category, as this beautiful property that defines the free ribbon category. So every time we have a category with breading, twists, and good dualities, we can take any functor from C to D. So here, really, you should think of this functor as giving an interpretation to each of the links here. Okay, so we give an interpretation to each of the links. And then just from the fact that this category is ribbon, we can lift this functor to a functor where the tangles, of course, it's very important here, the frame tangles, but in the topological sense, okay, so really, modulo deformation, if you like, are interpreted as morphisms of this category. And it's a way to construct many invariance of nuts in topology. And so I will try to explain how this can be adapted, but maybe before that, I will say, I mean, I think it's nice, especially here, to spend maybe five minutes explaining how we construct such ribbon categories, okay, before I move back to proof, because I want to show also that the fact that I look at proof has to do with finite dimensional versus like, possibly infinite dimensional representations of quantum groups. So the idea is that one way to construct these ribbon categories is to define them as categories of modules of half algebras. So suppose given like a symmetric monoidal category V, so you can, for instance, take the category of vector spaces over a field, okay. So bi algebra is an object H of the category V, equipped with a multiplication and a co-multiplication. So I use this diagram here for blue for multiplication. Remember, I always draw, oops, sorry. I go from below to top. So this is multiplication of H and unit and co-multiplication and co-unit. And we should ask these equations so that you know, okay, so typically this is the bi-algebra equation, which says that multiplication and co-multiplication are compatible in this way, okay, and then similarly for, I mean, unit and co-multiplication, multiplication and co-unit and unit and co-unit. Then an antipode is defined as the morphism from H to H, which satisfies these two equations. And whenever we have such, okay, so half algebra, which is a bi-algebra equipped with an antipode, then we can construct a monoidal closed category of left modules where the action on the home, the internal home, is defined by this formula. So I wrote it in the Swidler style, okay, and this generalizes the usual construction for groups, okay, where, so you can think of your half algebra as a group and then what you're asking, I mean, here, this says that you should multiply each input by the inverse of H, apply the function and then multiply by H. And so this is just the quantum group version, but there is the diagrammatic representation of it, okay, that I can just show you here. So that means that this object, the right negation, has, I mean, is an H module, okay. Similarly, there is also a way when the antipode is reversible to define a closure on the left, okay. And so similarly, except that we need to use this inverse of the antipode and we'll get the good properties, required properties. So this is a way to get, you know, this implication here. I mean, so what we get is a monoidal closed category on the two sides, left and right. But now maybe we want that to have also a braided monoidal category. So for that purpose, we introduce a notion of braiding on the Hopf algebra, which is in fact a vector of H tensor H, which satisfies a number of properties which can be represented diagrammatically like this. And now the important point here is that every braiding, okay, induces a braiding, so a braiding on the Hopf algebra induces a braiding on the category of left H modules, okay. And the idea is that you just take V, I mean, like a vector, like V tensor W, you swap W and V and you apply your, I mean, you multiply the braiding, okay, of your Hopf algebra at the same time as you permute the vectors V and W. Okay, so then what we get from that is a way to relate the, let's say, right negation with the left negation. And this is extremely important from my angle, like logical angle, because it's really saying that this braiding will induce a map from the left negation or right negation to the left negation, and that this can be understood in a very logical way, as I will explain. And this map, in fact, can be, I mean, if we compute it, this map, what it does, it associates to any form here, this form where we pre-compose the form with an action of U, and U is equal to this vector here and can be represented in this way, okay. And this is an extremely important vector in the theory of quantum groups. The thing is that it's, as a bad property, that it's not a group-like element. So in order to obtain a group-like element in the Hopf algebra, the very natural way is to define a twist. So this is where we get back to ribbons, which is just a vector of H satisfying these equations that I drew here diagrammatically. And then when you multiply the U with this twist, or its inverse, well, suddenly you get a group-like element. And there is an element of magic in this thing. This is something I try to understand, let's say, from the outside, looking at, let's say, braided monoidal categories and so on. And the reason why it's very important is that, in fact, it's related to this, I mean, all the work here that I'm describing was really developed by Rechetikin and Turayev in the 90s. And they're really the fundamental observation is that if we take the finite dimensional modules, this defines a ribbon category. So if I go back to my little picture before, sorry for that, but here I have this category of finite dimensional representations of my Hopf algebra with structure. So I can interpret ribbons as morphisms between such representations. And then using that, we can construct invariance of the ribbons. So it's a beautiful recipe. And I try to think about what I mean, its logical meaning. And so to that purpose, I will introduce the notion of dialogue category. So ribbon is about ribbons, and since I want to speak about dialogue games, I found it's nice to call my categories like dialogue categories. But you will see they're extremely stupid categories. I mean, the way they are defined is absolutely obvious. So the important thing here is the connection with games and mnemonics, the thing I was telling you before and the idea that there are proofs are based on interactions. And so the dialogue category is just defined as a category with an object button and a natural bijection. So we ask that there is a way to turn any map from A to B to this object, which I will call bottom. And you can think of it, for instance, as the base field, into a map from B into A implies bottom. So this is a very familiar situation in linear algebra. So we can do that on the left or on the right. And this is just a definition of a dialogue category. So it's very stupid and primitive. The important thing is that then we can look at, introduce the notion of pivotal dialogue category, which is a category where we can play with the inputs of forms. So whenever I have a map from A to B to bottom, I can turn it into a map from B to bottom. And this is the way I like to represent that. So it's going like this. And then when asked the coherence diagram, which says that if I turn A and then turn B, it should be the same as turning A to B. And this can be understood as some kind of coherence properties of a map between the two negations that is here, the coherence property is here. But what is important here is that we get from this, I mean, a notion of dialogue category with, you know, so, okay, so this was a pivotal dialogue category, but we could also say, okay, I will define a balanced dialogue category just as a dialogue category with these two negations, a braiding and a twist. And the important property is that every balanced dialogue category is defined as a pivotal category. And what is, I mean, an important observation is that we really need the twist to do that. So the idea is that whenever I have a map from A to B to bottom, I can pre-compose it with braiding, but also with a twist on A here. And really the intuition is that the, I mean, this operation of wheel I was describing here can be described at the same time as a, I mean, you see here is there is a twist and a braiding. So the braiding would not be sufficient. And this is the same, I mean, this is really related to what happens with HOPF algebra. So in the case of HOPF algebra, if you remember, we needed a little tita to make, to construct a group-like element in H. And here it's the same story that, I mean, in that, okay, I mean, when we have a good ribbon of algebra, in fact, the category of general representations, so finite dimensional and infinite dimensional, defines such a balanced dialogue category. Okay. And now from this structure, so in particular, I mean, so it satisfies this pivotal coherence property. And from that, what we get is that when bottom is the unit object of this dialogue category, then that the finite dimensional H modules define a ribbon category. So before what's, I mean, it was, I mean, here it can be deduced from a purely, I mean, a purely categorical and formal way that we have this property. So I will, so I don't have too much time, so I will just show you a little connection between proofs and nots that makes it even more meaningful. So the observation is that, you know, in a ribbon category, every object bottom, in fact, defines left and the right negation where whenever you dualize the object, you tensor it with this bottom. Okay. And so now in the same way as we constructed the free Cartesian close category, we can construct the free balance dialogue category. So I will show you the way it's constructed is very similar as the construction for free Cartesian close category. So it's just the objects are, let's say formulas constructed with a tonsure product, left negation and right negation. And then the maps are proofs. Okay. And so proofs of a logic that I call tensor your logic because it has to do with tensor your algebra. And the proofs are constructed exactly in the same way, you know, using the same, let's say Gensen like, you know, Gensen like constructions of proofs. But there is of course a little care about so called exchange rule. So a logic. Okay. So we need to care a little bit because this, this is really about, I mean, we're manipulating the hypothesis of a proof and so we manipulate them with nuts and rebounds. So we need to have a little bit of information about that. But this can be very nicely done using, I mean, the traditional proof theory is just a very basic adaptation of it. And from that we get the free dialogue category with a ribbon structure. Now we know that every time we have a ribbon category and we fix an object bottom, this defines a dialogue category here. So where we have, you know, two negations on the left and on the right. And so just because it's the free dialogue category, we can construct this functor and the main theorem and I will stop here is that the functor is faithful. Okay. And so what this means is that two proofs here in this logic, I mean, this is the world of logic, this is the world of topology, two proofs are equal in this category. If and only if the underlying ribbon structure is the same. And so I will just show you an application of that because this can be seen as a coherence theorem for dialogue categories. So imagine I take a an object in the dialogue category and I map it here to its double negation and this map is not involutive. Things for instance, you know, you're working in the category of general representations of quantum group. So this is not, I mean, this is not invertible. And then we can also take this other negation to where we take the left and right negation and we change the order. Then we can apply, you know, the two turns here enables to connect these two negations to these two negations. And the point is that we don't, I mean, if we do that, it's not equal to this one, we need to twist also the output and to see why. In fact, so this commutative diagram, I mean, imagine we want to prove that is commutative in any dialogue category. And so we need only to prove that it's commutative in the free dialogue category. And how do we do, well, we construct, we see the two maps as proofs. Okay, so there are the two maps. This is, this one is here and this composition is here. And then we look at their images through this, oops, through this factor here. And the images are just tangles. Okay. And the tangles, what they do, they follow, they track the manipulations we do on the formulas and in particular on this bottom. So they track the bottoms. And then the two tangles here are equal and we know that the proofs are equal. Yes. So I'm, I mean, I could speak more, but I think I'm finished with time. Yes. Maybe you could leave some time for questions. Maybe I should just say one word that these tangles here, what they represent, and maybe I will just show you this picture. Okay. What they represent is the flow of negations in the dialogue between the open and the player. So if you remember at the very beginning, we had this interaction between the prover and the refutation. And in fact, these tangles here, we, they can be also understood as little stretch, but they are not very good. So we have these two strategies where opponent ask a question or maybe I could play here. Opponent ask a question and then the player answers here. Yeah. And so there is this interesting relationship that I think would be, I mean, it's worth exploring more between proofs and topology. Thank you very much. Yeah. Thank you very much, Paul-André. I'm not sure we can hear you. At least I cannot. Yes. Cannot. Do you hear me, Paul-André? I can hear you. Okay. Good. Does anybody hear me? Yes. Sorry. It was my fault. No, no, it is because now you are on the dialogue mode. Yeah. But I realized that during all that talk, I had the sound off. I didn't realize that. So if you wanted to stop me, I was like, you know, a raging bull. I don't know. Okay. So are there questions? Actually, I have a question. It's Maxim. Can you say it? Yes. I got lost a bit when we discuss this, all this branding. Do you introduce because there's so much literature that's kind of polluted by brandings or it's really in this dialogue, things that you don't introduce branding by hand and it appears by itself? Ah, well, the thing is, there is this dream we have to understand the topology of proof. Yes. So in the traditional, you know, logic, we have this so-called exchange rule. So where we need, I mean, clearly when we describe this comes from Genson, it's an old tradition, we need to permute the hypothesis in a proof. So, and so the thing is usually we don't track, we don't track the permutations. Okay. We say it's a symmetry, but then it makes sense to say that whenever we have such a So it's kind of generalization by national grade. But I would not say, I mean, yeah, it's generalization, but I would say it's a more refined picture because this can be done, but now we track, we remember. And so now in the proofs, so, okay, so typically just to show you a proof, we will remember the permutations. Traditionally, we don't because we don't care. But now because we track them, we can get this free construction, which is, which has the, it's some kind of grammar, like a categorical grammar for infinite dimensional vector spaces with braiding. So I mean, and so the braiding is produced by the by the HOPF algebra action. And that's the idea. Yeah. Maybe I just want to give you a comment if you, because it's braiding seems to be it's kind of bit artificial, like fashion instance. Yeah. But if you can see just notion of by algebra, yeah, without anti-port unit to unit just very simple product and coproduct and look how many, this is a basis of map from N spiral to M spiral. Yeah, of course, there's some kind of normal form, but intrinsically there are also some three dimensional manifolds, some colorings. Yeah. So it's even without braiding one can see three dimensional picture. Yeah. So that's, that's, that's, yeah, indeed. And maybe, okay, you know, really all this work started from this more, I mean, you know, no, I mean, unbridled, but, but where, where I manipulate trees. So I, I agree. I mean, but what I wanted to show is that this phenomena that I agree with you there. I mean, there, there appear and it's there a bit questionable. Okay. What are they doing that in fact, from there, they have, they have some kind of, they can be understood at a logical level. That's what I mean before. Because the thing is when we look at ribbons diagrams, we see a lot of phenomena and it's difficult to understand what is really coming from the topology and what is coming from the fact that we can negate and we can turn things. And so the story that I want to tell. So for instance, I mean, just to say very briefly, this thing which I mean, which would have emerged anyway in proof theory without we did not read. So this operation that I was describing here of permuting, you know, to, I mean, by, by doing this kind of operation of, of, of, you know, if we think of a problem, you know, if we think of a proof as something very concrete, not, not something, you know, in the air, but something that people manipulate in space and time, you know, like, like we discussed, then we see that, that this operation is very natural. And then we see that the twist appears here. So, so there is this, I would say, surprising and slightly, I mean, we want to understand it's not, okay, this, this connections and maybe just, yeah, that's, that's, but I, I agree. And I would need, you know, I think we need many faults. I mean, at some point to avoid maybe these breading. My suggestions through to avoid breading make something simply. And in other things, it is all these games also relate to logic and some different way when you consider the statement is which sequences for any, for any, for any, it's like a game. Yeah. Yes, with the exist, but it's, yes, so maybe I should mention very briefly, I mean, just this last, there is something that I wanted to say that there is an interesting open problem. I mentioned the exponential modality, which you can think of, of it as a co free commutative common, okay, generated by, you know, and I, for the moment, I mean, so recently, not, not, not very long ago. Like, I mean, people like Daniel Murphy have, have, you know, studied this construction in, in the category of vector spaces. So, and so it, in fact, I mean, I have shown that it's connected to, you know, three less finite dual construction that, you know, this is one, I mean, I mean, this, this construction is far, I mean, far, far from obvious for me. I would be interested to see how this construction, which we know now on vector spaces could be lifted to representations. Maybe it exists, but I don't know it. And this is the kind of things I like to discuss with Gerard and the connection with automata theory here. And I, you know, all the story I've, I've told was about linear. So let's say arguments where we cannot repeat hypothesis. And so in the case of the drinker formula, the point is that we can, we can construct a co free, I mean, the algebraically, the story is explained like this, that we can construct a co free commutative communoid above the existential. So we have the existential. And this is what enables us to backtrack and change the witness. So if you remember the first time I was taking the Gerard as an existential and then I moved to Nicola and algebraically, this corresponds to the fact that I can construct this bank. So here, so the co free commutative communoid on top of a formula which contains an existential. And, and honestly, I don't fully understand how this could be, you know, expressed in the language of, you know, this hope for algebra. But I'm, I mean, I would love to have elements because that helps me to understand the material nature of proofs. I mean, this is really the point in a way. Dear, I take the opportunity to speak to you directly this regarding maybe questions, but we will, I will ask for questions afterwards. Paul Andre, you know that the street last you all constructed for the scholars being in a field, which, as you mentioned, the vector spaces encounters problems, even when the scholars form, form division, form a domain, ring without zero divisors. But I have been aware of paper by post P. Oh, yeah. Stay. You know it, maybe. Yes. So I don't have to send you. Nobody. So, so I, okay, I tried to adapt this construction to a situation where I mean some, some shift, like, pre shift, so it construction where I changed the base ring commutative ring. And so I needed to, to generalize this. Yes, to. So I use, but it's very categorical. Yes. And, and the question is, we are not, we'd like to understand better the combinatorics behind. And that's what I mean. Yes. So I mean, for, for, for very, you know, kind of general reasons, there exists such such a co free commutative common rate for like any commit commutative ring, but it's not clear why I mean, no, what I find fascinating is that you died all this connection with with with your work and differentiation. I think that I would need to understand better. And so I just wanted to mention this. We can interact in a way. Yeah, of course, I would, I would love to. Other questions. Please. Sorry if I missed it. But why exactly do you need to find a dual here? Do you need it to define exclamation mark mark a or do you need to dualize it? It's about this. So I mean, when you get to, when you want to work with So, okay, so what happened, okay, I will. So what happened is traditional models of, because it has to do with linear logic. So what happens with traditional models of linear logic is that, in fact, we are able to build using topological, you know, vector spaces or this kind of things were able to define the co free commutative common rate by some kind of variation on the general, I mean, symmetric algebra construction. So, and so we get something like, you know, powers, I mean, tensile powers of a to the end. We see, we see metrized it we do some, some clever, you know, limit construction is not anymore some and we get something when we do realize it, this gives the co free commutative common rate. In the case of vector spaces like you know with no topology, there is this construction which I find extremely, I mean, mysterious, where you use the fact that every co algebra induces an algebra structure on the dual. And then you do some kind of clever, clever restriction of the under double double on the by dual, so that you get the co free commutative common rate I'm not sure it answers your question but I just wanted to to say that to me, I kind of understand it by honestly I don't understand it I mean I understand it from the outside, but I don't have a completely clear combinatorial. And this is what I hope I understand I will, I will get from this kind of work by Farah and Christian. Sorry, sorry, I, I, we could discuss offline and I will be happy but thank you very much. Thanks for watching 1330. Thank you.
 Well, I'm very grateful for this invitation to speak a little bit about this connection  between proofs and nuts.  And I think there is a lot to explore still, so I will just explain a little bit the basic  ideas.  And I love this picture that summarizes the talk.  So it's about how a proof can be seen as some kind of naughty structure which has to  do with the structure of dialogue.  And so it's a long question about what is a logical proof, how should we should represent  it, describe it, and how we could have a properly mathematical notation for proofs.  And my starting point in this talk is the idea of game semantics.  So the idea is that every proof of a formula A initiates a dialogue where proponent tries  to convince opponent and opponent tries to refute proponent.  And this is really a nice interactive understanding of proofs.  And so here is a typical proof in, let's say, some kind of Genson notation, traditional  notation.  It's a little bit cryptic, a bit difficult to understand what's behind.  So, but what it proves is so-called drinkers formula, which says that in any open café  in Paris, with at least, so we need one drink, I mean one customer, so in the café, so there  exists a specific customer Y, which is so sober, it's very sober customer Y, such that  if A of Y, which means that Y is drinking, then all the other customers in the café  are also drinking.  And clearly this is counter-intuitive, but this is proved by this short proof in classical  logic.  Okay, this property is not true, is not valid in intuitionistic logic or constructive logic,  but it is valid in classical logic.  And here is the proof.  And I said that a proof gives a strategy, some interactive strategy to convince you.  So we could, I mean, I could play it with you.  So okay, imagine I want to convince you of this property, which you think is a little  bit strange.  Well, we open, I mean, we enter together in the café.  And then I say, okay, I know the customer was, I mean, was very sober, so I could pick  someone.  So for instance, I don't know, Gerard, if you allow me, I would say, okay, Gerard, you're  very sober.  So I know that, okay, if ever you drink, everybody else will be drinking in the café.  And then the point is, well, I may be wrong.  Okay.  So you may be drinking Gerard, but then someone else in the café is not drinking.  And so my opponent will refute me and say, come on, Paul, you're just wrong.  This customer, so I don't know, Nicolas, you're allowed to be, you know, the counter-witness.  So okay, say, okay, come on.  You know, here, I see Nicolas is not, I mean, he's not, so he's a counter-example to your  claim.  And so the proof what he does interactively is to allow me to backtrack.  And so this is a little bit hidden here in the fact that there is two existential here  introductions in the rules.  It allows me as, you know, prover to backtrack and say, oh, sorry, I was wrong.  I shouldn't have picked, you know, Gerard at the beginning, I should have picked Nicolas.  Okay.  And so the idea is that the fact, I mean, the reason why the existential here is not constructive.  Okay.  It has to do with the fact that I did use the witness from the interaction I have with  the, with the opponent.  Okay.  So in a way, I cheat.  Okay.  But this is exactly the way classical logic works interactively.  And I mean, you can, you know, instead of speaking about the drinker formula, you can  say that this formula says that every, every, you know, proposition is either true or as  a counter-example.  I mean, you can think of the way here as a counter-example.  And of, I mean, and clearly, you know, before a property is proved, well, this, still this  property holds because if someone finds a counter-example, then we have the counter-example.  I mean, this is the same story I've told you here.  Okay.  And so in a way, this syntax is a little bit, you know, difficult to understand while the  game semantics gives a more, much more intuitive understanding of it.  And so let me speak briefly about, you know, the way, you know, game semantics and algebra  are connected.  So this is through linear logic and a number of connectives, which in fact are really adapted  or are really consistent with linear, linear algebra.  Okay.  And so here we have negation, which is really like a dual in, and I will come back to that  in linear algebra between the game A played by, you know, the player and the game, not  a same game, but played now seen from the point of view of the opponent.  And so negation peruse the whole of opponent and proponent.  The sum here is what it does.  It says, okay, let's start with two games.  So there is a game A and a game B, there are some.  So imagine this is chess and poker, for instance.  Okay.  So some of the game is the game where I as a player decides whether I want to play chess  or I want to play poker.  And then once he's decided, we carry on.  We never come back to the other board.  Okay.  And so this is understood as here is this, this junction.  Okay.  It's a choice I do as a player, but there is a dual connective, which is just the same,  but where opponent makes the choice.  And this is understood has a form of conjunction because if I let the opponent, you know, the  environment choose, then clearly I should be a master in chess, but also a master in poker  if I want to, to, you know, win the game, because I don't know what the opponent will  choose.  And so this is really some, a notion of constructive, you know, conjunction.  It's an ant.  Okay.  So this is a little symbol used for ant.  But there is also a tensor product where the two games are played in parallel, but only  opponent is allowed to switchboard.  Okay.  And so player will just play where opponent has just played.  And this is understood as a classical conjunction when I say classical, I mean, in the sense  of classical logic.  And there is a dual where it's same, but now player is allowed to switchboard.  Okay, and the nice thing is that this is can be understood as a form of classical disjunction.  And so I will show you how to establish the fact that for every formula, so for every game.  So here, for instance, let's, let's take a data mind, you know, version of chess.  Well, we have the property that a, let's call it the chess is called property a, or here,  not a.  Remember, it's just you swap the board.  And so I will give you an interactive strategy which wins in that game.  And so really the idea is that we are playing, I mean, I am playing two boards here in parallel  and here in front of me, there is a tensor product and the tensor product can be seen  of a strategy or counter strategy of type tensor can be seen as a pair of strategies.  So let's say I'm playing against two, you know, famous Russian chess masters.  And I will show you how I can win by playing here white and here playing black.  Okay.  And of course, I mean, winning, you know, I'm not crazy.  I cannot win against both.  Or if I want to win against both, I need to be a very strong master myself.  But here is by pure logic.  So there is no, I mean, it's just by some kind of logical, let's say manipulations  or logical, you know, truth.  Okay.  So I want to prove that a or not a and the strategy to do that is just to let it's very  simple and it's like cheating really.  So it's to let course noise start here.  And so course noise plays a move like this or here.  And then copycat what course noise has done on this board.  And I can do that because as because this connective, you know, enables me to play,  I mean, to switch board when because whenever a move has been playing on one board, I'm  allowed to move to the other board like this.  Okay.  And so I've copycat the move by course noise, carp of answers.  And then I move to the other board and I play like carp of.  Okay.  And then course noise answers and then I just move like course noise has just moved.  And in that way, I just by copy, you know, some kind of copycat strategy.  I mean, carp of really believes is playing against course noise and course noise is really  believes is playing against carp of and in the end, one of the two wins.  And so that means that I will lose maybe carp of wins.  So I lose on this board, but I win on this board.  And after I want to prove that they are not a.  And so that means that I only need to win on one of the two boards.  Okay.  So the idea is that we that, you know, we can understand, you know, the fact that the  properties through or its negation, something purely interactive and purely linguistic,  which doesn't have to do with the, you know, outside world.  It's not about whether today it's, you know, cold or hot weather.  It's really about just pure linguistic phenomena.  Okay.  And so I mentioned that there is also this exponential modality, which is very nice.  I will not speak about it anymore in this talk, but it's nice to know that there is  something which enables opponent to reopen to reopen balls whenever the opponent is  embarrassed.  And this is what happened in the drinker formula thing.  At some point I was embarrassed as a player.  So I reopened a new board and I won on the new board on the second board using information  I knew from the first, the fact that I mean, Nicola was the good witness and not Gerard.  Okay.  So this I learned on the first board and then I use this information on the second board.  And so, and by the way, this, I mean, maybe I will have the time to mention it, but this  has to do with co free constructions of co-algebras or commutative co-algebras in vector spaces.  And okay, I try to come back to this, but now what I will try to show you is that there  are connections between these ideas of, you know, game semantics and ideas coming from  linear algebra and representation theory.  So okay, I will, I will move that.  Okay.  And so, but before I do that, there is this important, let's say tool coming from categories  and ideas by Lombak in particular, which is to give a factorial approach to proof invariance  in the same way that we will see there is a functional approach to not invariance.  Okay.  So, so I will speak about the, in particular, I will start from this idea coming from Brewer,  Haytman, Kolmogorov, that a proof of a conjunction.  Okay.  So, there really is a pair consisting of a proof of a and a proof of B. Okay.  So, and the idea is that, I mean, from the game semantics point of view is that someone,  you know, if I claim a and B, my environment, my opponent could attack me on a or on B.  So I need to be able to prove a and to prove B. So I should have a proof of a and a proof  of B.  Okay.  So this is fine.  And we will see that this will be interpreted by the existence of a Cartesian product in  categories.  But then there is this more mysterious description of a proof of a formula from A to B in logic  as an algorithm, which is able to turn any proof of A, Phi, into a proof of B. Psi of  Phi.  So this algorithm Phi, the question is what does, I mean, what does it mean, an algorithm?  And this was, I mean, this is still a question that people, I mean, it's not so clear.  Whereas here it's quite clear what it means.  Okay.  A pair is a pair.  But an algorithm is something like saying, okay, I have a notion of algorithm somewhere  in the air, but I don't know exactly what it means.  And so the notion of Cartesian close category is an attempt to answer that question by saying,  come on.  Okay, an algorithm will be a map in a specific category.  But this category should be Cartesian.  So it should have a Cartesian product.  And it should be closed in the sense that we should have a family of adjunctions between  the function A times and the function A implies.  And what this means is that we have a natural bijection between the set of maps from A times  B to C and the set of maps from B to A implies C.  And we can think of this as some kind of implication.  So clearly a basic example is the category of sets and functions.  Okay, but there are many, many other examples.  And we spend a lot of time, you know, when we study proofs to construct Cartesian close  categories of many shapes.  Okay.  And so, I mean, just, I mean, a typical example is every topos is such, you know, every, every,  every category of shapes is such.  And there are many, many other examples that we can analyze.  It's a very rich and interesting topic.  But here I want to focus on the free construction.  Okay.  And so, and you will see it's very symbolic.  And so if you want to say, okay, I know I start from a category.  Now I want to construct the free Cartesian close category.  And you think about it, you say, okay, I should start by the objects and the objects, they  should be constructed from the objects of the original category.  And then the products and the implications.  Okay.  So there should be this grammar of objects.  And so the objects of the category of the free Cartesian close category are constructed  by this grammar.  Okay.  So you can think of them as formulas or as types constructed by this, this, this very  simple grammar with Cartesian product and implication.  And here, again, Cartesian product is some, you can understand it as some kind of conjunction  and implication here.  Okay.  And so the, the, the, now the morphisms in this category, they are not as, I mean, there  are a bit subtle to define, to describe.  And I will just say a word about them.  So they are lambda terms.  And so just to say a little bit, you know, a word about lambda terms.  So lambda, lambda terms are terms in a calculus, which is a pure calculus of functions.  Okay.  And I will say a word on that now more.  But then these terms of this calculus should be considered modulo some, some notion of  beta, eta conversion.  And what I claim here is that the situation is very similar to what we have in nut theory,  where we have like this tango diagrams.  Okay.  And then up to deformation of diagrams.  Okay.  Typically, write the master moves.  So, so how is the lambda calculus defined?  I mean, there is some kind of, I mean, some kind of calculus where you describe functions  in a given context.  So typically you said that there is, for instance, a function x.  Okay.  This is just a variable in a context where x is of type a, and then x will be here.  This term will be of type a.  And the most important two rules is the abstraction rule, which says that if you have a term p  of type b, okay, in a given context where the variable has been declared of type a,  then you will construct the function, which is written lambda x dot p.  And the function here, you can think of it as the function which to x associates p of  x.  And so this is the notation here.  And this type is the type of functions from a to b.  And so I said implication, but you can also think of it as description of some kind of  function, function space.  Okay.  All the functions from a to b.  Okay.  And since the variable here is of type a, and the output is of type b, then lambda x  dot x, this function is of type from, I mean, a implies b.  And once we have constructed such a function from a to b, we can apply it to an argument.  So this is the notation.  So p is applied to the argument to get something of type b.  So the argument is of type a, applied, I mean, we apply the function of type a implies b,  or a to b, and then we get something.  And then there are three basic rules here that organize, I mean, that deal with the context.  And so then what are the beta and eta rules?  So they're very cute rules.  I mean, they are very beautiful and powerful.  So the first one says, okay, if I have constructed the function, which to x associates p of x,  and then I apply it to an argument, then I will get, I mean, I can rewrite it into the  same, I mean, the p, but now it's p of q.  And this is the way it's written here.  So because it's a pure calculus of functions, we have variables x appearing in p.  And so we can then substitute them by q.  Okay, similarly here, there is a rule which says that every term of this calculus can be  seen as a function lambda x, which to x associates the term applied to the argument x.  Okay.  And this is completely formal, completely symbolic.  But at the same time, it's known to be deeply connected to a language, I mean, a language  of proofs.  And so this lambda terms here, this lambda terms in red, they can be seen as proofs of  some propositions which are written with implication here and conjunction.  So there were these, you know, little logic calculus here of, which you can see, think  also as a calculus of formulas and here, this is the description of the proofs of these  formulas.  But what is important, I mean, okay, I don't ask you to understand all these details about  proofs and formulas.  But what I want to stress is that there is a completely algebraic construction of the  free Cartesian closed category.  And what this means is that whenever I take a category C here, and I have a functor into  a Cartesian closed category D, I can lift this functor to the because this is Cartesian  closed, I can lift this functor from C to D to a functor which preserves up to coherent  isomorphism Cartesian product and the implication arrow, okay, from this free Cartesian closed  category into D.  And so this gives, so this construction is extremely important in the construction of  what we call proof invariance.  And I mean, you know, I work in a, in a, in a like computer science lab.  And the reason is that in fact, this lambda calculus can be seen also as a language of  programs.  So there is a nice correspondence between proofs here and programs.  So you can think of it as a very simple programming language here.  If you like that you transport, you interpret all the, so the morphisms are programs and  you interpret them into some category.  And so here, the category typically will be, could be a category like the category of  sets and functions could be a, you know, a pre-shift, a pre-shift or a shift category  or a topos or whatever.  As long as it is Cartesian closed category, we have this beautiful little functor, okay.  And the, okay, this is the story for, for, you know, what, what, what I would do, you  know, all my day, okay, constructed this kind of things.  But then people in, I mean, studying not invariance, and this is the connection with, with nuts,  they do something extremely similar where instead of constructing, so, so they start  from the functors, let's say, I mean, it's one way to think about.  The construction of nut invariance, there are many ways to construct nut invariance,  but here I will describe the functorial approach, which is to say, okay, if I'm able to, to,  to associate to every color, you know, an interpretation in a ribbon category, and I  will explain briefly how to construct such ribbon categories using representation theory  of quantum groups.  So when we have such a ribbon category and a functor into, into that, we can leave the  functor to a functor which preserves the structure of ribbon categories.  But this, I mean, this free ribbon category is a, is a category where the morphisms are  frame tangles.  So in particular, we can study like ribbon nuts and we can associate invariance to each  ribbon nut because this category is, is, is typically the morphisms from the unit object  to, to, to itself are, are ribbon, I mean, ribbon diagrams which are closed and so they  are, they are really like ribbon nuts.  And so you see there is this very, I mean, kind of fascinating analogy between what we  do with proofs in the functorial semantics of proofs and the functorial, you know, invariance  of, of nuts.  And so I will try to explain the connection.  So I will go very briefly just to explain this ribbon categories on string diagrams.  So it's a notation for monoidal categories.  So the idea is that a morphism from A tensor B tensor C to D tensor E will be described  as some diagram with three inputs and two outputs.  Okay.  So ABC here as input and DE as output.  So, so the flow, I mean, goes in that direction from, from the bottom to top.  Okay.  So this is the arrow here.  And so composition is described by vertical composition.  So the composition in the category and the tensor product as horizontal, I mean, putting  side by side F and G.  So typically here is an example where F tensor identity.  So F here identity here and then F tensor identity composed with identity tensor J.  Okay.  So, I mean, if you, I mean, if you interpret this morphism here in the string diagram notation,  you get this picture, but then if you interpret this other morphism, you get this picture  where you see here F and G have been kind of, I mean, we play with the order in which  they appear here.  And the point is that in a, in a monoidal category, these two morphisms are equal.  So really we can be, I mean, we can trust our eyes up to the formation of diagrams.  And indeed this diagram here and this diagram here describe the same morphism.  Okay.  And this is really the beginning of a beautiful story where you try to make, you know, this  topological intuition valid up to the point where you can say, okay, I have a nut and  I described as a morphism in a specific category.  And the morphism is invariant up to deformation.  Okay.  So this is what I will explain now.  Okay.  So a braided category or monoidal category is just a monoidal category equipped with  a braiding.  So it's a family of isomorphisms from A tensor B to B tensor A. So, and this is the way I  will draw them.  Okay.  I think many people here know this, all the story, but I felt that it's good to tell  it again anyway.  So this is the way the braiding is described, but of course there is an inverse which is  described as a negative braiding whereas here it's a positive braiding.  And our coherence diagrams.  So this one, for instance, says that these two sequences of arrows are equal in the braided  monoidal category.  And diagrammatically it says this, okay, that if we permute A with B tensor C is the same  as permuting A with B and then permuting A with C.  Okay.  Another diagram which is essentially saying the same, but for the other configuration.  And so this is like braided monoidal category, but then we can define, and I will be very  much interested in the notion of balanced monoidal category.  So it's just a braided monoidal category with a twist, which is defined as a family of isomorphisms  and which I will depict as a twist like this.  Okay.  So there is a little like we twist the ribbon and this is why I work with ribbons rather  than just strings.  Okay.  So we can see this little action here on the ribbon.  And so it should satisfy that theta i equals the identity.  So when we twist the unit, we just do nothing and then this very nice equation, we say that  when we twist the tensor, so when we twist the tensor, it's the same as braiding, twisting,  braiding.  Okay.  And so this is the way to sit.  So if you want, so A tensor B is really A and B in parallel.  So if you twist A tensor B, this is what you get.  You need to twist A and B independently, but also braids them twice.  Okay.  So you see this is a typical example where purely algebraic, you know, coherence property,  which says that this map should be equal to this sequence of three maps, coincides with  a very topological intuition about how we twist ribbons.  Okay.  And so now I carry on, you know, what I'm trying to do now is really to build what I  will call a ribbon category.  So we have, we need a notion of duality.  So a dual pair between an object and A and an object B, where we say that A is left  dual to B, is defined as a pair of morphisms.  So one morphism from the unit object to A tensor B, and the other morphism from B tensor  A to the unit.  So you can think of it as some kind of identity here that we are building.  And here are some evaluations.  So this is sometimes called co-evaluation map and evaluation map.  Okay.  So typically we have that when A, imagine that A is a finite dimensional vector space  and this is B is the vector space of its, I mean, it's dual vector space of forms.  Okay.  So like this is V and V star.  Okay.  And so we ask that these equations are the exact equalities are satisfied, okay, which  are represented like this.  And we said that, yes, so in that case, we said that A is the right dual of B.  And yes.  So anyway, a ribbon category is simply defined now as a balance category.  So if you remember, it means braiding, twisting, okay.  But moreover, every object A has a right dual.  And there is this further requirement that when I take A star tensor A and I twist A  and then I evaluate, so I get this map from A star tensor A into I, or I twist A star and  then I evaluate, I should get the same.  Okay.  And the nice thing is that once we, I mean, in any ribbon category, the object A star  is also left dual to A. And so you can use the twisting and the braiding to build, I  mean, a unit, so a co-evaluation map and an evaluation map, but where you see A star is  on the right now.  Okay.  Oh, yes, so here.  So A star is not anymore just a right dual, it's also a left dual, thanks to this structure  of twist and this equation.  Okay.  And so in particular, we have this nice equation satisfied in every ribbon category.  That twisting is the same as braiding and then doing this, you know, playing between  the here, co-evaluation and co-evaluation, but this is the original evaluation and then  this is the one that we deduce from the twist.  But we can also define the twist from that fact that A star is at the same time a right  dual and a left dual of A. Okay.  And I will come back to that later because we see the similar phenomena appearing in  logic and I claim that this is of course topology, but in fact, and this is really the purpose  of, you know, I mean, my work, but also this talk, okay, is to show that this kind of phenomena  can also, I mean, it's interesting to look at them from a logical point of view.  And there are some kind of maybe projections of some more, I mean, like let's say, people  say purely logical structures about negations.  Okay.  Because of course, when I say duality, I have in mind some kind of negations and we will  see that these dualities can be seen as particular instances, extremely interesting and rich,  but instances of a more general pattern where negation is not involutive anymore.  So something important here in this ribbon category is that when we dualize twice an  object, we come back to the original object, which is true for instance for finite dimensional  vector spaces, or we see representations, which is not true anymore for general vector  spaces because typically the map from V to V is double negation or is by dual is not  an isomorphism.  And so, I mean, what we see here, this phenomena, okay, I mean, this kind of very nice, typically  here reconstruction of the, I mean, the twist here from dualities.  So you know, these equations can be also played and I will come back to that as a logical  level and I will explain how to do that.  Okay, anyway, we have this free ribbon category.  So there is this beautiful theorem by Schum, which says that the free ribbon category can  be constructed and it has, okay, so it's a free ribbon category generated by a given  category.  So the objects are sine sequences of objects of C. So sine means that epsilon 1, epsilon  k are plus or minus to indicate the direction of the links.  And the morphisms are frame tangles.  So frame tangles means they are ribbon, you can draw them with ribbons with links labeled  by maps in C. So this is a typical example.  So this is a map from A plus to B plus C minus D plus.  And so you see A plus, this is the input.  So the map goes in that direction and the output is B plus, I mean, I could say B plus  tensor C minus tensor D plus and the C minus here, the minus means that the flow of, you  know, of the computation goes in that direction.  Okay, so this is typically a map in this free ribbon category.  Okay, and so clearly I want to, you remember that in the free Cartesian close category,  the maps were proofs, they were lambda terms, they were very symbolic objects, whereas here  is purely topological.  And so my purpose in the next 15 minutes is to show you that there is a way to think  about lambda terms, at least in good situations where the lambda terms are linear.  I will explain that.  Okay, and you can think of this, you know, in connection to the next talk by Noam Zeilberger.  So when the lambda terms are linear, then we get a very, I mean, slightly mysterious,  but also very natural, I mean, the two connections between proofs and nuts.  And so as I was saying, okay, this category here for the free ribbon category, as this  beautiful property that defines the free ribbon category.  So every time we have a category with breading, twists, and good dualities, we can take any  functor from C to D. So here, really, you should think of this functor as giving an  interpretation to each of the links here.  Okay, so we give an interpretation to each of the links.  And then just from the fact that this category is ribbon, we can lift this functor to a functor  where the tangles, of course, it's very important here, the frame tangles, but in the topological  sense, okay, so really, modulo deformation, if you like, are interpreted as morphisms  of this category.  And it's a way to construct many invariance of nuts in topology.  And so I will try to explain how this can be adapted, but maybe before that, I will say,  I mean, I think it's nice, especially here, to spend maybe five minutes explaining how  we construct such ribbon categories, okay, before I move back to proof, because I want  to show also that the fact that I look at proof has to do with finite dimensional versus  like, possibly infinite dimensional representations of quantum groups.  So the idea is that one way to construct these ribbon categories is to define them as categories  of modules of half algebras.  So suppose given like a symmetric monoidal category V, so you can, for instance, take  the category of vector spaces over a field, okay.  So bi algebra is an object H of the category V, equipped with a multiplication and a co-multiplication.  So I use this diagram here for blue for multiplication.  Remember, I always draw, oops, sorry.  I go from below to top.  So this is multiplication of H and unit and co-multiplication and co-unit.  And we should ask these equations so that you know, okay, so typically this is the bi-algebra  equation, which says that multiplication and co-multiplication are compatible in this way,  okay, and then similarly for, I mean, unit and co-multiplication, multiplication and co-unit  and unit and co-unit.  Then an antipode is defined as the morphism from H to H, which satisfies these two equations.  And whenever we have such, okay, so half algebra, which is a bi-algebra equipped with an antipode,  then we can construct a monoidal closed category of left modules where the action on the home,  the internal home, is defined by this formula.  So I wrote it in the Swidler style, okay, and this generalizes the usual construction  for groups, okay, where, so you can think of your half algebra as a group and then what  you're asking, I mean, here, this says that you should multiply each input by the inverse  of H, apply the function and then multiply by H.  And so this is just the quantum group version, but there is the diagrammatic representation  of it, okay, that I can just show you here.  So that means that this object, the right negation, has, I mean, is an H module, okay.  Similarly, there is also a way when the antipode is reversible to define a closure on the left,  okay.  And so similarly, except that we need to use this inverse of the antipode and we'll get  the good properties, required properties.  So this is a way to get, you know, this implication here.  I mean, so what we get is a monoidal closed category on the two sides, left and right.  But now maybe we want that to have also a braided monoidal category.  So for that purpose, we introduce a notion of braiding on the Hopf algebra, which is  in fact a vector of H tensor H, which satisfies a number of properties which can be represented  diagrammatically like this.  And now the important point here is that every braiding, okay, induces a braiding, so a braiding  on the Hopf algebra induces a braiding on the category of left H modules, okay.  And the idea is that you just take V, I mean, like a vector, like V tensor W, you swap W  and V and you apply your, I mean, you multiply the braiding, okay, of your Hopf algebra at  the same time as you permute the vectors V and W.  Okay, so then what we get from that is a way to relate the, let's say, right negation  with the left negation.  And this is extremely important from my angle, like logical angle, because it's really saying  that this braiding will induce a map from the left negation or right negation to the  left negation, and that this can be understood in a very logical way, as I will explain.  And this map, in fact, can be, I mean, if we compute it, this map, what it does, it  associates to any form here, this form where we pre-compose the form with an action of  U, and U is equal to this vector here and can be represented in this way, okay.  And this is an extremely important vector in the theory of quantum groups.  The thing is that it's, as a bad property, that it's not a group-like element.  So in order to obtain a group-like element in the Hopf algebra, the very natural way  is to define a twist.  So this is where we get back to ribbons, which is just a vector of H satisfying these equations  that I drew here diagrammatically.  And then when you multiply the U with this twist, or its inverse, well, suddenly you  get a group-like element.  And there is an element of magic in this thing.  This is something I try to understand, let's say, from the outside, looking at, let's say,  braided monoidal categories and so on.  And the reason why it's very important is that, in fact, it's related to this, I mean,  all the work here that I'm describing was really developed by Rechetikin and Turayev  in the 90s.  And they're really the fundamental observation is that if we take the finite dimensional  modules, this defines a ribbon category.  So if I go back to my little picture before, sorry for that, but here I have this category  of finite dimensional representations of my Hopf algebra with structure.  So I can interpret ribbons as morphisms between such representations.  And then using that, we can construct invariance of the ribbons.  So it's a beautiful recipe.  And I try to think about what I mean, its logical meaning.  And so to that purpose, I will introduce the notion of dialogue category.  So ribbon is about ribbons, and since I want to speak about dialogue games, I found it's  nice to call my categories like dialogue categories.  But you will see they're extremely stupid categories.  I mean, the way they are defined is absolutely obvious.  So the important thing here is the connection with games and mnemonics, the thing I was  telling you before and the idea that there are proofs are based on interactions.  And so the dialogue category is just defined as a category with an object button and a  natural bijection.  So we ask that there is a way to turn any map from A to B to this object, which I will  call bottom.  And you can think of it, for instance, as the base field, into a map from B into A implies  bottom.  So this is a very familiar situation in linear algebra.  So we can do that on the left or on the right.  And this is just a definition of a dialogue category.  So it's very stupid and primitive.  The important thing is that then we can look at, introduce the notion of pivotal dialogue  category, which is a category where we can play with the inputs of forms.  So whenever I have a map from A to B to bottom, I can turn it into a map from B to bottom.  And this is the way I like to represent that.  So it's going like this.  And then when asked the coherence diagram, which says that if I turn A and then turn  B, it should be the same as turning A to B. And this can be understood as some kind of  coherence properties of a map between the two negations that is here, the coherence  property is here.  But what is important here is that we get from this, I mean, a notion of dialogue category  with, you know, so, okay, so this was a pivotal dialogue category, but we could also say,  okay, I will define a balanced dialogue category just as a dialogue category with these two  negations, a braiding and a twist.  And the important property is that every balanced dialogue category is defined as a pivotal  category.  And what is, I mean, an important observation is that we really need the twist to do that.  So the idea is that whenever I have a map from A to B to bottom, I can pre-compose it  with braiding, but also with a twist on A here.  And really the intuition is that the, I mean, this operation of wheel I was describing here  can be described at the same time as a, I mean, you see here is there is a twist and  a braiding.  So the braiding would not be sufficient.  And this is the same, I mean, this is really related to what happens with HOPF algebra.  So in the case of HOPF algebra, if you remember, we needed a little tita to make, to construct  a group-like element in H. And here it's the same story that, I mean, in that, okay, I  mean, when we have a good ribbon of algebra, in fact, the category of general representations,  so finite dimensional and infinite dimensional, defines such a balanced dialogue category.  Okay.  And now from this structure, so in particular, I mean, so it satisfies this pivotal coherence  property.  And from that, what we get is that when bottom is the unit object of this dialogue category,  then that the finite dimensional H modules define a ribbon category.  So before what's, I mean, it was, I mean, here it can be deduced from a purely, I mean,  a purely categorical and formal way that we have this property.  So I will, so I don't have too much time, so I will just show you a little connection  between proofs and nots that makes it even more meaningful.  So the observation is that, you know, in a ribbon category, every object bottom, in fact,  defines left and the right negation where whenever you dualize the object, you tensor  it with this bottom.  Okay.  And so now in the same way as we constructed the free Cartesian close category, we can  construct the free balance dialogue category.  So I will show you the way it's constructed is very similar as the construction for free  Cartesian close category.  So it's just the objects are, let's say formulas constructed with a tonsure product, left negation  and right negation.  And then the maps are proofs.  Okay.  And so proofs of a logic that I call tensor your logic because it has to do with tensor  your algebra.  And the proofs are constructed exactly in the same way, you know, using the same, let's  say Gensen like, you know, Gensen like constructions of proofs.  But there is of course a little care about so called exchange rule.  So a logic.  Okay.  So we need to care a little bit because this, this is really about, I mean, we're manipulating  the hypothesis of a proof and so we manipulate them with nuts and rebounds.  So we need to have a little bit of information about that.  But this can be very nicely done using, I mean, the traditional proof theory is just a very  basic adaptation of it.  And from that we get the free dialogue category with a ribbon structure.  Now we know that every time we have a ribbon category and we fix an object bottom, this  defines a dialogue category here.  So where we have, you know, two negations on the left and on the right.  And so just because it's the free dialogue category, we can construct this functor and  the main theorem and I will stop here is that the functor is faithful.  Okay.  And so what this means is that two proofs here in this logic, I mean, this is the world  of logic, this is the world of topology, two proofs are equal in this category.  If and only if the underlying ribbon structure is the same.  And so I will just show you an application of that because this can be seen as a coherence  theorem for dialogue categories.  So imagine I take a an object in the dialogue category and I map it here to its double negation  and this map is not involutive.  Things for instance, you know, you're working in the category of general representations  of quantum group.  So this is not, I mean, this is not invertible.  And then we can also take this other negation to where we take the left and right negation  and we change the order.  Then we can apply, you know, the two turns here enables to connect these two negations  to these two negations.  And the point is that we don't, I mean, if we do that, it's not equal to this one, we  need to twist also the output and to see why.  In fact, so this commutative diagram, I mean, imagine we want to prove that is commutative  in any dialogue category.  And so we need only to prove that it's commutative in the free dialogue category.  And how do we do, well, we construct, we see the two maps as proofs.  Okay, so there are the two maps.  This is, this one is here and this composition is here.  And then we look at their images through this, oops, through this factor here.  And the images are just tangles.  Okay.  And the tangles, what they do, they follow, they track the manipulations we do on the  formulas and in particular on this bottom.  So they track the bottoms.  And then the two tangles here are equal and we know that the proofs are equal.  Yes.  So I'm, I mean, I could speak more, but I think I'm finished with time.  Yes.  Maybe you could leave some time for questions.  Maybe I should just say one word that these tangles here, what they represent, and maybe  I will just show you this picture.  Okay.  What they represent is the flow of negations in the dialogue between the open and the player.  So if you remember at the very beginning, we had this interaction between the prover  and the refutation.  And in fact, these tangles here, we, they can be also understood as little stretch,  but they are not very good.  So we have these two strategies where opponent ask a question or maybe I could play here.  Opponent ask a question and then the player answers here.  Yeah.  And so there is this interesting relationship that I think would be, I mean, it's worth  exploring more between proofs and topology.  Thank you very much.  Yeah.  Thank you very much, Paul-André.  I'm not sure we can hear you.  At least I cannot.  Yes.  Cannot.  Do you hear me, Paul-André?  I can hear you.  Okay.  Good.  Does anybody hear me?  Yes.  Sorry.  It was my fault.  No, no, it is because now you are on the dialogue mode.  Yeah.  But I realized that during all that talk, I had the sound off.  I didn't realize that.  So if you wanted to stop me, I was like, you know, a raging bull.  I don't know.  Okay.  So are there questions?  Actually, I have a question.  It's Maxim.  Can you say it?  Yes.  I got lost a bit when we discuss this, all this branding.  Do you introduce because there's so much literature that's kind of polluted by  brandings or it's really in this dialogue, things that you don't introduce  branding by hand and it appears by itself?  Ah, well, the thing is, there is this dream we have to understand the topology of  proof.  Yes.  So in the traditional, you know, logic, we have this so-called exchange rule.  So where we need, I mean, clearly when we describe this comes from Genson, it's an  old tradition, we need to permute the hypothesis in a proof.  So, and so the thing is usually we don't track, we don't track the permutations.  Okay.  We say it's a symmetry, but then it makes sense to say that whenever we have such a  So it's kind of generalization by national grade.  But I would not say, I mean, yeah, it's generalization, but I would say it's a more refined picture  because this can be done, but now we track, we remember.  And so now in the proofs, so, okay, so typically just to show you a proof, we will remember  the permutations.  Traditionally, we don't because we don't care.  But now because we track them, we can get this free construction, which is, which has  the, it's some kind of grammar, like a categorical grammar for infinite dimensional vector spaces  with braiding.  So I mean, and so the braiding is produced by the by the HOPF algebra action.  And that's the idea.  Yeah.  Maybe I just want to give you a comment if you, because it's braiding seems to be it's kind  of bit artificial, like fashion instance.  Yeah.  But if you can see just notion of by algebra, yeah, without anti-port unit to unit just  very simple product and coproduct and look how many, this is a basis of map from N spiral  to M spiral.  Yeah, of course, there's some kind of normal form, but intrinsically there are also some  three dimensional manifolds, some colorings.  Yeah.  So it's even without braiding one can see three dimensional picture.  Yeah.  So that's, that's, that's, yeah, indeed.  And maybe, okay, you know, really all this work started from this more, I mean, you know,  no, I mean, unbridled, but, but where, where I manipulate trees.  So I, I agree.  I mean, but what I wanted to show is that this phenomena that I agree with you there.  I mean, there, there appear and it's there a bit questionable.  Okay.  What are they doing that in fact, from there, they have, they have some kind of, they can  be understood at a logical level.  That's what I mean before.  Because the thing is when we look at ribbons diagrams, we see a lot of phenomena and it's  difficult to understand what is really coming from the topology and what is coming from  the fact that we can negate and we can turn things.  And so the story that I want to tell.  So for instance, I mean, just to say very briefly, this thing which I mean, which would  have emerged anyway in proof theory without we did not read.  So this operation that I was describing here of permuting, you know, to, I mean, by, by  doing this kind of operation of, of, of, you know, if we think of a problem, you know,  if we think of a proof as something very concrete, not, not something, you know, in the air, but  something that people manipulate in space and time, you know, like, like we discussed,  then we see that, that this operation is very natural.  And then we see that the twist appears here.  So, so there is this, I would say, surprising and slightly, I mean, we want to understand  it's not, okay, this, this connections and maybe just, yeah, that's, that's, but I,  I agree.  And I would need, you know, I think we need many faults.  I mean, at some point to avoid maybe these breading.  My suggestions through to avoid breading make something simply.  And in other things, it is all these games also relate to logic and some different way  when you consider the statement is which sequences for any, for any, for any, it's like a game.  Yeah.  Yes, with the exist, but it's, yes, so maybe I should mention very briefly, I mean, just  this last, there is something that I wanted to say that there is an interesting open problem.  I mentioned the exponential modality, which you can think of, of it as a co free commutative  common, okay, generated by, you know, and I, for the moment, I mean, so recently, not,  not, not very long ago.  Like, I mean, people like Daniel Murphy have, have, you know, studied this construction  in, in the category of vector spaces.  So, and so it, in fact, I mean, I have shown that it's connected to, you know, three less  finite dual construction that, you know, this is one, I mean, I mean, this, this construction  is far, I mean, far, far from obvious for me.  I would be interested to see how this construction, which we know now on vector spaces could be  lifted to representations.  Maybe it exists, but I don't know it.  And this is the kind of things I like to discuss with Gerard and the connection with automata  theory here.  And I, you know, all the story I've, I've told was about linear.  So let's say arguments where we cannot repeat hypothesis.  And so in the case of the drinker formula, the point is that we can, we can construct a co free, I  mean, the algebraically, the story is explained like this, that we can construct a co free commutative  communoid above the existential.  So we have the existential.  And this is what enables us to backtrack and change the witness.  So if you remember the first time I was taking the Gerard as an existential and then I moved to  Nicola and algebraically, this corresponds to the fact that I can construct this bank.  So here, so the co free commutative communoid on top of a formula which contains an existential.  And, and honestly, I don't fully understand how this could be, you know, expressed in the language of, you  know, this hope for algebra.  But I'm, I mean, I would love to have elements because that helps me to understand the material nature of proofs.  I mean, this is really the point in a way.  Dear, I take the opportunity to speak to you directly this regarding maybe questions, but we will, I will ask for questions afterwards.  Paul Andre, you know that the street last you all constructed for the scholars being in a field, which, as you mentioned, the vector spaces encounters problems, even when the scholars form, form division,  form a domain, ring without zero divisors.  But I have been aware of paper by post P.  Oh, yeah.  Stay.  You know it, maybe.  Yes.  So I don't have to send you.  Nobody. So, so I, okay, I tried to adapt this construction to a situation where I mean some, some shift, like, pre shift, so it construction where I changed the base ring commutative ring.  And so I needed to, to generalize this.  Yes, to.  So I use, but it's very categorical.  Yes.  And, and the question is, we are not, we'd like to understand better the combinatorics behind.  And that's what I mean. Yes.  So I mean, for, for, for very, you know, kind of general reasons, there exists such such a co free commutative common rate for like any commit commutative ring, but it's not clear why I mean, no, what I find fascinating is that you died all this connection with with with your work and differentiation.  I think that I would need to understand better. And so I just wanted to mention this.  We can interact in a way.  Yeah, of course, I would, I would love to.  Other questions.  Please.  Sorry if I missed it.  But why exactly do you need to find a dual here? Do you need it to define exclamation mark mark a or do you need to dualize it?  It's about this.  So I mean, when you get to, when you want to work with  So, okay, so what happened, okay, I will.  So what happened is traditional models of, because it has to do with linear logic.  So what happens with traditional models of linear logic is that, in fact, we are able to build using topological, you know, vector spaces or this kind of things were able to define the co free commutative common rate by some kind of variation on the general, I mean, symmetric algebra construction.  So, and so we get something like, you know, powers, I mean, tensile powers of a to the end.  We see, we see metrized it we do some, some clever, you know,  limit construction is not anymore some and we get something when we do realize it, this gives the co free commutative common rate. In the case of vector spaces like you know with no topology, there is this construction which I find extremely, I mean, mysterious, where you use the  fact that every co algebra induces an algebra structure on the dual. And then you do some kind of clever, clever restriction of the under double double on the by dual, so that you get the co free commutative common rate I'm not sure it answers your question but I just wanted to  to say that to me, I kind of understand it by honestly I don't understand it I mean I understand it from the outside, but I don't have a completely clear combinatorial.  And this is what I hope I understand I will, I will get from this kind of work by Farah and Christian.  Sorry, sorry, I, I, we could discuss offline and I will be happy but thank you very much.  Thanks for watching 1330. Thank you.
Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_60_131.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_132_383.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_384_8039.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_8040_9179.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_9180_11831.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_11832_21695.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_21696_35987.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_35988_36863.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_36864_37175.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_37176_37427.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_37428_37571.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_37572_38147.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_38148_39287.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_39288_40331.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_40332_40415.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_40416_41327.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_41328_44483.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_44484_47639.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_47640_48443.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_48444_48527.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_48528_52163.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_52164_62411.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_62412_62639.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_62640_63107.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_63108_65867.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_65868_65939.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_65940_66083.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_66084_66551.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_66552_66647.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_66648_67235.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_67236_67835.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_67836_67883.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_67884_67955.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_67956_68363.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_68364_68411.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_68412_68459.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_68460_68507.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_68508_68651.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_68652_73451.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_73452_74483.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_74484_74603.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_74604_76211.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_76212_76583.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_76584_76799.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_76800_77903.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_77904_79199.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_79200_81371.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_81372_81443.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_81444_82283.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_82284_82331.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_82332_82787.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_82788_82835.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_82836_85499.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_85500_86615.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_86616_86687.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_86688_86975.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_86976_88523.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_88524_88571.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_88572_88631.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_88632_88727.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_88728_89867.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_89868_89927.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_89928_89975.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_89976_90023.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_90024_91355.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_91356_91403.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_91404_91775.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_91776_91823.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_91824_91883.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_91884_102359.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_102360_102407.png Paul_Andre_Mellies_-_Dialogue_Games_and_Logical_Pr_JK2B_9eFRMA_102408_102479.png