BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:David Spivak DTSTART:20210204T170000Z DTEND:20210204T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/1 DESCRIPTION:Title: Poly: a category of remarkable abundance\nby D avid Spivak as part of Topos Institute Colloquium\n\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /1/ END:VEVENT BEGIN:VEVENT SUMMARY:Richard Garner DTSTART:20210211T210000Z DTEND:20210211T220000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/2 DESCRIPTION:Title: Comodels of an algebraic theory\nby Richard Ga rner as part of Topos Institute Colloquium\n\n\nAbstract\nIn 1991 Eugenio Moggi introduced the monadic approach to computational effects\; this is t he mechanism by which purely functional programming languages such as Hask ell can express computations with side-effects such as output\, input\, or interaction with an external store.\n\nAround 2000\, Plotkin and Power re fined the Moggi perspective by looking not at monads\, but the equational algebraic theories which generate them: this amounts to specifying not jus t a kind of side-effect\, but a set of primitive operations by which one c an program with these side-effects.\n\nAlgebraic theories have models\, no t only in the category of sets\, but also in any category with finite prod ucts. In particular\, one can look at comodels of a theory: a model in the opposite of the category of sets. A crucial insight of Power and Shkaravs ka is that\, if T is a theory encoding interaction with an environment\, t hen a T-comodel is a state machine providing an instance of the environmen t with which T interacts.\n\nThe objective of this talk is to explain this history\, and to prove a new result: the category of comodels of any alge braic theory T is a presheaf category [B\,Set]\, where B is a small catego ry\, which can be computed explicitly\, that encodes the static and dynami c properties of the side-effects encoded by T.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /2/ END:VEVENT BEGIN:VEVENT SUMMARY:Gunnar E. Carlsson DTSTART:20210218T170000Z DTEND:20210218T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/3 DESCRIPTION:Title: Relative topology\, motion planning\, and coverage problems\nby Gunnar E. Carlsson as part of Topos Institute Colloquium \n\n\nAbstract\nAlgebraic topology produces invariants that capture aspect s of the shape of a space\, or in the case of topological data analysis. A lthough these invariants are in general quite rich\, they are somewhat spa rse in low dimensions. On the other hand\, it is possible to consider comm a categories of spaces\, for example the category of spaces with reference to a fixed base space and morphisms respecting the reference map. When on e does this\, one obtains a much richer set of invariants. I will discuss how to apply this kind of construction in the setting of evasion problems for sensor nets and more general motion planning problems.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /3/ END:VEVENT BEGIN:VEVENT SUMMARY:Samson Abramsky DTSTART:20210311T170000Z DTEND:20210311T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/4 DESCRIPTION:Title: The logic of contextuality\nby Samson Abramsky as part of Topos Institute Colloquium\n\n\nAbstract\n(joint work with Rui Soares Barbosa)\n\nContextuality is a key signature of quantum non-classi cality\, which has been shown to play a central role in enabling quantum a dvantage for a wide range of information-processing and computational task s.\nWe study the logic of contextuality from a structural point of view\, in the setting of partial Boolean algebras introduced by Kochen and Specke r in their seminal work.\nThese contrast with traditional quantum logic a la Birkhoff--von Neumann\nin that operations such as conjunction and disju nction are partial\, only being defined in the domain where they are physi cally meaningful.\n\nWe study how this setting relates to current work on contextuality such as the sheaf-theoretic and graph-theoretic approaches.\ nWe introduce a general free construction extending the commeasurability r elation on a partial Boolean algebra\, i.e. the domain of definition of th e binary logical operations.\nThis construction has a surprisingly broad r ange of uses.\nWe apply it in the study of a number of issues\, including: \n\n- establishing the connection between the abstract measurement scenari os studied in the contextuality literature and the setting of partial Bool ean algebras\;\n\n- formulating various contextuality properties in this s etting\, including probabilistic contextuality as well as the strong\, sta te-independent notion of contextuality given by Kochen--Specker paradoxes\ , which are logically contradictory statements validated by partial Boolea n algebras\, specifically those arising from quantum mechanics\;\n\n- inve stigating a Logical Exclusivity Principle\, and its relation to the Probab ilistic Exclusivity Principle widely studied in recent work on contextuali ty\nas a step towards closing in on the set of quantum-realisable correlat ions\;\n\n- developing some work towards a logical characterisation of the Hilbert space tensor product\, using logical exclusivity to capture some of its salient quantum features.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /4/ END:VEVENT BEGIN:VEVENT SUMMARY:John Baez DTSTART:20210325T180000Z DTEND:20210325T190000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/5 DESCRIPTION:Title: Mathematics in the 21st century\nby John Baez as part of Topos Institute Colloquium\n\n\nAbstract\nThe climate crisis is part of a bigger transformation in which humanity realizes that the Earth is a finite system and that no physical quantity can grow exponentially f orever. This transformation may affect mathematics — and be affected by it — just as dramatically as the agricultural and industrial revolutions did. After a review of the problems\, we discuss how mathematicians can h elp make this transformation a bit easier\, and some ways in which mathema tics may change.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /5/ END:VEVENT BEGIN:VEVENT SUMMARY:Dan Christensen DTSTART:20210401T170000Z DTEND:20210401T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/6 DESCRIPTION:Title: Reasoning in an ∞-topos with homotopy type theor y\nby Dan Christensen as part of Topos Institute Colloquium\n\n\nAbstr act\nThis talk will be an introduction to homotopy type theory that will  explain how it can be used to prove theorems that hold in any ∞-topos. I will introduce the basic ideas of type theory and give some intuition f or what these mean homotopically.  I will end by giving examples of resu lts proved in homotopy type theory that tell us new results in any ∞-to pos.  No prior knowledge of type theory or ∞-category theory will be a ssumed.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /6/ END:VEVENT BEGIN:VEVENT SUMMARY:Joachim Kock DTSTART:20210408T170000Z DTEND:20210408T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/7 DESCRIPTION:Title: Noncrossing hyperchords and free probability\n by Joachim Kock as part of Topos Institute Colloquium\n\n\nAbstract\nFree probability is a noncommutative probability theory introduced by Voiculesc u in the 1980s\, motivated by operator algebras and free groups\, and usef ul in random matrix theory. Where classical independence relates to the te nsor product of algebras\, free independence relates to the free product o f algebras. Speicher discovered the combinatorial substrate of the theory: noncrossing partitions. He derived the free cumulant-moment relations fro m Möbius inversion in the incidence algebra of the lattice of noncrossing partitions\, and used it\, via two reduction procedures\, to model free m ultiplicative convolution. A crucial ingredient\, which has no analogue in the classical setting\, is the notion of Kreweras complement of a noncros sing partition. In this talk\, after a long introduction to these topics\, I will explain some more categorical viewpoints. A first step is an opera d of noncrossing partitions. A second step is a decomposition space (2-Seg al space) Y of noncrossing hyperchords\, whose simplicial structure encode s higher versions of Kreweras complementation. The incidence bialgebra of Y is a direct combinatorial model for free multiplicative convolution. It is related to the previous models by the standard simplicial notion of dec alage: the first decalage of Y gives the (two-sided bar construction of th e) operad\, and the second decalage gives the lattice. These two decalages encode precisely Speicher's two reductions.\n\nThis is joint work with Ku rusch Ebrahimi-Fard\, Loïc Foissy\, and Frédéric Patras.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /7/ END:VEVENT BEGIN:VEVENT SUMMARY:Emily Riehl DTSTART:20210506T170000Z DTEND:20210506T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/8 DESCRIPTION:Title: Contractibility as uniqueness\nby Emily Riehl as part of Topos Institute Colloquium\n\n\nAbstract\nWhat does it mean for something to exist uniquely? Classically\, to say that a set A has a uniq ue element means that there is an element x of A and any other element y o f A equals x. When this assertion is applied to a space A\, instead of a m ere set\, and interpreted in a continuous fashion\, it encodes the stateme nt that the space A is contractible\, i.e.\, that A is continuously deform able to a point. This talk will explore this notion of contractibility as uniqueness and its role in generalizing from ordinary categories to infini te-dimensional categories.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /8/ END:VEVENT BEGIN:VEVENT SUMMARY:Maria Emilia Maietti DTSTART:20210513T170000Z DTEND:20210513T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/9 DESCRIPTION:Title: Quotient completions for topos-like structures \nby Maria Emilia Maietti as part of Topos Institute Colloquium\n\n\nAbstr act\nIn this talk we report fundamental results concerning free completion s with quotients of specific Lawvere doctrines for building toposes\, quas i-toposes and predicative versions of them. Our final goal is to use such completions for modelling foundations of constructive and classical mathem atics which are predicative in the sense of Poincaré\, Weyl and Feferman\ , including that in [M09]. We first recall how the tool of completing an e lementary existential Lawvere doctrine with exact quotients is the fundame ntal construction behind the tripos-to-topos construction in [HJP80] besid e including as instances both the exact completion of a regular category a nd that of a weakly lex finite product category\, as reported in [MR15]. W e then describe recent work with Fabio Pasquali and Pino Rosolini where we show how the elementary quotient completion of an elementary Lawvere doct rine in [MR13] is the fundamental construction behind a tripos-to-quasi-to pos construction including toposes as exact completions of a left exact ca tegory in [Me03] as instances. We also mention a joint work with Davide Tr otta where we extend results in [MPR17] about tripos-to-topos construction s coinciding with exact completions of a left exact category. We end by a pplying the elementary quotient completion to build examples of predicati ve toposes including the Effective Predicative Topos in [MM21].\n\nReferen ces\n\n[HJP80] J.M. Hyland\, P. T. Johnstone and A.M.Pitts. Tripos theory. Math. Proc. Cambridge Philos. Soc. 88\, 205-232\, 1980\n\n[M09] M.E. Maie tti. A minimalist two-level foundation for constructive mathematics. Annal s of Pure and Applied Logic\, 160(3): 319-354\, 2009\n\n[MR13] M.E. Maiett i and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories\, 27(17): 445–463\, 2013\n\n[MR15 ] M.E. Maietti and G. R osolini. Unifying Exact Completions. Applied Categorical Structures 23(1): 43-52\, 2015\n\n[MPR17] M.E. Maietti\, F. Pasquali and G. Rosolini. Tripo ses\, exact completions\, and Hilbert's ε-operator. Tbilisi Mathematical Journal. 10(3): 141-66\, 2017\n\n[Me03] M. Menni. A characterization of th e left exact categories whose exact completions are toposes. Journal of Pu re and Applied Algebra\, 3(177): 287-301\, 2003\n\n[MM21] M.E. Maietti\, S . Maschio. A predicative variant of Hyland's Effective Topos. To appear in The Journal of Symbolic Logic\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /9/ END:VEVENT BEGIN:VEVENT SUMMARY:Tobias Fritz DTSTART:20210520T170000Z DTEND:20210520T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/10 DESCRIPTION:Title: The law of large numbers in categorical probabili ty\nby Tobias Fritz as part of Topos Institute Colloquium\n\n\nAbstrac t\nThe law of large numbers (in its various guises) can be regarded as the most central result of probability theory\, and any serious axiomatic sys tem for probability must reproduce it in some form. After a general introd uction to categorical probability in terms of Markov categories\, I will e xplain how to formulate a form of the strong law of large numbers within t his framework\, namely the Glivenko-Cantelli theorem on the convergence of the empirical distribution. I will also sketch how to use this statement in order to derive other laws of large numbers from it.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /10/ END:VEVENT BEGIN:VEVENT SUMMARY:Michael Shulman DTSTART:20210527T170000Z DTEND:20210527T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/11 DESCRIPTION:Title: Two-dimensional semantics of homotopy type theory \nby Michael Shulman as part of Topos Institute Colloquium\n\n\nAbstra ct\nThe general higher-categorical semantics of homotopy type theory invol ves (∞\,1)-toposes and Quillen model categories. However\, for many appl ications it suffices to consider (2\,1)-toposes\, which are reasonably con crete categorical objects built out of ordinary groupoids. In this talk I 'll describe how to interpret homotopy type theory in (2\,1)-toposes\, and some of the applications we can get from\nsuch an interpretation. I will assume a little exposure to type theory\, as in Dan Christensen's talk fro m April\, but no experience with higher toposes or homotopy theory. This t alk will also serve as an introduction to some basic notions of Quillen mo del categories\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /11/ END:VEVENT BEGIN:VEVENT SUMMARY:Steve Awodey DTSTART:20210603T170000Z DTEND:20210603T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/12 DESCRIPTION:Title: Model Structures from Models of HoTT\nby Stev e Awodey as part of Topos Institute Colloquium\n\n\nAbstract\nHomotopical models of Martin-Löf type theory often make use of the notion of a Quille n model category\, even if only implicitly. From the interpretation of id entities between terms as paths in an abstract space\, to the univalence p rinciple identifying identities of types with homotopy equivalences of spa ces\, the standard tools of abstract homotopy theory provide the means to make rigorous the basic intuition behind the homotopical interpretation of the formal logical system. \nSo good is this kind of model that it turns out to be possible to invert the process\, in a certain sense\; given a c ategorical model of HoTT of an appropriate kind\, one can construct from i t a full Quillen model structure on the underlying category. This can be seen as a further strengthening of the idea of HoTT as the internal langua ge of an $\\infty$-topos.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /12/ END:VEVENT BEGIN:VEVENT SUMMARY:Kathryn Hess DTSTART:20210624T180000Z DTEND:20210624T190000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/13 DESCRIPTION:Title: From comonads to calculus\nby Kathryn Hess as part of Topos Institute Colloquium\n\n\nAbstract\nAbstracting the framewo rk common to most flavors of functor calculus\, one can define a calculus on a category M equipped with a distinguished class of weak equivalences t o be a functor that associates to each object x of M a tower of objects in M that are increasingly good approximations to x\, in some well defined\, Taylor-type sense. Such calculi could be applied\, for example\, to test ing whether morphisms in M are weak equivalences.\n\nIn this talk\, after making the definition above precise\, I will describe a machine for creati ng calculi on functor categories Fun (C\,M) that is natural in both the so urce C and the target M. Our calculi arise by comparison of the source cat egory C with a tower of test categories\, equipped with cubical structure of progressively higher dimension\, giving rise to sequences of resolution s of functors from C to M\, built from comonads derived from the cubical s tructure on the test categories. The stages of the towers of functors tha t we obtain measure how far the functor we are analyzing deviates from bei ng a coalgebra over each of these comonads. The naturality of this constr uction makes it possible to compare both different types calculi on the sa me functor category\, arising from different towers of test categories\, and the same type of calculus on different functor categories\, given by a fixed tower of test categories.\n\n(Joint work with Brenda Johnson)\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /13/ END:VEVENT BEGIN:VEVENT SUMMARY:Asgar Jamneshan DTSTART:20210415T170000Z DTEND:20210415T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/14 DESCRIPTION:Title: Topos theory and measurability\nby Asgar Jamn eshan as part of Topos Institute Colloquium\n\n\nAbstract\nIn point-free ( or abstract) measure theory measurable spaces are replaced by $\\sigma$-co mplete Boolean algebras\, measurable functions by Boolean homomorphisms\, and measure spaces by measure algebras. This more general perspective has some advantages over the traditional pointwise approach to measure theory. For example\, it facilitates the use of topos-theoretic techniques to stu dy measurability. To this effect\, a translation process between the inter nal language/ logic of certain Boolean topoi and the "usual" external lang uage/ logic is required which we can accomplish by using the formalism of conditional analysis. We illustrate this with some recent applications in ergodic theory.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /14/ END:VEVENT BEGIN:VEVENT SUMMARY:Chris Heunen DTSTART:20210617T170000Z DTEND:20210617T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/15 DESCRIPTION:Title: Sheaf representation of monoidal categories\n by Chris Heunen as part of Topos Institute Colloquium\n\n\nAbstract\nWould n't it be great if monoidal categories were nice and easy? They are! We wi ll discuss how a monoidal category embeds into a "nice" one\, and how a "n ice" monoidal category consists of global sections of a sheaf of "easy" mo noidal categories. This theorem cleanly separates "spatial" and "temporal" directions of monoidal categories.\n\nMore precisely\, "nice" means that certain morphisms into the tensor unit have joins that are respected by te nsor products\, namely those morphisms that are central and idempotent wit h respect to the tensor product. By "easy" we mean that the topological sp ace of which these central idempotents form the opens is a lot like a sing leton space\, namely local.\n\nCategorifying flabby sheaves in the appropr iate way makes the representation functorial from monoidal categories to s chemes of local monoidal categories. The representation respects many prop erties of monoidal categories: if a monoidal category is closed/traced/com plete/Boolean\, then so are its local stalks. As instances we recover the Lambek-Moerdijk-Awodey sheaf representation for toposes\, the Stone repres entation of Boolean algebras\, the representation by germs of open subsets of a topological space\, and the Takahashi representation of Hilbert modu les as continuous fields of Hilbert spaces.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /15/ END:VEVENT BEGIN:VEVENT SUMMARY:Shaowei Lin DTSTART:20210422T170000Z DTEND:20210422T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/16 DESCRIPTION:Title: Proofs as programs: challenges and strategies for program synthesis\nby Shaowei Lin as part of Topos Institute Colloqui um\n\n\nAbstract\nThe Curry-Howard correspondence between proofs and progr ams suggests that we can exploit proof assistants for writing software. I will discuss the challenges behind a naïve execution of this idea\, and s ome preliminary strategies for overcoming them. As an example\, we will or ganize higher-order information in knowledge graphs using dependent type t heory\, and automate the answering of queries using a proof assistant. In another example\, we will explore how decentralized proof assistants can e nable mathematicians or programmers to work collaboratively on a theorem o r application. If time permits\, I will outline connections to canonical s tructures (ssreflect)\, reflection (ssreflect)\, transport\, unification a nd universe management.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /16/ END:VEVENT BEGIN:VEVENT SUMMARY:Geoffrey Cruttwell DTSTART:20210708T170000Z DTEND:20210708T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/17 DESCRIPTION:Title: Categorical differential structures and their rol e in abstract machine learning\nby Geoffrey Cruttwell as part of Topos Institute Colloquium\n\n\nAbstract\nA fundamental component of many machi ne learning algorithms is differentiation. Thus\, if one wishes to abstra ct and generalize aspects of machine learning\, it is useful to have an ab stract perspective on differentiation. There has been much work on catego rical differential structures in the past few years with the advent of dif ferential categories\, Cartesian differential categories\, and tangent cat egories. In this talk I'll focus on Cartesian reverse differential catego ries\, a recent variant of Cartesian differential categories\, and touch o n how they can be used in abstract machine learning.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /17/ END:VEVENT BEGIN:VEVENT SUMMARY:Walter P Tholen DTSTART:20210722T170000Z DTEND:20210722T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/18 DESCRIPTION:Title: What is monoidal topology?\nby Walter P Thole n as part of Topos Institute Colloquium\n\n\nAbstract\nMonoidal topology m ay be seen as being inspired by some visionary remarks in Hausdorff‘s „Grundzüge der Mengenlehre“ of 1914\, and it takes its modern lead fr om two distinct seminal contributions of the early 1970s: the Manes-Barr p resentation of topological spaces in terms of ultrafilter convergence axio ms\, and Lawvere’s presentation of metric spaces as small categories enr iched in the extended non-negative half-line of the reals. Both types of s paces become instances of small so-called (T\,V)-categories\, where T is a Set-monad and V a (commutative) quantale\, i.e. a small\, thin and (symme tric) monoidal-closed category. The setting therefore allows for a general study of „spaces“ that combines geometric and numerical aspects in a natural way.\n\nIn this talk we present some key elements of the theory an d its applications\, showing in particular how the strictification and inv ersion of some naturally occurring inequalities in this lax-monoidal sett ing leads to interesting topological properties and unexpected connections . Time permitting\, we will also point to some on-going and future work in the area.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /18/ END:VEVENT BEGIN:VEVENT SUMMARY:Marcy Robertson DTSTART:20210729T220000Z DTEND:20210729T230000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/19 DESCRIPTION:Title: Topological Inspiration for Infinity Modular Oper ads\nby Marcy Robertson as part of Topos Institute Colloquium\n\n\nAbs tract\nA modular operad can be thought of as an undirected network which a llows for feedback “loops”. An infinity modular operad is such a netwo rk where operations can be continuously varied with respect to time. The goal of this talk is to give a gentle introduction to a Segal model for in finity modular operads\, focusing on the topological origins of the idea. The audience is not expected to be familiar with operads or topology. This talk will cover snippets of joint work with Luci Bonatto\, Pedro Boavida\ , Philip Hackney \, Geoffroy Horel and Donald Yau.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /19/ END:VEVENT BEGIN:VEVENT SUMMARY:Eugene Lerman DTSTART:20210610T170000Z DTEND:20210610T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/20 DESCRIPTION:Title: A category of hybrid systems\nby Eugene Lerma n as part of Topos Institute Colloquium\n\n\nAbstract\nHybrid systems are dynamical systems that exhibit both continuous time evolution and abrupt t ransitions. Examples include mechanical systems (e.g.\, a ball bouncing of f a floor) and cyber-physical systems (e.g.\, a room with a thermostat). D efinitions of a hybrid dynamical systems vary widely in literature but the y usually include directed graphs\, spaces with vector fields attached to the nodes of graphs and partial maps or\, more generally\, relations attac hed to the edges of graphs. The vector fields are used to model continuous evolution and the relations the abrupt transitions.\n\nI wanted to unders tand if analogues of coupled cell networks of Golubitsky\, Stewart and the ir collaborators (these are highly structured coupled systems of ODEs) mak e sense for hybrid dynamical systems. In order to do that I needed to mak e sense of open hybrid systems\, their interconnection\, networks of hybri d systems and maps between networks of hybrid systems.\n\nProceeding by an alogy with continuous time systems I introduced the notion of a hybrid pha se space and its underlying manifold. A hybrid phase space can be succinc tly defined as double functor. Hybrid phase spaces form a category HyPh with morphisms coming from vertical natural transformations. A hybrid dyna mical system is a pair (A\,X) where A is a hybrid phase space and X is a v ector field on the manifold U(A) underlying A. I then constructed a catego ry HyDS of hybrid dynamical system. The definition of HyDS passes a couple of sanity checks.\n\nUsing the foundation laid out above James Schmidt an d I showed that one can also define hybrid surjective submersions\, hybri d open systems\, their interconnections and networks of hybrid systems. T his way one can model systems of bouncing balls and several interconnected rooms with separate thermostats.\n\nReferences: arXiv:1612.01950 [math.DS ] and arXiv:1908.10447 [math.DS] (DOI: 10.1016/j.geomphys.2019.103582).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /20/ END:VEVENT BEGIN:VEVENT SUMMARY:Jonathan Gorard DTSTART:20210429T170000Z DTEND:20210429T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/21 DESCRIPTION:Title: Fast Diagrammatic Reasoning and Compositional App roaches to Fundamental Physics\nby Jonathan Gorard as part of Topos In stitute Colloquium\n\n\nAbstract\nThe Wolfram Model — a discrete spaceti me model based upon hypergraph rewriting — can be naively formalized as a conventional double-pushout rewriting system over a partial adhesive cat egory of (directed) hypergraphs. However\, the abstract rewriting structur e of the model also permits an elegant interpretation in terms of dagger c ompact categories\, with considerable formal analogies to FdHilb and the f oundations of categorical quantum mechanics\, yet with an additional causa l semantics definable in terms of a second symmetric strict partial monoid al structure (such that the entire system can be formalized\, for instance \, in terms of a double category or a weak 2-category). In addition to pot entially defining a general categorical semantics for discrete models of q uantum gravity\, this formalism presents a fundamentally new approach to p erforming efficient diagrammatic reasoning over combinatorial structures\, by suggesting various generalizations of the standard deductive inference rules of resolution\, superposition\, paramodulation and factoring in the Knuth-Bendix completion approach to automated theorem-proving\, and by ma king more explicit use of the causal structure of the abstract rewriting s ystem in the choice of which inference rules to apply. We show how this ap proach can be applied to the problem of enacting fast diagrammatic simplif ication of circuits in quantum information theory\, as well as (time-permi tting) the problem of efficiently discretizing the Cauchy problem in numer ical general relativity\, showcasing comparisons against some existing sof tware frameworks and algorithms.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /21/ END:VEVENT BEGIN:VEVENT SUMMARY:Todd Trimble DTSTART:20210805T170000Z DTEND:20210805T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/22 DESCRIPTION:Title: From 2-rigs to lambda-rings\nby Todd Trimble as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk will summar ize some aspects of recent work with John Baez and Joe Moeller\, which aim s to tie together representations of symmetric groups\, Schur functors\, a nd lambda rings from the point of view of 2-rigs\, which are a categorific ation of ordinary 'rigs' or rings without negatives. A common theme in thi s area is the notion of 'plethory'. We sketch how the archetypal plethory of lambda rings arises simply and naturally from the simplest possible '2- plethory'\, and applying decategorification to it.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /22/ END:VEVENT BEGIN:VEVENT SUMMARY:Pawel Sobocinski DTSTART:20210930T150000Z DTEND:20210930T160000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/23 DESCRIPTION:Title: Algebraic theories with string diagrams\nby P awel Sobocinski as part of Topos Institute Colloquium\n\n\nAbstract\nIn La wvere theories the central role is played by categories with finite produc ts. The free category with finite products on one object (FinSet^op) is th e Lawvere theory of the empty algebraic theory\, and the free category wit h finite products on a signature (of an algebraic theory) has a concrete d escription as a category of classical syntactic terms. But\, using a theor em due to Thomas Fox\, we can also capture these categories nicely using s tring diagrams.\n\nThe string diagrammatic approach gets you further than ordinary syntax. In a POPL 21 paper with Ivan Di Liberti\, Fosco Loregian and Chad Nester\, we developed a Lawvere-style approach to algebraic theor ies with partially defined operations. It turns out that in this setting\, instead of categories with finite products\, the relevant concept is disc rete cartesian restriction categories (dcrc). And string diagrams are the right syntax for this setting: they let us describe the free dcrc on an ob ject and the free dcrc on a signature. I will sketch some of our results a nd talk about some of the ramifications\, including a string diagrammatic description of categories with free finite limits.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /23/ END:VEVENT BEGIN:VEVENT SUMMARY:John Bourke DTSTART:20210909T170000Z DTEND:20210909T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/24 DESCRIPTION:Title: Tensor products\, multimaps and internal homs \nby John Bourke as part of Topos Institute Colloquium\n\n\nAbstract\nThe notions of monoidal category\, multicategory and closed category are close ly related\, with each having their own advantages. Considering the relat ionship between them leads naturally to skew variants — skew monoidal ca tegories\, skew multicategories and skew closed categories — and I will explore some of these variants in this talk.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /24/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrew J. Blumberg DTSTART:20210923T170000Z DTEND:20210923T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/25 DESCRIPTION:Title: Abstract homotopy theory for topological data ana lysis\nby Andrew J. Blumberg as part of Topos Institute Colloquium\n\n \nAbstract\nA starting point for the modern perspective on algebraic topol ogy is the Eilenberg-Steenrod axioms characterizing homology theories. Mo re generally\, there has been a great deal of work starting from insights of Verdier\, Quillen\, and Dwyer-Kan that gives abstract characterizations of the structures of homotopy theory in terms of formal cylinder and susp ension objects or mapping spaces. This talk will be about efforts to unde rstand the invariants of topological data analysis from an abstract perspe ctive. There will be many more questions than answers.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /25/ END:VEVENT BEGIN:VEVENT SUMMARY:Lawrence Paulson DTSTART:20210701T170000Z DTEND:20210701T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/26 DESCRIPTION:Title: Formalising Contemporary Mathematics in Simple Ty pe Theory\nby Lawrence Paulson as part of Topos Institute Colloquium\n \n\nAbstract\nA long-standing question in mathematics is the relevance of formalisation to practice. Rising awareness of fallibility among mathemati cians suggests formalisation as a remedy. But are today's proof assistants up to the task? And what is the right formalism?\n\nA wide variety of mat hematical topics have been formalised in simple type theory using Isabelle /HOL. The partition calculus was introduced by Erdös and R. Rado in 1956 as the study of “analogues and extensions of Ramsey’s theorem”. High ly technical results were obtained by Erdös-Milner\, Specker and Larson ( among many others) for the case of ordinal partition relations\, which is concerned with countable ordinals and order types. Much of this material w as formalised last year (with the assistance of Džamonja and Koutsoukou-A rgyraki). \n\nGrothendieck's Schemes have also been formalised in Isabelle /HOL. This achievement is notable because some prominent figures had conje ctured that schemes were beyond the reach of simple type theory.\n\nSome h ighlights of this work will be presented along with general observations a bout role of type theory in the formalisation of mathematics.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /26/ END:VEVENT BEGIN:VEVENT SUMMARY:Jamie Vicary DTSTART:20210916T170000Z DTEND:20210916T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/27 DESCRIPTION:Title: Understanding free infinity-categories\nby Ja mie Vicary as part of Topos Institute Colloquium\n\n\nAbstract\nInfinity-c ategories have a reputation for being difficult algebraic objects to defin e and work with. In this talk I will present a new definition of free infi nity-category that demystifies them\, and makes them easy to understand fr om an algebraic perspective. The definition is given as a sequence of indu ctive-recursive data structures\, and we explore how this relates to Groth endieck's original ideas on infinity-categories. No knowledge of infinity- categories is required to follow this talk!\n\nThis is joint work with Chr istopher Dean\, Eric Finster\, Ioannis Markakis and David Reutter.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /27/ END:VEVENT BEGIN:VEVENT SUMMARY:Valeria de Paiva DTSTART:20210819T170000Z DTEND:20210819T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/28 DESCRIPTION:Title: Categorical Explicit Substitutions\nby Valeri a de Paiva as part of Topos Institute Colloquium\n\n\nAbstract\nThe advant ages of functional programming are well-known: programs are easier to writ e\, understand and verify than their imperative counterparts. However\, fu nctional languages tend to be more memory intensive and these problems hav e hindered their wider use in industry. The xSLAM project tried to address these issues by using *explicit substitutions* to construct and implement more efficient abstract machines\, proved correct by construction.\n\nIn this talk I recap two results from the xSLAM project which haven't been su fficiently discussed. First\, we provided categorical models for the calcu li of explicit substitutions (linear and cartesian) that we are interested in. No one else seems to have provided categorical models for explicit su bstitutions calculi\, despite the large number of explicit substitutions s ystems available in the literature. Indexed categories provide models of cartesian calculi of explicit substitutions. However\, these structures ar e inherently non-linear and hence cannot be used to model *linear* calculi of explicit substitutions. Our work replaces indexed categories with pre -sheaves\, thus providing a categorical semantics covering both the linear and cartesian cases. Our models satisfy soundness and completeness\, as e xpected. \n\nSecondly\, we recall a different linear-non-linear type theor y\, built from Barber and Plotkin DILL ideas\, which\, like DILL\, is bett er for implementations. Unlike DILL\, this type theory\, called ILT\, sat isfies an internal language theorem. Thus we describe ILT\, show categoric al semantics for it and sketch the proof of its internal language theorem \, thus justifying its use in implementations. These results are examples of `(categorically) structured deep syntax'\, to borrow Hyland's characte rization.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /28/ END:VEVENT BEGIN:VEVENT SUMMARY:Anders Mortberg DTSTART:20211007T150000Z DTEND:20211007T160000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/29 DESCRIPTION:Title: Cubical Methods in Homotopy Type Theory and Univa lent Foundations\nby Anders Mortberg as part of Topos Institute Colloq uium\n\n\nAbstract\nOne of the aims of Homotopy Type Theory and Univalent Foundations (HoTT/UF) is to provide a practical foundation for computer fo rmalization of mathematics by building on deep connections between type th eory\, homotopy theory and (higher) category theory. Some of the key inven tions of HoTT/UF include Voevodsky's univalence axiom relating equality an d equivalence of types\, the internal stratification of types by the compl exity of their equality\, as well as higher inductive types which allow sy nthetic reasoning about spaces in type theory. In order to provide computa tional support for these notions various cubical type theories have been i nvented. In particular\, the Agda proof assistant now has a cubical mode w hich makes it possible to work and compute directly with the concepts of H oTT/UF. In the talk I will discuss some of the mathematical ideas which mo tivate these developments\, as well as show examples of how computer mecha nization of mathematics looks like in Cubical Agda. I will not assume expe rt knowledge of HoTT/UF and key concepts will be introduced throughout the talk.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /29/ END:VEVENT BEGIN:VEVENT SUMMARY:Andreas Blass DTSTART:20211014T170000Z DTEND:20211014T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/30 DESCRIPTION:Title: A topos view of axioms of choice for finite sets< /a>\nby Andreas Blass as part of Topos Institute Colloquium\n\n\nAbstract\ nTarski proved (in set theory without choice) that if one assumes that\nal l families of 2-element sets have choice functions then one can\nprove tha t all families of 4-element sets have choice functions.\nMostowski (1937) investigated similar implications\, giving\nnumber-theoretic and group-the oretic conditions\, some necessary and\nsome sufficient for such implicati ons. But some questions remained\nunsolved\, in particular: Do choice fro m 3-element sets\, from 5-element\nsets\, and from 13-element sets togethe r imply choice from 15-element\nsets. Gauntt (1970) resolved those remain ing questions\, using\ngroup-theoretic criteria. I plan to describe some of this work and to\nexplain what it has to do with topos theory.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /30/ END:VEVENT BEGIN:VEVENT SUMMARY:Chris Kapulkin DTSTART:20211021T170000Z DTEND:20211021T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/31 DESCRIPTION:Title: Cubical setting for Discrete Homotopy Theory\ nby Chris Kapulkin as part of Topos Institute Colloquium\n\n\nAbstract\nDi screte homotopy theory\, developed by H. Barcelo and collaborators\, is a homotopy theory of (simple) graphs. Homotopy invariants of graphs have fou nd numerous applications\, for instance\, in the theory of matroids\, hype rplane arrangements\, and time series analysis. Discrete homotopy theory i s also a special instance of a homotopy theory of simplicial complexes\, d eveloped by R. Atkin\, to study social and technological networks.\n\nIn t he talk\, I will introduce the main concepts and open problems of discrete homotopy theory. I will also report on the joint work with D. Carranza on developing a new foundation for discrete homotopy theory in the category of cubical sets\, which offers solutions to a number of long standing open problems in the field.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /31/ END:VEVENT BEGIN:VEVENT SUMMARY:Dorette Pronk DTSTART:20211028T170000Z DTEND:20211028T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/32 DESCRIPTION:Title: Doubly Lax Colimit of Double Categories with Appl ications\nby Dorette Pronk as part of Topos Institute Colloquium\n\n\n Abstract\nThus far\, lax and oplax pseudo colimits of double categories ha ve been considered in two flavours [2]: horizontally lax and vertically la x\, based on the notions of horizontal and vertical transformations (respe ctively) between double functors. Also\, the diagrams of double categories have typically been indexed by a 2-category.\n\nIn this work we introduce diagrams indexed by a double category\; in order to make sense of this we will map into a version of the quintets of the category of double categor ies\, because this category itself is only enirched in double categories a nd is often taken as a 2-category. Between the new indexing functors we in troduce a new notion of transformation\, namely doubly lax transformation. We then introduce a double categorical version of the Grothendieck constr uction and show that it has a universal property as doubly lax colimit of the diagram\; i.e.\, a colimit that is lax with respect to the new transfo rmations.\n\nAs applications we obtain:\n\n— a universal property as lax colimit for the Grothendieck construction for bicategories described in [ 1]\;\n\n— a universal property for the elements construction for double categories\;\n\n— a notion of fibration for double categories\, differen t from the internal one described by Street and others\;\n\n— a double c ategorical generalization of the classical tom Dieck fundamental groupoid for a space with an action by a topological group.\n\nThis is joint work w ith Marzieh Bayeh (University of Ottawa) and Martin Szyld (Dalhousie Unive rsity).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /32/ END:VEVENT BEGIN:VEVENT SUMMARY:Kevin Buzzard DTSTART:20210812T170000Z DTEND:20210812T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/33 DESCRIPTION:Title: What is the point of Lean's maths library?\nb y Kevin Buzzard as part of Topos Institute Colloquium\n\n\nAbstract\nLean is a computer proof checker developed by Microsoft Research. Over the last four years I have been part of a team of mathematicians and computer scie ntists who have got it into their heads that it is somehow "obviously" a g ood idea to build a formally verified library of modern mathematics in Lea n. You can think of it as a 21st century Bourbaki if you like\, although o ur plans are actually far grander than Bourbaki's. I will talk about two t hings: (1) how it's going and (2) why we're doing it. No background in com puter proof checkers will be necessary to follow the talk.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /33/ END:VEVENT BEGIN:VEVENT SUMMARY:Conor McBride DTSTART:20210826T170000Z DTEND:20210826T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/34 DESCRIPTION:Title: Cats and Types: Best Friends?\nby Conor McBri de as part of Topos Institute Colloquium\n\n\nAbstract\nIntensional Type T heory and Category Theory ought to fit well together\, but the current pra ctical experience of representing concepts from one with the tools of the other is often quite strained. On the one hand\, fibrational approaches to dependency often seem heavy. On the other hand\, definitional equality in type systems often falls way short of delivering even the simplest of coh erences. In this talk\, I shall reflect on the problems and search for opp ortunities. What has to change to make type theoretic proof assistants a g ood medium for categorical approaches to programming and proof? I wish I k new the answer to that question! I can at least offer a few clues. For exa mple\, I shall exhibit a universe of indexed inductively defined datatypes which exhibit nontrivial presheaf structure by construction.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /34/ END:VEVENT BEGIN:VEVENT SUMMARY:Evan Patterson DTSTART:20211202T170000Z DTEND:20211202T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/35 DESCRIPTION:Title: Categories of diagrams in data migration and comp utational physics\nby Evan Patterson as part of Topos Institute Colloq uium\n\n\nAbstract\nDiagrams are among the most fundamental and ubiquitous concepts of category theory. Less appreciated are the several notions of morphism between diagrams in a category. After reviewing the resulting cat egories of diagrams\, this talk will explain their central role in two rec ent projects by the author and collaborators. First\, due to their close c onnections with limits and colimits\, the categories of diagrams provide a natural syntax for defining flexible data migrations between categorical databases. We describe a prototype implementation of this system in Catlab .jl. In the second part of the talk\, we explain how "Tonti diagrams\," di agrammatic presentations of physics equations expressed in vector calculus or exterior calculus\, can be formalized using category-theoretic diagram s. When combined with a suitable discretization scheme\, such as the discr ete exterior calculus (DEC)\, the result is a diagrammatic and composition al approach to building numerical simulators of physical systems.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /35/ END:VEVENT BEGIN:VEVENT SUMMARY:Robert Harper DTSTART:20211209T170000Z DTEND:20211209T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/36 DESCRIPTION:Title: Phase Distinctions in Type Theory\nby Robert Harper as part of Topos Institute Colloquium\n\n\nAbstract\n(Joint work wi th Jon Sterling and Yue Niu)\n\nThe informal phase distinction between com pile-time and run-time in programming languages is formally manifested by the distinction between kinds\, which classify types\, and types\, which c lassify code. The distinction underpins standard programming methodology w hereby code is first type-checked for consistency before being compiled fo r execution. When used effectively\, types help eliminate bugs before they occur.\n\nProgram modules\, in even the most rudimentary form\, threaten the distinction\, comprising as they do both types and programs in a singl e unit. Matters worsen when considerating "open" modules\, with free modul e variables standing for its imports. To maintain the separation in their presence it is necessary to limit the dependency of types\, the static par ts of a module\, to their imported types. Such restrictions are fundamenta l for using dependent types to express modular structure\, as originally s uggested by MacQueen.\n\nTo address this question Moggi gave an "analytic" formulation of program modules in which modules are explicitly separated into their static and dynamic components using tools from category theory. Recent work by Dreyer\, Rossberg\, and Russo develops this approach fully in their account of ML-like module systems. In this talk we consider inst ead a "synthetic" formulation using a proposition to segregate the static from the dynamic\, in particular to define static equivalence to manage ty pe sharing and type dependency\n\nRobert Harper is a Professor of Computer Science at Carnegie Mellon\, where he\nhas been a member of faculty since 1988. He is past recipient of the Allen\nNewell Award for research excell ence and the Herbert Simon Award for teaching\nexcellence. He is author of Practical Foundations for Programming Languages\, a\ntextbook account of programming language theory. His work focuses on the\napplication of type theory to program development\, language design\, compiler\nconstruction\ , and mechanized proof.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /36/ END:VEVENT BEGIN:VEVENT SUMMARY:Paolo Perrone DTSTART:20211118T170000Z DTEND:20211118T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/37 DESCRIPTION:Title: The rise of quantitative category theory\nby Paolo Perrone as part of Topos Institute Colloquium\n\n\nAbstract\nIn seve ral domains of applications\, category theory can be useful to add concept ual clarity and scalability to mathematical models.\nHowever\, ordinary ca tegories often fail to grasp some quantitative aspects: the total cost of a certain strategy\, the number of composite steps\, the discrepancy betwe en a concrete construction and its ideal model\, and so on.\n\nIn order to incorporate these aspects\, it is helpful to switch to a "quantitative" v ersion of categories: weighted categories. These are particular enriched c ategories where each arrow carries a number\, or "weight"\, as in a weight ed graph. The composition of paths comes with a triangle inequality\, anal ogous to the one of metrics and norms\, which equips universal properties with quantitative bounds. Most results in category theory have a weighted analogue\, which often carries additional geometric or analytic significan ce.\nWeighted categories have been around since early work of Lawvere\, bu t only in the last few years researchers are starting to recognize their i mportance. More and more recent papers are using them in fields as diverse as topological data analysis\, geometry\, and probability theory\, some t imes even rediscovering the concepts independently.\n\nIn this talk we are going to see what it's like to work with weighted categories\, their rela tionship with graphs\, and the quantitative aspects about limits and colim its. We will also define a weighted analogue of lenses\, and use it to exp ress liftings of transport plans between probability measures.\n\nRelevant literature: arxiv.org/abs/2110.06591 and additional work in preparation.\ n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /37/ END:VEVENT BEGIN:VEVENT SUMMARY:Florian Rabe DTSTART:20210902T170000Z DTEND:20210902T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/38 DESCRIPTION:Title: MMT: A UniFormal Approach to Knowledge Representa tion\nby Florian Rabe as part of Topos Institute Colloquium\n\n\nAbstr act\nUniFormal is the idea of representing all aspects of knowledge unifor mly\, including narration\, deduction\, computation\, and databases.\nMore over\, it means to abstract from the multitude of individual systems\, whi ch not only often focus on just one aspect but are doing so in mutually in compatible ways\, thus creating a universal framework of formal knowledge. \n\nMMT is a concrete representation language to that end.\nIt systematica lly abstracts from assumptions typically inherent in the syntax and semant ics of concrete systems\, and focuses on language-independence\, modularit y\, and system interoperability.\nWhile constantly evolving in order to co nverge towards UniFormal\, its design and implementation have become very mature.\nIt is now a readily usable high-level platform for the design\, a nalysis\, and implementation of formal systems.\n\nThis talk gives an over view of the current state of MMT\, its existing successes and its future c hallenges.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /38/ END:VEVENT BEGIN:VEVENT SUMMARY:Jeremy Avigad DTSTART:20211104T180000Z DTEND:20211104T190000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/39 DESCRIPTION:Title: Formal mathematics\, dependent type theory\, and the Topos Institute\nby Jeremy Avigad as part of Topos Institute Collo quium\n\n\nAbstract\nModern logic tells us that mathematics can be formali zed\, in principle. Computational proof assistants\, developed over the la st half century\, make it possible to do so in practice. In this talk\, I will briefly survey the state of the field today and discuss some of the r easons that formalization is desirable. I will discuss one particular proo f assistant\, Lean\, and its library\, mathlib. I will explain why depende nt type theory\, Lean's underlying logical framework\, provides an attract ive platform for formalization. Finally\, I will consider ways that formal mathematics can support and enhance the Topos Institute's missions.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /39/ END:VEVENT BEGIN:VEVENT SUMMARY:David Danks DTSTART:20220217T170000Z DTEND:20220217T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/40 DESCRIPTION:Title: Ethics in AI\, not Ethics of AI\nby David Dan ks as part of Topos Institute Colloquium\n\n\nAbstract\nDiscussions of the ethical (and societal) impact of AI often implicitly assume that ethical issues arise only once the AI Is deployed or used. If AI is “just math ” or “just a tool\,” then one might think that ethics is simply irre levant to research and development of AI systems. In contrast\, I will arg ue that ethical issues arise throughout every step of AI creation\, includ ing research efforts that seem to be outside of the scope of ethics. That is\, ethics is an intrinsic part of AI\, not something that arises only af ter the fact. Throughout this argument\, I will provide examples of practi cal tools and practices to improve the ethics in one’s AI systems. These insights and examples will apply to technology development in general\, i ncluding fundamental mathematical research.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /40/ END:VEVENT BEGIN:VEVENT SUMMARY:Bob Coecke DTSTART:20220224T170000Z DTEND:20220224T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/41 DESCRIPTION:Title: Compositional Intelligence\nby Bob Coecke as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk will be fairly high-level and requires no prior technical background. We will introduce the notion of compositional intelligence that my Oxford-based CQ-team is trying to achieve. \n\nIn particular\, starting from the compositional ma tch between natural language and quantum\, which also extends to other dom ains [1]\, we will argue that a new generation of AI can emerge when fully pushing this analogy while exploiting the completeness of categorical qua ntum mechanics [2]. \n\nWe also discuss the notion of compositionality it self\, which takes many different forms within many different contexts\, a nd how the one we need goes beyond previous ones [3]. \n\n[1] Vincent Wan g-Mascianica\, BC (2021) Talking Space: inference from spatial linguistic meanings. https://arxiv.org/abs/2109.06554 \n\n[2] BC\, Dom Horsman\, Ale ks Kissinger\, Quanlong Wang (2021) Kindergarden quantum mechanics graduat es (...or how I learned to stop gluing LEGO together and love the ZX-calcu lus). https://arxiv.org/abs/2102.10984\n\n[3] BC (2021) Compositionality as we see it\, everywhere around us. https://arxiv.org/abs/2110.05327\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /41/ END:VEVENT BEGIN:VEVENT SUMMARY:Maaike Zwart DTSTART:20220331T170000Z DTEND:20220331T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/43 DESCRIPTION:Title: Lessons from failing distributive laws\nby Ma aike Zwart as part of Topos Institute Colloquium\n\n\nAbstract\nComposing monads via distributive laws is tricky business\, as too often small mista kes are overlooked. After failing to find a distributive law for the list monad over itself\, I started proving that finding such a distributive law is impossible. At the same time\, Dan Marsden was studying the famous cou nterexample by Gordon Plotkin that probability does not distribute over no n-determinism. Together we developed an algebraic method to find and gener alise such counterexamples\, resulting in our no-go theorems. In this talk I will explain the main ideas behind our method\, illustrated by a proof that 'plus does not distribute over times'. Then\, I will highlight some c rucial steps in our method\, which tell us which type of monads are "high risk" in failing to compose with other monads. Lastly (time permitting)\, I will say a few words about my current research on combining monads with guarded recursion.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /43/ END:VEVENT BEGIN:VEVENT SUMMARY:Thierry Coquand DTSTART:20220602T170000Z DTEND:20220602T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/44 DESCRIPTION:Title: Sheaf Cohomology in Univalent Type Theory\nby Thierry Coquand as part of Topos Institute Colloquium\n\n\nAbstract\nIn t he introduction of his book on Higher Topos Theory\, Jacob Lurie motivates this theory by the fact that it allows an elegant and general treatment o f sheaf cohomology. It was realised early on that these ideas could be exp ressed in the setting of univalent foundations/homotopy type theory (cf. t he blog post of Mike Shulman on cohomology\, 24 July 2013). I will try to explain recent insights which show that this can be done in a maybe surpri singly direct way. Furthermore\, all this can be formulated in a construct ive meta theory\, avoiding the non effective notion of injective resolutio ns.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /44/ END:VEVENT BEGIN:VEVENT SUMMARY:Zoé Christoff DTSTART:20220317T170000Z DTEND:20220317T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/45 DESCRIPTION:Title: The logic of social influence in networks\nby Zoé Christoff as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk gives an introduction to the use of logical tools in understanding so cial influence and social networks phenomena. Individuals often form their opinions by interpreting the behavior of others around them\, and by reas oning about how those others have formed their opinions. This leads to sev eral well-known herd phenomena\, such as informational cascades\, bystande r effect\, pluralistic ignorance\, bubbles\, and polarization. For instanc e\, in the case of informational cascades\, agents in a sequence imitate o ne another’s choices despite having diverging private evidence\, sometim es leading the whole community to make the worst possible choice. Similar cascading mechanisms are at the heart of diffusion phenomena in social net works. \n\nI first show how an epistemic logic modeling allows to make pre cise the conditions for such cascades to form\, as well as prove their ine scapability. I then turn to what logical tools can do for analysing inform ation flow and influence in social networks. I illustrate how extremely si mplified models can yield surprising new results\, for instance about stab ilization conditions of diffusion processes. Finally\, I discuss how logic might help us further understand how social networks affect collective de cision making processes.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /45/ END:VEVENT BEGIN:VEVENT SUMMARY:Giuseppe Rosolini DTSTART:20220407T170000Z DTEND:20220407T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/46 DESCRIPTION:Title: When an elementary quotient completion is a quasi topos\nby Giuseppe Rosolini as part of Topos Institute Colloquium\n\n\ nAbstract\nThe elementary quotient completion of an elementary doctrine ge neralises the exact completion of a category with finite products and weak equalisers. I intend to present a characterisation of those elementary qu otient completions which produce a quasitopos. As a corollary one gets a c haracterisation of the elementary quotient completions which give an eleme ntary topos. Our work is reminiscent of\, and gathers ideas\, from others: in particular\, Carboni and Vitale’s characterisation of exact completi ons in terms of their projective objects\, Carboni and Rosolini’s charac terisation of locally cartesian closed exact completions\, also in the rev ision by Emmenegger\, and Menni’s characterisation of the exact completi ons which are elementary toposes. This is joint work with Maria Emilia Mai etti and Fabio Pasquali.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /46/ END:VEVENT BEGIN:VEVENT SUMMARY:Tai-Danae Bradley DTSTART:20220526T170000Z DTEND:20220526T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/47 DESCRIPTION:Title: Entropy as an Operad Derivation\nby Tai-Danae Bradley as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk fe atures a small connection between information theory\, algebra\, and topol ogy—namely\, a correspondence between Shannon entropy and derivations of the operad of topological simplices. We will begin with a brief review of operads and their representations with topological simplices and the real line as the main example. We then give a general definition for a derivat ion of an operad in any category with values in an abelian bimodule over t he operad. The main result is that Shannon entropy defines a derivation of the operad of topological simplices\, and that for every derivation of th is operad there exists a point at which it is given by a constant multiple of Shannon entropy. We show this is compatible with\, and relies heavily on\, a well-known characterization of entropy given by Faddeev in 1956 and a recent variation given by Leinster.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /47/ END:VEVENT BEGIN:VEVENT SUMMARY:Dominic Verity DTSTART:20220324T200000Z DTEND:20220324T210000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/48 DESCRIPTION:Title: Zen and the art of ∞-categories\nby Dominic Verity as part of Topos Institute Colloquium\n\n\nAbstract\nYou may well have heard the rumour that ∞-category theory is “really just like cate gory theory with a little homotopy theory thrown in”. Inspired by that c omment\, you might even have headed to a book on ∞-categories or to the nLab to find out more\, only to find that things in the ∞-world are far from that simple.\n\nFirstly you will have discovered that there is no uni versal agreement on what an ∞-category actually is. Instead\, you’ve b een met with a proliferation of ∞-categorical models\; simplicially enri ched categories\, quasi-categories\, (iterated) complete Segal spaces\, co mplicial sets\, Θ-spaces and so on. Then you discover\, to your horror\, that each one of these models supports its own particular interpretations of common categorical concepts\, some of which appear far more familiar th an others. Finally\, you realise that the relationships between the catego ry theories developed for each model are also much less than clear.\n\nIf this weren’t enough to leave anyone reaching for the Aspirin bottle\, th ere is more bad news to come. It quickly becomes clear that there exists q uite a large gap between the informal language used to describe ∞-catego rical arguments\, in blog posts and wiki articles\, and the corresponding formal arguments expressed in any particular model of ∞-categories. Most of these are given either as concrete constructions with simplicial (or i ncreasingly cubical) objects or as abstract model category theoretic argum ents. Now I have no doubt that we “all” love a good simplicial argumen t\, but encoding things in this way does very little to aid our categorica l intuition.\n\nThere must be a better way!\n\nIn this talk we discuss rec ent developments in ∞-technology that seek to address these issues. Spec ifically\, we review the current state of the art in model agnostic ∞-ca tegory theory [2]\, which seeks to provide a unified account of ∞-catego ry theory freed from the straight jacket of a specific model. This allows both for the model independent\, synthetic development of ∞-categorical results and for the transport of analytically derived such results from on e model to another. We shall also see how these techniques are rapidly bei ng reframed in type theoretic terms\, through the development of directed type theory [1\,3]\, thereby promising a more natural language for the for mal development of ∞-categorical concepts and results.\n\nReferences\n\n [1] E. Riehl\, M. Shulman\, A type theory for synthetic ∞-categories\, H igh. Struct. 1 (2017) 147224.\n\n[2] E. Riehl\, D. Verity\, Elements of ∞-category theory\, Cambridge University Press\, 2022.\n\n[3] J. Weinber ger\, A synthetic perspective on (∞\,1)-category theory: Fibrational and semantic aspects\, arXiv Preprint arXiv:2202.13132. (2022).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /48/ END:VEVENT BEGIN:VEVENT SUMMARY:Glynn Winskel DTSTART:20220303T170000Z DTEND:20220303T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/50 DESCRIPTION:Title: Making concurrency functional\nby Glynn Winsk el as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk bridges between two major paradigms in computation\, the *functional*\, at basis c omputation from input to output\, and the *interactive*\, where computatio n reacts to its environment while underway. Central to any compositional theory of interaction is the dichotomy between a system and its environmen t. Concurrent games and strategies address the dichotomy in fine detail\, very locally\, in a distributed fashion\, through distinctions between Pla yer moves (events of the system) and Opponent moves (those of the environm ent). A functional approach has to handle the dichotomy much more ingeniou sly\, through its blunter distinction between input and output. This has l ed to a variety of functional approaches\, specialised to particular inte ractive demands. Through concurrent games we can more clearly see what sep arates and connects the differing paradigms\, and show how: \n\n\n— to l ift functions to strategies\; the "Scott order" intrinsic to \nconcurrent games plays a key role in turning functional dependency to causal depende ncy. \n\n— several paradigms of functional programming and logic arise n aturally as subcategories of concurrent games\, \nincluding stable domain theory\; nondeterministic dataflow\; geometry of interaction\; the dialec tica interpretation\; lenses and optics\; and \ntheir extensions to contai ners in dependent lenses and optics. \n\n— to transfer enrichments of strategies (such as to probabilistic\, quantum or real-number computation) to functional cases.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /50/ END:VEVENT BEGIN:VEVENT SUMMARY:Leo McElroy DTSTART:20220414T170000Z DTEND:20220414T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/51 DESCRIPTION:Title: Making Microworlds: A Framework for Making Sense by Making Things\nby Leo McElroy as part of Topos Institute Colloquium \n\n\nAbstract\nPeople learn best by making things they care about\, which they share with others. The role of an educational technologist is to com municate this principle through tools provided to learners. A primary item in this toolmakers’ toolkit is the microworld\, a concept developed by Seymour Papert as a “growing place for a specific species of powerful id eas or intellectual structures.” A microworld presents someone with a sm all set of ideas in an explorable environment which helps the learner reco mpose those ideas for their own personal expression. Following the develop ment of a collection of microworlds\, we will uncover the meta-structure o f the “growing place” for intellectual structures\, with the aim of id entifying a framework for making tools\, for making sense\, by making thin gs.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /51/ END:VEVENT BEGIN:VEVENT SUMMARY:Alexandra Silva DTSTART:20220519T170000Z DTEND:20220519T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/52 DESCRIPTION:Title: Learning Weighted Automata over Principal Ideal D omains\nby Alexandra Silva as part of Topos Institute Colloquium\n\n\n Abstract\nIn the first part of this talk\, we discuss active learning algo rithms for weighted automata over a semiring. We show that a variant of An gluin's seminal L* algorithm works when the semiring is a principal ideal domain\, but not for general semirings such as the natural numbers. In the second part\, we present some preliminary work on active learning for pro babilistic automata\, and in particular discuss what the setup of the prob lem looks like and how that leads (or not) to impossibility results.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /52/ END:VEVENT BEGIN:VEVENT SUMMARY:Moshe Vardi DTSTART:20220623T170000Z DTEND:20220623T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/53 DESCRIPTION:Title: Ethics Washing in AI\nby Moshe Vardi as part of Topos Institute Colloquium\n\n\nAbstract\nOver the past decade Artifici al Intelligence\, in general\, and Machine Laerning\, in particular\, have made impressive advancements\, in image recognition\, game playing\, natu ral-language understanding and more. But there were also several instances where we saw the harm \nthat these technologies can cause when they are d eployed too hastily. A Tesla crashed on Autopilot\, killing the driver\; a self-driving Uber crashed\, killing a pedestrian\; and commercial face-re cognition systems performed terribly in audits on dark-skinned people. In response to that\, there has been much recent talk of AI ethics. Many orga nizations produced AI-ethics guidelines and companies publicize their newl y established responsible-AI teams.\n\nBut talk is cheap. "Ethics washing" — also called “ethics theater” — is the practice of fabricating o r exaggerating a company’s interest in equitable AI systems that work fo r everyone. An example is when a company promotes “AI for good” initia tives with one hand\, while selling surveillance tech to governments and c orporate customers with the other. I will argue that the ethical lens is t oo narrow. The real issue is how to deal with technology's impact on socie ty. Technology is driving the future\, but who is doing the steering?\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /53/ END:VEVENT BEGIN:VEVENT SUMMARY:Nicolas Behr DTSTART:20220609T170000Z DTEND:20220609T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/54 DESCRIPTION:Title: Fundamentals of Compositional Rewriting Theory\nby Nicolas Behr as part of Topos Institute Colloquium\n\n\nAbstract\nTh is presentation is based upon [1] (joint work with R. Harmer and J. Krivin e). \n\nCategorical rewriting theory is a research field in both computer science and applied category theory\, with a rich history spanning over 50 years of active developments\, starting with the pioneering work of Ehrig in the 1970s.\n\nIn this talk\, I will present recent results [1] on a no vel foundation for reasoning about rewriting theories via so-called compos itional rewriting double categories (crDCs). The design principles followe d in this approach are the typical "unify and conquer" strategy of applied category theory and a particular variant of the notion of compositionalit y. \n\nTo wit\, crDCs permit to formulate a wide variety of categorical re writing semantics uniformly\, whereby the horizontal category for a given semantics models the rewriting rules\, while the vertical category models matchings and co-matchings of rules into objects\, and where the squares m odel so-called direct derivations (i.e.\, individual rewriting steps). Eve n before considering compositionality\, it is already noteworthy that in o rder for crDCs to be well-defined\, strong constraints are imposed upon th e horizontal and vertical categories and the squares of the crDC\, which i n effect suggest categories with adhesivity properties (e.g.\, toposses\, quasi-toposses\, adhesive HLR categories\,...) as natural starting points for constructing crDCs. In this sense\, the notion of crDCs thus permits t o justify the by now standard approach for categorical rewriting theories developed over the past 20 years as being based upon categories with adhes ivity properties (starting with the seminal work of Lack and Sobocinski on adhesive categories) from a clear mathematical high-level perspective.\n\ nCompositionality\, on the other hand\, is a much deeper mathematical prop erty that a categorical rewriting theory may carry. This property entails the existence of so-called Concurrency and Associativity Theorems. The for mer concerns being able to reason on two-step rewriting sequences via impl ementing the overall effect of the two-step rewrite via a composite rule a pplied in a single rewrite step\, and vice versa. The Associativity Theore m then implies that the operation of forming compositions of rewriting rul es is\, in a certain sense\, associative. Compositionality is a necessary and crucial ingredient in the stochastic mechanics and rule algebra formal ism developed by Behr et al. since 2015\, and which permits to provide a m athematically fully consistent and universal formalism for continuous- [2] and discrete-time Markov Chains [3] (central to applications of rewriting to bio- and organo-chemistry\, social network modeling\, etc.) and rule-a lgebraic combinatorics [4].\n\nA central result of [1] is then that a suff icient set of conditions on a double category to model a *compositional* r ewriting theory consists in requiring certain fibrational properties for t he vertical source and target functors from squares of the double categori es\, i.e.\, that they are (residual) multi-opfibrations. I will sketch how these fibrational properties in conjunction with the other crDC axioms yi eld a completely uniform proof of both the Concurrency and the Associativi ty Theorems\, and\, time permitting\, how a large variety of categorical r ewriting semantics indeed fall under the umbrella of our novel crDC formal ism. \n\nFinally\, I will provide an overview of open questions and potent ial fruitful cross-connections of crDC theory with the TIC and broader ACT communities.\n\n\n[1] N. Behr\, R. Harmer and J. Krivine\, "Fundamentals of Compositional Rewriting Theory"\, https://arxiv.org/abs/2204.07175 \n\n [2] N. Behr\, J. Krivine\, J.L. Andersen\, D. Merkle (2021)\, "Rewriting t heory for the life sciences: A unifying theory of CTMC semantics"\, https: //doi.org/10.1016/j.tcs.2021.07.026\n\n[3] N. Behr\, B.S. Bello\, S. Ehme s\, R. Heckel (2021)\, "Stochastic Graph Transformation For Social Network Modeling"\, https://doi.org/10.4204/EPTCS.350.3\n\n[4] N. Behr (2021)\, "On Stochastic Rewriting and Combinatorics via Rule-Algebraic Methods"\, h ttp://dx.doi.org/10.4204/EPTCS.334.2\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /54/ END:VEVENT BEGIN:VEVENT SUMMARY:Martín Escardó DTSTART:20220428T170000Z DTEND:20220428T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/55 DESCRIPTION:Title: Compact totally separated types in constructive u nivalent type theory\nby Martín Escardó as part of Topos Institute C olloquium\n\n\nAbstract\nIf a type X is finite\, then for every map p: X → 𝟚 we can tell\, by exhaustive search\, whether p has a root (we can exhibit x with p x = 0) or not (for every x : X we have that p x = 1). Pe rhaps surprisingly\, there are infinite types X for which this decision is constructively possible. We call such types compact. It turns out that th ere are plenty of infinite compact types in any 1-topos. A basic\, but per haps surprising\, example is the type ℕ∞ of decreasing infinite binary sequences. There are plenty more\, and the purpose of this talk is to exh ibit them. No matter how hard we tried to avoid that\, all searchable type s we could find happen to be well-ordered. But this is just as well\, beca use we can use ordinals to measure how complicated the compact types that we can write down in constructive univalent type theory are. Much of the a bove discussion can be carried out in (the internal language of) a 1-topos . But then some of our constructions go beyond that\, by considering the t ype of all ordinals in a universe\, which is itself an ordinal in the next universe\, and requires univalence and hence moves us to the realm of ∞ -toposes. It remains to address the notion of total separatedness of a typ e X. This is the condition that there are plenty of maps X → 𝟚 to "se parate the points of X" in a suitable sense. I'll rigorously define this a nd exhibit plenty of compact\, totally separated\, well-ordered types in u nivalent type theory. I will mention Johnstone's topological topos as an e xample of where "compact" and "totally separated" acquire their usual topo logical meaning. There is an old\, non-constructive\, theorem of topology that characterizes the compact countable Hausdorff spaces as the countable ordinals with the interval topology. In the topological topos\, assuming a non-constructive meta-language to reason about it\, the searchable objec ts we get are of this form.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /55/ END:VEVENT BEGIN:VEVENT SUMMARY:Christoph Benzmueller DTSTART:20220616T170000Z DTEND:20220616T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/56 DESCRIPTION:Title: Logico-pluralistic exploration of foundational th eories with computers\nby Christoph Benzmueller as part of Topos Insti tute Colloquium\n\n\nAbstract\nSymbolic knowledge representation and reaso ning (KR&R) is a key aspect of human intelligence. Among other things\, it enables scientists to explore new theories\, declaratively describe them\ , and share them with colleagues. In the natural sciences\, abstract theor ies often arise from observations and experiments\; in other fields\, such as metaphysics\, they may result from pure thought experiments\, possibly without data from which to start (and learn from). Strong AI without exp licit symbolic KR&R capabilities thus seems unthinkable. But how can the e xploration of abstract theories\, especially fundamental theories of metap hysics and mathematics\, including logical formalisms\, be fruitfully supp orted on computers? \n\nIn this talk\, I review recent contributions in wh ich a logico-pluralistic KR&R methodology and infrastructure\, called Logi KEy\, has been successfully applied to the exploration and assessment of f oundational theories in metaphysics and mathematics. One such exploratory study on the axiomatic foundations of category theory\, conducted jointly with Dana Scott and students at FU Berlin\, will be described in some more detail. Since LogiKEy also supports exploration and assessment of ethical and legal theories\, it also has applications in the areas of trusted AI and AI&Law.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /56/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrej Bauer DTSTART:20220512T170000Z DTEND:20220512T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/57 DESCRIPTION:Title: The countable reals\nby Andrej Bauer as part of Topos Institute Colloquium\n\n\nAbstract\nJoint work with James E. Hans on from the University of Maryland\, https://james-hanson.github.io.\n\nIn 1874 Georg Cantor published a theorem stating that every sequence of real s is avoided by some real\, thereby showing that the reals are not countab le. Cantor's proof uses classical logic. There are constructive proofs\, a lthough they all rely on the axiom of countable choice. Can the real numbe rs be shown uncountable without excluded middle and without the axiom of c hoice? An answer has not been found so far\, although not for lack of tryi ng.\n\nWe show that there is a topos in which the real numbers are countab le\, i.e.\, there is an epimorphism from the object of natural numbers to the object of Dedekind reals. Therefore\, higher-order intuitionistic logi c cannot show the reals to be uncountable.\n\nThe starting point of our co nstruction is a sequence of reals\, shown to exist by Joseph S. Miller fro m University of Wisconsin–Madison\, with a strong counter-diagonalizatio n property: if an oracle Turing machine computes a specific real number\, when given any oracle representing Miller's sequence\, then the number app ears in the sequence. One gets the idea that the reals ought to be countab le in a realizability topos built from Turing machines with oracles for Mi ller's sequence. However\, we cannot just use ordinary realizability\, bec ause all realizability toposes validate countable choice and consequently the uncountability of the reals.\n\nTo obtain a topos with countable reals \, we define a variant of realizability which we call parameterized realiz ability. First we define parameterized partial combinatory algebras (ppca) \, which are partial combinatory algebras whose evaluation depends on a pa rameter. We then define parameterized realizability toposes. In these real izers witness logical statements uniformly in the parameters. The motivati ng example is the parameterized realizability topos built from the ppca of oracle Turing machines parameterized by oracles for Miller's sequence. In this topos\, Miller's sequence is the desired epimorphism from natural nu mbers to Dedekind reals.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /57/ END:VEVENT BEGIN:VEVENT SUMMARY:John Terilla DTSTART:20220505T170000Z DTEND:20220505T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/58 DESCRIPTION:Title: Rethinking language\nby John Terilla as part of Topos Institute Colloquium\n\n\nAbstract\nLanguage is essential to bein g human. Without it\, no aspect of modern life could exist. But what is language exactly? How precisely does meaning emerge from sequences constr ucted from a small collection of basic symbols or sounds? Biologists\, li nguists\, and philosophers have been debating this question---still unansw ered---for thousands of years. \n\nNow\, at a pivotal moment when intelli gent machines are beginning to acquire human language skills\, new insight s into the nature of language are emerging. Some old beliefs about langu age can probably be cast aside and achievements in artificial intelligence are inspiring some new ways of thinking of language.\n\nI will present an argument for rethinking language and give a tour of some relevant mathema tical ideas. The talk will be prepared keeping in mind the four themes of the Topos Institute Colloquium: ethics and societal impact of mathematic s\, applied category theory\, foundation models\, and technology and tools .\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /58/ END:VEVENT BEGIN:VEVENT SUMMARY:Eduardo Dubuc DTSTART:20220915T170000Z DTEND:20220915T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/59 DESCRIPTION:Title: On localizations via homotopies\nby Eduardo D ubuc as part of Topos Institute Colloquium\n\n\nAbstract\n(joint work with J. Gilabert based on work by Descotte-Dubuc-Szyld).\n\nLet $\\mathcal{C}$ be a category and $\\Sigma$ be a class of morphisms. The localization of \n$\\mathcal{C}$ at $\\Sigma$ is a category $\\mathcal{C}[\\Sigma^{-1}]$ t ogether with a functor $q: \\mathcal{C} \\longrightarrow \\mathcal{C}[\\Si gma^{-1}]$ such that $q(s)$ is an isomorphism for all $s \\in \\Sigma$\, a nd which is initial among such functors. The 2-localization is a 2-catego ry $\\mathcal{C}[\\Sigma^{\\sim 1}]$ together with a functor \n$q: \\mathc al{C} \\longrightarrow \\mathcal{C}[\\Sigma^{\\sim 1}]$ such that $q(s)$ i s a equivalence for all $s \\in \\Sigma$\, and which is initial among such functors. In this talk I will consider the construction of such localizat ions by means of cylinders and its corresponding homotopies\, which will d etermine the 2-cells of $\\mathcal{C}[\\Sigma^{\\sim 1}]$. I will examine the case where $\\Sigma = \\mathcal{W}$ is the class of weak equivalences of a Quillen's model category\, and in particular the role of the fibrant and cofibrant replacements. I will elaborate about functorial versus non functorial factorizations in this construction. \nI will recall informally but with sufficient precision the necessary definitions so that the non experts can grasp the ideas and follow the proofs.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /59/ END:VEVENT BEGIN:VEVENT SUMMARY:Noam Zeilberger DTSTART:20220630T170000Z DTEND:20220630T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/60 DESCRIPTION:Title: Parsing as a lifting problem and the Chomsky-Sch ützenberger representation theorem\nby Noam Zeilberger as part of Top os Institute Colloquium\n\n\nAbstract\nJoint work with Paul-André Melliè s.\n\nIn “Functors are Type Refinement Systems” [1]\, we argued for th e idea that rather than being modelled merely as categories\, type systems should be modelled as functors p : D → T from a category D whose morphi sms are typing derivations to a category T whose morphisms are the terms c orresponding to the underlying subjects of those derivations. One advantag e of this fibrational point of view is that the notion of typing judgment receives a simple mathematical status\, as a triple (R\,f\,S) consisting o f two objects R\, S in D and a morphism f in T such that p(R)=dom(f) and p (S)=cod(f). The question of finding a typing derivation for a typing judgm ent (R\,f\,S) then reduces to the lifting problem of finding a morphism α : R → S such that p(α)=f. We developed this perspective in a series of papers\, and believe that it may be usefully applied to a large variety o f deductive systems\, beyond type systems in the traditional sense. In thi s work [2]\, we focus on derivability in context-free grammars\, a classic topic in formal language theory with wide applications in computer scienc e.\n\nThe talk will begin by explaining how derivations in any context-fre e grammar G may be naturally encoded by a functor of operads p : Free S → W[Σ] from a freely generated operad into a certain “operad of splic ed words”. This motivates the introduction of a more general notion of c ontext-free grammar over any category C\, defined as a finite species S eq uipped with a color denoting the start symbol and a functor of operads p : Free S → W[C] into the operad of spliced arrows in C. We will see that many standard concepts and properties of context-free grammars and languag es can be formulated within this framework\, thereby admitting simpler ana lysis\, and that parsing may indeed be profitably considered from a fibrat ional perspective\, as a lifting problem along a functor from a freely gen erated operad.\n\nThe second half of the talk will be devoted to a new pro of of the Chomsky-Schützenberger Representation Theorem. An important ing redient is the identification of a left adjoint C[−] : Operad → Cat to the operad of spliced arrows functor W[−] : Cat → Operad. This constr uction builds the contour category C[O] of any operad O\, whose arrows hav e a geometric interpretation as “oriented contours” of operations. A d irect consequence of the contour / splicing adjunction is that every finit e species equipped with a color induces a universal context-free grammar\, generating a language of tree contour words. Finally\, we prove a general ization of the Chomsky-Schützenberger Representation Theorem\, establishi ng that any context-free language of arrows over a category C is the funct orial image of the intersection of a C-chromatic tree contour language and a regular language.\n\n[1] P.-A. Melliès and N. Zeilberger\, Functors ar e type refinement systems\, POPL 2015\n\n[2] P.-A. Melliès and N. Zeilber ger\, Parsing as a lifting problem and the Chomsky-Schützenberger represe ntation theorem\, to appear at MFPS 2022\, preliminary version available a t https://hal.archives-ouvertes.fr/hal-03702762\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /60/ END:VEVENT BEGIN:VEVENT SUMMARY:Dan Koditschek DTSTART:20221013T170000Z DTEND:20221013T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/61 DESCRIPTION:Title: Working Compositions for Correct Execution of Rob ot Task Specifications\nby Dan Koditschek as part of Topos Institute C olloquium\n\n\nAbstract\nA long tradition in robotics has deployed dynamic al primitives as empirical modules of behavior [1]. Physically grounded fo rmalization of these practices offers the prospect of an expressive progra mming language of work for dynamically dexterous robotics whose programs l ead to task and motion planners with associated controllers that are corre ct by design [2]. This talk will offer a brief progress report on a bottom -up robotics research agenda seeking to formalize the use of Lagrangian en ergy landscapes as “letters” whose hierarchical [3]\, parallel [4] and sequential [5] compositions yield “words” of hybrid dynamical systems with guaranteed behavioral properties. Attention then shifts to an emergi ng architecture for top-down task and motion planning [6] that offers the promise of abstract\, semantic\, formal specification [7] for mobile mani pulation tasks carried out by general purpose robots [8] in learned\, geom etrically complicated environments [9].\n\nThe talk concludes with a more speculative appraisal of the prospects for a unified programming environme nt allowing the expressive top-down specification of robot behavior with a utomatic compilation into bottom-up words of work that are correct by desi gn. A recent categorical treatment [10] of robot hybrid dynamical systems [11] encodes a well-grounded version of sequential composition [12] and a weak but still practicable version of hierarchical composition [3]\, while neglecting the consideration of cross-talk [4] in its idealization of par allel composition as a monoidal product. Subsequent results imbue a slight ly restricted version of this hybrid dynamical category [10] with a versio n of Conley’s fundamental theorem [13] guaranteeing the existence of glo bal Lyapunov functions that decompose a suitably formulated relaxation of the hybrid state space into a covering by attractor basins and their bound aries [14]. Thus equipped with generalized energy landscapes\, more physi cally grounded refinements of this hybrid dynamical category may yield a p racticable type theory whose associated resource-aware linear logic clause s might be integrated into the more expressive linear temporal logic inter face to the task and motion planning architecture of [7]. Such future dev elopments would greatly advance the longer term agenda toward an empirical ly practicable theory of “programming work” [2].\n\n[1] M. H. Raibert\ , Legged Robots That Balance. Cambridge: MIT Press\, 1986.\n\n[2] D. E. Ko ditschek\, “What Is Robotics? Why Do We Need It and How Can We Get It?\, ” Annu. Rev. Control Robot. Auton. Syst.\, vol. 4\, no. 1\, pp. 1–33\, May 2021\, doi: 10.1146/annurev-control-080320-011601.\n\n[3] R. J. Full and D. E. Koditschek\, “Templates and anchors: neuromechanical hypothese s of legged locomotion on land\,” J. Exp. Biol.\, vol. 202\, pp. 3325– 3332\, 1999.\n\n[4] A. De\, S. A. Burden\, and D. E. Koditschek\, “A hyb rid dynamical extension of averaging and its application to the analysis o f legged gait stability:\,” Int. J. Robot. Res.\, vol. 37\, no. 2–3\, pp. 266–286\, Mar. 2018\, doi: 10.1177/0278364918756498.\n\n[5] R. R. Bu rridge\, A. A. Rizzi\, and D. E. Koditschek\, “Toward a systems theory f or the composition of dexterous robot behaviours\,” Robot. Res. Seventh Int. Symp. ISRR’95\, pp. 149–161.\n\n[6] V. Vasilopoulos et al.\, “R eactive Semantic Planning in Unexplored Semantic Environments Using Deep P erceptual Feedback\,” IEEE Robot. Autom. Lett.\, vol. 5\, no. 3\, pp. 44 55–4462\, Jul. 2020\, doi: 10.1109/LRA.2020.3001496.\n\n[7] V. Vasilopou los\, Y. Kantaros\, G. Pappas\, and D. Koditschek\, “Reactive Planning f or Mobile Manipulation Tasks in Unexplored Semantic Environments\,” IEEE Int. Conf. Robot. Autom. ICRA\, May 2021\, [Online]. Available: https://r epository.upenn.edu/ese_papers/880\n\n[8] T. T. Topping\, V. Vasilopoulos\ , A. De\, and D. Koditschek E.\, “Composition of Templates for Transitio nal Pedipulation Behaviors\,” in Proc. Int. Symp. Rob. Res.\, 2019. [Onl ine]. Available: https://repository.upenn.edu/ese_papers/860/\n\n[9] V. Va silopoulos\, G. Pavlakos\, K. Schmeckpeper\, K. Daniilidis\, and D. E. Kod itschek\, “Reactive navigation in partially familiar planar environments using semantic perceptual feedback\,” Int. J. Robot. Res.\, vol. 41\, n o. 1\, pp. 85–126\, Jan. 2022\, doi: 10.1177/02783649211048931.\n\n[10] J. Culbertson\, P. Gustafson\, D. E. Koditschek\, and P. F. Stiller\, “F ormal composition of hybrid systems\,” Theory Appl. Categ.\, vol. 35\, n o. 45\, pp. 1634–1682\, Oct. 2020.\n\n[11] A. M. Johnson\, S. A. Burden\ , and D. E. Koditschek\, “A hybrid systems model for simple manipulation and self-manipulation systems\,” Int. J. Robot. Res.\, vol. 35\, no. 11 \, pp. 1354--1392\, Sep. 2016\, doi: 10.1177/0278364916639380.\n\n[12] R. R. Burridge\, A. A. Rizzi\, and D. E. Koditschek\, “Sequential Compositi on of Dynamically Dexterous Robot Behaviors\,” Int. J. Robot. Res.\, vol . 18\, no. 6\, pp. 534–555\, 1999\, doi: 10.1177/02783649922066385.\n\n[ 13] C. R. Robinson\, Dynamical Systems: Stability\, Symbolic Dynamics\, an d Chaos\, Second. Boca Raton\, FL: CRC Press\, 1999. Accessed: Jan. 29\, 2 017. [Online]. Available: http://imb-biblio.u-bourgogne.fr/Record.htm?reco rd=325212414349&idlist=1\n\n[14] M. D. Kvalheim\, P. Gustafson\, and D. E. Koditschek\, “Conley’s Fundamental Theorem for a Class of Hybrid Syst ems\,” SIAM J. Appl. Dyn. Syst.\, pp. 784–825\, Jan. 2021\, doi: 10.11 37/20M1336576.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /61/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrea Censi DTSTART:20220825T170000Z DTEND:20220825T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/62 DESCRIPTION:Title: Categorification of Negative Information\nby Andrea Censi as part of Topos Institute Colloquium\n\n\nAbstract\nI will p resent some very recent and in-progress work about dealing\nwith “negati ve information” categorically. This need arises naturally\nin applicatio ns. For example\, in motion planning problems\, providing\nan optimal solu tion is the same as giving a feasible solution (the\n“positive” inform ation) together with a proof of the fact that there\ncannot be feasible so lutions better than the one given (the “negative”\ninformation). We mo del negative information by introducing the concept\nof “norphisms”\, as opposed to the positive information of morphisms. A\n“nategory” is a category that has “Nom”-sets in addition to hom-sets\,\nand specifie s the compatibility rules between norphisms and morphisms.\nWith this setu p we can choose to work in “coherent” “subnategories”:\nsubcategor ies that describe a potential instantiation of the world in\nwhich all mor phisms and norphisms are compatible. We derive the\ncomposition rules for norphisms in a coherent subnategory\; we show\nthat norphisms do not compo se by themselves\, but rather they need to\nuse morphisms as catalysts. We have two distinct rules of the type\nmorphism + norphism → norphism. We then show that those complex rules\nfor norphism inference are actually a s natural as the ones for\nmorphisms\, from the perspective of enriched ca tegory theory.\n\nThis is joint work with Dr. Jonathan Lorand and Ph.D. st udent Gioele Zardini.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /62/ END:VEVENT BEGIN:VEVENT SUMMARY:Angeliki Koutsoukou Argyraki DTSTART:20221006T170000Z DTEND:20221006T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/63 DESCRIPTION:Title: The new era of formalised mathematics and the ALE XANDRIA Project\nby Angeliki Koutsoukou Argyraki as part of Topos Inst itute Colloquium\n\n\nAbstract\nThe formalisation of mathematics with proo f assistants has recently seen a \nconsiderable increase in activity\, wit h fast-expanding\, flourishing communities attracting computer scientists\ , mathematicians and students. I will discuss the philosophy and motivatio n behind the use of modern proof assistants to formalise mathematics\, ref erring to the state of the art and potential of the area and to recent dev elopments involving the formalisation of advanced\, research-level mathema tics. I will share my experiences from my participation in the ERC project "ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician" (htt ps://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/) at the University of Cambr idge led by Professor Lawrence C. Paulson FRS and I will give an overview of the main contributions and achievements of the project so far.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /63/ END:VEVENT BEGIN:VEVENT SUMMARY:Richard Zanibbi DTSTART:20221027T160000Z DTEND:20221027T170000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/65 DESCRIPTION:Title: Mathematical Information Retrieval: Searching wit h Formulas and Text\nby Richard Zanibbi as part of Topos Institute Col loquium\n\n\nAbstract\nMathematical information is essential for technical work\, but its creation\, interpretation\, and search are challenging. In the hopes of helping users locate mathematical information more easily\, multimodal retrieval models and search interfaces that support both formul as and text have been developed.\n\nIn this talk we will start by discussi ng some differences between the information needs and search behaviors of mathematical experts vs. non-experts. We will then examine techniques used for retrieving math formulas\, and math-aware search engines that support queries containing both formulas and text. Finally\, we will consider fut ure research directions for math-aware search\, including tasks involving Natural Language Processing (NLP) for mathematical texts.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /65/ END:VEVENT BEGIN:VEVENT SUMMARY:David Jaz Myers DTSTART:20220908T170000Z DTEND:20220908T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/66 DESCRIPTION:Title: A synthetic approach to orbifolds\nby David J az Myers as part of Topos Institute Colloquium\n\n\nAbstract\nOrbifolds ar e smooth spaces where the points may have finitely many internal symmetrie s. These spaces often arise as quotients of manifolds by the actions of di screte groups --- that is\, in situations with discrete symmetries\, such as in crystallography. \n\nFormally\, the notion of orbifold has been pres ented in a number of different guises -- from Satake's V-manifolds to Moer dijk and Pronk's proper étale groupoids -- which do not on their face res emble the informal definition. The reason for this divergence between form alism and intuition is that the points of spaces cannot have internal symm etries in traditional\, set-level foundations. In this talk\, we will see a formal definition which closely tracks the informal idea of an orbifold. \n\nBy working with the axioms of synthetic differential geometry in cohes ive homotopy type theory\, we will give a synthetic definition of orbifold (subsuming the traditional definitions) which closely resembles the infor mal definition: an orbifold is a microlinear type where the type of identi fications between any two points is properly finite. In homotopy type theo ry\, we can construct these orbifolds simply by giving their type of point s.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /66/ END:VEVENT BEGIN:VEVENT SUMMARY:Jacques Carette DTSTART:20220922T170000Z DTEND:20220922T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/67 DESCRIPTION:Title: What I learned from formalizing Category Theory i n Agda\nby Jacques Carette as part of Topos Institute Colloquium\n\n\n Abstract\nAn interesting side-effect of formalizing mathematics in a theor em prover is that such efforts frequently leads to learning new details (* ) about a known topic. I'll discuss these "little gems" that become much m ore apparent via formalization. While the focus will be mostly on items le arned through formalizing Category Theory\, a few nuggets from other domai ns (Universal Algebra\, and the theory of programming languages) will also be thrown in.\n\n(*) These details are frequently known to select experts \, but rarely ever recorded in print.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /67/ END:VEVENT BEGIN:VEVENT SUMMARY:Chad Scherrer DTSTART:20220901T170000Z DTEND:20220901T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/68 DESCRIPTION:Title: Applied Measure Theory for Composable Statistical Modeling\nby Chad Scherrer as part of Topos Institute Colloquium\n\n\ nAbstract\nStatistics is often framed in terms of probability distribution s. Distributions are special cases of measures\; we find that working in t hese more general terms leads more naturally to a composable system. For e xample\, a univariate probability density function is defined relative to Lebesgue measure. Bayesian inference often leaves us with an unnormalized posterior\, which (until normalized) is not a distribution at all\, but a measure.\n\nThe MeasureTheory.jl ecosystem takes a principled approach to design\, identifying primitives (measures like Lebesgue and Counting measu re that cannot be described in terms of other measures)\, and a rich set o f combinators for building new measures from existing ones. This approach gives good performance and makes it easy to describe measures and related structures (kernels\, likelihoods\, etc) that are awkward or impossible to express in other systems.\n\nAfter introducing some fundamental concepts relevant to the field of measure theory\, this talk will give an overview of the MeasureTheory.jl library\, finally closing with a brief introductio n to Tilde.jl\, a probabilistic programming language that specifically tar gets MeasureTheory.jl.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /68/ END:VEVENT BEGIN:VEVENT SUMMARY:Josef Urban DTSTART:20220707T170000Z DTEND:20220707T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/69 DESCRIPTION:Title: Combining learning and deduction over formal math corpora\nby Josef Urban as part of Topos Institute Colloquium\n\n\nAb stract\nThe talk will give a brief overview of recent methods that combine learning and deduction over large formal libraries. I will mention the " hammer" linkups between ITPs and ATPs\, systems that learn and perform dir ect tactical guidance of ITPs\, discuss learning of premise selection over large libraries\, and learning-based guidance of saturation-style and tab leau-style automated theorem provers (ATPs) trained over the large proof c orpora. I will also mention feedback loops between proving and learning in this setting\, and show some autoformalization and conjecturing experimen ts.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /69/ END:VEVENT BEGIN:VEVENT SUMMARY:Johan Commelin DTSTART:20220929T170000Z DTEND:20220929T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/70 DESCRIPTION:Title: Breaking the one-mind-barrier in mathematics usin g formal verification\nby Johan Commelin as part of Topos Institute Co lloquium\n\n\nAbstract\nIn this talk I will argue that formal verification helps break the\none-mind-barrier in mathematics. Indeed\, formal verific ation allows a\nteam of mathematicians to collaborate on a project\, witho ut one person\nunderstanding all parts of the project. At the same time\, it also\nallows a mathematician to rapidly free mental RAM in order to wor k on a\ndifferent component of a project. It thus also expands the\none-mi nd-barrier by reducing cognitive load.\n\nI will use the Liquid Tensor Exp eriment as an example\, to illustrate\nthe above two points. This project recently finished the formalization\nof the main theorem of liquid vector spaces\, following up on a\nchallenge by Peter Scholze.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /70/ END:VEVENT BEGIN:VEVENT SUMMARY:Gilles Dowek DTSTART:20221110T170000Z DTEND:20221110T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/72 DESCRIPTION:Title: From the Universality of Mathematical Truth to th e Interoperability of Proof Systems\nby Gilles Dowek as part of Topos Institute Colloquium\n\n\nAbstract\nThe development of computerized proof systems is a major step forward in the never ending quest of mathematical rigor. But it jeopardizes once again the universality of mathematical trut h\, each proof system defining its own language for mathematical statement s and its own truth conditions for these statements. One way to address t his issue is to view the formalisms implemented in these systems as theori es expressed in a common logical framework\, such as Predicate logic\, λ- Prolog\, Isabelle\, the Edinburgh logical framework\, or Dedukti. We show in the talk how theories\, such as Simple type theory\, Simple type theor y with polymorphism\, Simple type theory with predicate subtyping\, the Ca lculus of constructions... can be expressed in Dedukti. Proofs developed with proof processing systems then can be expressed in these theories\, in dependently of the system they have been developed with\, and used in any system that supports the axioms they use.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /72/ END:VEVENT BEGIN:VEVENT SUMMARY:Pawel Sobocinski DTSTART:20221201T170000Z DTEND:20221201T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/74 DESCRIPTION:Title: Electrical circuits with string diagrams\nby Pawel Sobocinski as part of Topos Institute Colloquium\n\n\nAbstract\nOne of the goals of applied category theory is to develop new mathematics for reasoning about open systems of various kinds. In this talk\, I will intro duce a string diagrammatic methodology for reasoning about and manipulatin g non-passive electrical circuits\, which are a classical and well-known e xample of open system. This joint work with Guillaume Boisseau is\, on the one hand\, a rigorous\, compositional\, sound and complete equational cal culus\, while on the other hand\, it retains elements of the intuitive\, c lassical diagrammatic syntax for circuits. It is based on previous work on Affine Graphical Algebra\, joint work with Bonchi\, Piedeleu and Zanasi w hich I will first introduce.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /74/ END:VEVENT BEGIN:VEVENT SUMMARY:Robin Cockett DTSTART:20221020T170000Z DTEND:20221020T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/75 DESCRIPTION:Title: Turing categories\nby Robin Cockett as part o f Topos Institute Colloquium\n\n\nAbstract\nThis talk is based on the foll owing papers/notes:\n\n(1) "Introduction to Turing categories" with Pieter Hofstra\n\n(2) "Timed set\, functional complexity\, and computability" wi th Boils\, Gallagher\, Hrubes\n\n(3) "Total maps of Turing categories" wit h Pieter Hofstra and Pavel Hrubes\n\n(4) "Estonia notes" on my website\n\n Turing categories are the theory of "abstract computability". Their devel opment followed my meeting Pieter Hofstra. He was in Ottawa at the time a nd he subsequently joined me as a postdoc. The core theory was developed in Calgary before he returned to Ottawa as a faculty member. Tragically h e died earlier this year when there was still so much to do and\, indeed\, that he had done\, but had not published.\n\nTuring categories are import ant because they characterize computability in a minimal traditional conte xt. These ideas are not original to Pieter and I: De Paola\, Heller\, Lon go\, Moggi\, and others had all travelled in this terrain before we did. Pieter and I simply took the ideas polished them a bit and moved them a s tep further on a road which still stretches ahead. \n\nSo\, the purpose o f the talk is to try and explain what all this was about ... and what we w ere striving to accomplish. To do this I have to introduce restriction ca tegories and Turing categories in that context. Then I will describe a fa mily of models which are fundamental to computer science. Finally\, I wil l take a quick look along the road at some open issues.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /75/ END:VEVENT BEGIN:VEVENT SUMMARY:Bryce Clarke DTSTART:20221103T170000Z DTEND:20221103T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/76 DESCRIPTION:Title: A double-categorical approach to lenses via algeb raic weak factorisation systems\nby Bryce Clarke as part of Topos Inst itute Colloquium\n\n\nAbstract\nThe goal of this talk is to draw a common thread between three concepts: double categories\, lenses\, and algebraic weak factorisation systems (AWFS). A double category is a 2-dimensional ca tegorical structure consisting of objects\, horizontal and vertical morphi sms\, and cells between them. In applied category theory\, lenses are a ki nd of morphism which consist of a forwards component and a backwards compo nent. An AWFS on a category C consists of a compatible comonad L and monad R on the arrow category of C\, such that each morphism factors into an L- coalgebra followed by an R-algebra. In each case\, two classes of morphism s play a central role — horizontal and vertical\, forwards and backwards \, coalgebras and algebras — and it is natural to wonder if there is a d eeper relationship between these three concepts. \n\nIn this talk\, I will develop a double-categorical approach to lenses via AWFS. The approach bu ilds upon the work of Bourke and Garner\, which characterises AWFS as cert ain kinds of double categories\, and the work of Johnson\, Rosebrugh\, and Wood\, which implicitly characterises lenses as members of the right clas s of an AWFS. Combining these results leads indirectly to a double-categor ical approach to lenses. However\, there is also a direct approach which c onstructs a generalised notion of lens inside any double category\, using a process called the "right-connected completion". I will compare these tw o approaches\, and explore settings where they coincide.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /76/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrei Rodin DTSTART:20221215T170000Z DTEND:20221215T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/77 DESCRIPTION:Title: Univalent Foundations and Applied Mathematics \nby Andrei Rodin as part of Topos Institute Colloquium\n\n\nAbstract\nIn a series of lectures given in 2003 Vladimir Voevodsky identified two strat egic goals for his further mathematical research. The goal number one was to develop a "computerised library of mathematical knowledge". This line o f research eventually led Voevodsky to the idea of Univalent Foundations a nd its implementation with the UniMath library. The goal number two was t o "bridge pure and applied mathematics". Voevodsky's research towards the second goal did not bring published results but in an interview given in 2 012 he expressed his intention to return to this project in the future and explained a possible role of Univalent Foundations in it. \n\nIn this tal k based on archival sources I reconstruct Voevodsky’s original strategy of bridging pure and applied mathematics\, illustrate it with some example s\, and argue that Applied Univalent Foundations is a viable research prog ram. \n\n[1] Andrei Rodin\, Voevodsky’s Unfinished Project: Bridging the Gap between Pure and Applied Mathematics\, BioSystems\, 204 (2021)\, 1043 91\; preprint arXiv : 2012.01150\n\n[2] UniMath Library : https://github.c om/UniMath/UniMath\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /77/ END:VEVENT BEGIN:VEVENT SUMMARY:Alexandre Miquel DTSTART:20221208T170000Z DTEND:20221208T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/78 DESCRIPTION:Title: Implicative algebras: a new foundation for realiz ability and forcing\nby Alexandre Miquel as part of Topos Institute Co lloquium\n\n\nAbstract\nIn this talk\, I will present implicative algebras \, a simple algebraic\nstructure generalizing complete Heyting algebras an d abstract Krivine\nstructures\, and based on a surprising identification between the\nnotions of a realizer and of a type. I will show that this s tructure\nnaturally induces a family of triposes - the implicative tripose s -\nthat encompass all triposes known so far\, namely: Heyting triposes\, \nBoolean triposes\, intuitionistic realizability triposes and classical\n realizability triposes\, thus providing a unified framework for\nexpressin g forcing and realizability\, both in intuitionistic and\nclassical logic. Finally\, I will discuss about some recent\ncompleteness results about th e very notion of implicative model\, both\nin higher-order logic and first -order logic.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /78/ END:VEVENT BEGIN:VEVENT SUMMARY:Paige North DTSTART:20230202T170000Z DTEND:20230202T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/79 DESCRIPTION:Title: Fuzzy type theory\nby Paige North as part of Topos Institute Colloquium\n\n\nAbstract\nIn this talk\, I will report on progress developing a fuzzy type theory\, a project that started as part o f the ACT 2022 Adjoint School. The motivation is to develop a logic which can model opinions\, and we do this by generalizing Martin-Löf type theor y. Martin-Löf type theory provides a system in which one can construct a proof (aka a term) of a proposition (aka a type)\, and we usually interpre t such a term as saying that the proposition holds. Fuzzy type theory is a similar system in which one can provide or construct evidence (aka a fuzz y term) to support an opinion (aka a type)\, but the evidence (fuzzy term) comes with a parameter\, for instance a real number between 0 and 1\, whi ch expresses to what extent the opinion holds. Martin-Löf type theory is closely related to category theory: from such a type system one can constr uct a category in which (very roughly) the types become objects and the te rms become morphisms\, and this can be made part of an equivalence. Thus\, we base our development of fuzzy type theory to be the thing which corres ponds to categories enriched in a category of fuzzy sets in the same way t hat Martin-Löf type theory corresponds to categories (enriched in sets).\ n\nThis is joint work with Shreya Arya\, Greta Coraglia\, Sean O’Connor\ , Hans Riess\, and Ana Tenório.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /79/ END:VEVENT BEGIN:VEVENT SUMMARY:Prakash Panangaden DTSTART:20230209T170000Z DTEND:20230209T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/83 DESCRIPTION:Title: Nuclear ideals in monoidal *-categories\nby P rakash Panangaden as part of Topos Institute Colloquium\n\n\nAbstract\nThi s talk is based on 25-year old material developed in joint work with Samso n Abramsky\nand Richard Blute. I hope that this talk will stimulate other s (any myself) to look at\nthese topics in light on modern developments. Our goal was to develop quantitative\nanalogues of the concept of binary r elations. In particular\, we were interested in\nfinding a suitable defin ition of probabilistic relations.\n\nThe formulation that we came up with arose by generalizing the notion of nuclear maps from\nfunctional analysis by defining nuclear ideals in monoidal *-categories. The compact\nclosed structure associated with the category of relations does not generalize d irectly\,\ninstead one obtains nuclear ideals.\n\nMany such categories hav e a large class of morphisms which behave as if they were part of\na compa ct closed category\, i.e. they allow one to transfer variables between the domain\nand the codomain. We introduce the notion of nuclear ideals to a nalyze these classes of\nmorphisms. In compact closed categories all morp hisms are nuclear\, and in the category of\nHilbert spaces\, the nuclear m orphisms are the Hilbert-Schmidt maps.\n\nWe also introduce two new exampl es of monoidal *-categories\, in which integration plays\nthe role of comp osition. In the first\, morphisms are a special class of distributions\,\n which we call tame distributions. The second example is based on measure and probability\nand serves as a possible candidate for probabilistic rela tions.\n\nSince our original paper was published\, other examples of this phenomenon were discovered.\nWe also explored concepts associated with tra ce ideals\, I will briefly talk about these.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /83/ END:VEVENT BEGIN:VEVENT SUMMARY:Sergey Goncharov DTSTART:20230216T170000Z DTEND:20230216T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/84 DESCRIPTION:Title: Towards a Higher-Order Mathematical Operational S emantics\nby Sergey Goncharov as part of Topos Institute Colloquium\n\ n\nAbstract\nCompositionality proofs in higher-order languages are notorio usly involved\, and general \nsemantic frameworks guaranteeing composition ality are hard to come by. In particular\, Turi and Plotkin’s \nbialgebr aic abstract GSOS framework\, which has been successfully applied to obtai n off-the-shelf \ncompositionality results for first-order languages\, so far did not apply to higher-order languages. I \nwill present a recently e merged development of the theory of abstract GSOS specifications for \nhig her-order languages\, in effect transferring the core principles of Turi a nd Plotkin’s framework to a \nhigher-order setting. In the present frame work\, the operational semantics of higher-order languages is \nrepresente d by certain dinatural transformations\, we dub higher-order GSOS laws< /b>. I will present a \ngeneral compositionality result w.r.t. the strong variant of Abramsky’s applicative bisimilarity that \napplies to all sys tems specified in this way. For presentation purposes\, I will stick to a variant of \nthe combinatory logic\, as a main vehicle.\n\nThe talk is bas ed on a recent POPL'23 paper\, which is a joint work with: Stefan Milius\, Lutz Schröder\, \nStelios Tsampas\, and Henning Urbat.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /84/ END:VEVENT BEGIN:VEVENT SUMMARY:Justin Curry DTSTART:20230302T170000Z DTEND:20230302T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/85 DESCRIPTION:Title: Algebraic and Geometric Models for Space Networki ng\nby Justin Curry as part of Topos Institute Colloquium\n\n\nAbstrac t\nIn this talk I will describe recent and ongoing work dedicated to devel oping scalable autonomous routing protocols for a future solar system wide internet. At the heart of the talk will be a description of a new coordin ate system (based on cosheaves and persistence) for time-varying graphs. I n this new coordinate system\, we can describe distances between various s pace networking scenarios\, as well as model routing (with propagation del ay) using matrix multiplication in a modified coefficient system valued in semi-rings. To demonstrate these models in practice\, we use simulations of Earth-Moon-Mars systems generated in SOAP (Satellite Orbital Analysis P rogram) ranging from 10s to 100s of nodes in size. These simulations are p art of a growing codebase being developed by SUNY Albany and NASA Glenn Re search Center under the TIMAEUS project.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /85/ END:VEVENT BEGIN:VEVENT SUMMARY:Urs Schreiber DTSTART:20230413T170000Z DTEND:20230413T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/87 DESCRIPTION:Title: Effective Quantum Certification via Linear Homoto py Types\nby Urs Schreiber as part of Topos Institute Colloquium\n\n\n Abstract\nThe intricacies of realistic — namely: of classically controll ed and (topologically) error-protected — quantum algorithms arguably mak e computer-assisted verification a practical necessity\; and yet a satisfa ctory theory of dependent quantum data types had been missing\, certainly one that would be aware of topological error-protection.\n\nTo solve this problem we present Linear homotopy type theory (LHoTT) as a programming an d certification language for quantum computers with classical control and topologically protected quantum gates\, focusing on (1.) its categorical s emantics\, which is a homotopy-theoretic extension of that of Proto-Quippe r and a parameterized extension of Abramsky et al.'s quantum protocols\, ( 2.) its expression of quantum measurement as a computational effect induce d from dependent linear type formation and reminiscent of Lee at al.'s dyn amic lifting monad but recovering the interacting systems of Coecke et al. 's "classical structures" monads.\n\nNamely\, we have recently shown that classical dependent type theory in its novel but mature full-blown form of Homotopy Type Theory (HoTT) is naturally a certification language for rea listic topological logic gates. But given that categorical semantics of Ho TT is famously provided by parameterized homotopy theory\, we had argued e arlier [Sc14] for a quantum enhancement LHoTT of classical HoTT\, now with semantics in parameterized stable homotopy theory. This linear homotopy t ype theory LHoTT has meanwhile been formally described\; here we explain i t as the previously missing certified quantum language with monadic dynami c lifting\, as announced in.\n\nConcretely\, we observe that besides its s upport\, inherited from HoTT\, for topological logic gates\, LHoTT intrins ically provides a system of monadic computational effects which realize wh at in algebraic topology is known as the ambidextrous form of Grothendieck ’s "Motivic Yoga"\; and we show how this naturally serves to code quantu m circuits subject to classical control implemented via computational effe cts. Logically this emerges as a linearly-typed quantum version of epistem ic modal logic inside LHoTT\, which besides providing a philosophically sa tisfactory formulation of quantum measurement\, makes the language validat e the quantum programming language axioms proposed by Staton\; notably the deferred measurement principle is verified by LHoTT.\n\nFinally we indica te the syntax of a domain-specific programming language QS (an abbreviatio n both for "Quantum Systems" and for "QS^0 -modules" aka spectra) which su gars LHoTT to a practical quantum programming language with all these feat ures\; and we showcase QS-pseudocode for simple forms of key algorithm cla sses\, such as quantum teleportation\, quantum error-correction and repeat -until-success quantum gates.\n\n(This is joint work with D. J. Myers\, M. Riley and H. Sati. Slides will be available at: ncatlab.org/schreiber/sho w/Quantum+Certification+via+Linear+Homotopy+Types)\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /87/ END:VEVENT BEGIN:VEVENT SUMMARY:David Corfield DTSTART:20230309T170000Z DTEND:20230309T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/88 DESCRIPTION:Title: Philosophical perspectives on category theory \nby David Corfield as part of Topos Institute Colloquium\n\n\nAbstract\nF or the whole length of my academic career\, I have looked to make philosop hical sense of (higher) category theory. My earliest interests concerned c ategory theory as a new structuralist foundational language for mathematic s and for mathematical physics. Later at the n-Category Café there were a lso attempts to make category-theoretic sense of probability theory\, lear ning theory and diagrammatic reasoning. Today\, alongside successes in log ic\, mathematics and physics\, we find a flourishing world of applied cate gory theory\, involving work in probability theory\, causal reasoning\, le arning theory\, natural language processing\, and so on. These are all top ics of profound interest to philosophy. In this talk\, I will discuss ways in which philosophy can come into a fruitful relationship with category t heory.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /88/ END:VEVENT BEGIN:VEVENT SUMMARY:Christina Vasilakopoulou DTSTART:20230323T170000Z DTEND:20230323T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/89 DESCRIPTION:Title: Dual algebraic structures and enrichment\nby Christina Vasilakopoulou as part of Topos Institute Colloquium\n\n\nAbstra ct\nIn this talk\, we will provide a detailed overview of the sometimes ca lled “Sweedler theory” for algebras and modules. This begins by establ ishing an enrichment of the category of algebras in the category of coalge bras\, as well as an enrichment of a global category of modules in a globa l category of comodules\, giving rise to a structure described as an enric hed fibration. Moreover\, by investigating a many-object generalization in volving categories and modules\, we will discuss further directions and ap plications of this framework to operadic structures.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /89/ END:VEVENT BEGIN:VEVENT SUMMARY:Simon Willerton DTSTART:20230330T170000Z DTEND:20230330T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/90 DESCRIPTION:Title: Metric spaces\, entropic spaces and convexity \nby Simon Willerton as part of Topos Institute Colloquium\n\n\nAbstract\n A certain notion of convexity of sets can be captured by a monad\, known a s a convexity monad or barycentric monad\; this is a finite version of so- called probability monads. Various authors (including Mardare-Panangaden- Plotkin\, and Fritz-Perrone) have looked at convexity/probability monads o n categories of metric spaces. The work of Fritz-Perrone can be recast in terms of enriched categories if you consider metric spaces as categories e nriched over the quantale of extended non-negative real numbers.\n\nOne ca n then do a similar thing for any 'suitably convex' quantale R and define a convexity monad on the category of R-categories. In particular\, if R i s the extended real line [-oo. oo] with the opposite order to that used in metric spaces\, then R-categories are what Lawvere called 'entropic space s' and argued gave a necessary structure for state spaces in thermodynamic s. The category of strict algebras with lax algebra maps for the convexity monad in this case is the category of convex entropic spaces with concave maps. The hope is that this connects the Lawvere approach to thermodynam ics with the recent approach of Baez-Lynch-Moeller which involves convex s paces and concave maps (without the entropic structure).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /90/ END:VEVENT BEGIN:VEVENT SUMMARY:Davide Trotta DTSTART:20230420T170000Z DTEND:20230420T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/91 DESCRIPTION:Title: Generalized existential completions and applicati ons\nby Davide Trotta as part of Topos Institute Colloquium\n\n\nAbstr act\nThis talk presents an overview of the "generalized existential comple tion" of Lawvere doctrines and its applications. I present this constructi on that freely adds (generalized) existential quantifiers to a given doctr ine and I will provide an intrinsic characterization of this notion based on an algebraic description of the logical concept of existential-free for mulas.\nThis characterization provides a useful tool to recognize a wide v ariety of examples of doctrines arising as generalized existential complet ions. These include the subobjects doctrine and the weak subobjects doctri ne as well all realizability triposes and\, among localic triposes\, only the supercoherent ones.\n\nI will also present some applications of the co nstruction to the dialectica interpretation\, showing how our algebraic de scription of quantifier-free formulas allows us to prove that the logical principles involved in the dialectica interpretation are satisfied in the categorical setting\, establishing a tight correspondence between the logi cal system and the categorical framework given by dialectica doctrines.\n\ nThis talk is based on the following works:\n\n- Maria Emilia Maietti\, Da vide Trotta (2023). A characterization of generalized existential completi ons. In Annals of Pure and Applied Logic.\n\n- Davide Trotta\, Matteo Spad etto\, Valeria de Paiva (2023). Dialectica principles via Gödel doctrines . In Theoretical Computer Science.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /91/ END:VEVENT BEGIN:VEVENT SUMMARY:Georges Gonthier DTSTART:20230427T170000Z DTEND:20230427T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/92 DESCRIPTION:Title: Foothills and cathedrals: organising the librarie s behind big proofs\nby Georges Gonthier as part of Topos Institute Co lloquium\n\n\nAbstract\nWhile mathematics is amongst the best organized fo rms of knowledge\, the level of detail of computer-assisted formal mathema tics demands an even higher degree of structuring. The cathedrals that are the computer proofs of famous results such as the Four Color or the Odd O rder theorems rest on the foothills of large\, architected libraries of pr erequisites\, ranging from the trivial and elementary to undergraduate and graduate curricula. While these can often be crafted to resemble traditio nal course material\, the extra attention to detail also motivates differe nces\, some examples of which we will highlight.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /92/ END:VEVENT BEGIN:VEVENT SUMMARY:Michael Barany DTSTART:20230504T170000Z DTEND:20230504T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/93 DESCRIPTION:Title: How Categories Come to Matter: On the history and sociology of categories in modern mathematics\nby Michael Barany as p art of Topos Institute Colloquium\n\n\nAbstract\nI will situate categories and related mathematical principles in the history of modern mathematics from the late nineteenth century to the present. The worldviews and perspe ctives adopted by the Topos Institute derive from specific transformations in the nature and scale of mathematical research over the last century-an d-a-bit. These connect the ideas of modern mathematics to its people\, ins titutions\, and infrastructures. I will consider two main senses in which categories "come to matter": first\, how categories of various kinds becam e meaningful\, salient\, and important as ways of seeing the mathematical world and and the worlds of mathematicians\; and second\, how such categor ies were encoded\, translated\, reproduced\, and made to move on and acros s various kinds of material media (i.e. physical matter) such as blackboar ds\, index cards\, and printed journals. I contend that these two senses a re historically connected\, in ways that relate to the continuing goals an d challenges of the Topos community.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /93/ END:VEVENT BEGIN:VEVENT SUMMARY:Riehl\, Bradley\, Cheng\, Dancstep\, and Lugg DTSTART:20230316T170000Z DTEND:20230316T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/94 DESCRIPTION:Title: Category theory outreach panel\nby Riehl\, Br adley\, Cheng\, Dancstep\, and Lugg as part of Topos Institute Colloquium\ n\n\nAbstract\nCategory theory is a wonderful subject\, deep and broad\, s panning the breadth of mathematics and having applications throughout scie nce\, engineering\, technology\, and the arts. But for people outside of a cademia\, it can be a difficult subject to learn. Topos Institute is hosti ng a panel discussion\, moderated by Emily Riehl\, featuring panelists who are actively involved in producing category theory books and videos for a non-expert audience. The panellists will discuss their philosophy and tec hniques\, and provide support and encouragement for others to join in this important work. They will also take questions from viewers to help people get a better handle on how they may begin to learn the subject and to hel p category theorists understand what they can do to facilitate this proces s.\n\nFor more information\, including how to submit questions\, please se e https://topos.site/ct-outreach-self-learners/\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /94/ END:VEVENT BEGIN:VEVENT SUMMARY:Chad Giusti DTSTART:20230511T170000Z DTEND:20230511T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/95 DESCRIPTION:Title: Toward a useful category for persistent homology< /a>\nby Chad Giusti as part of Topos Institute Colloquium\n\n\nAbstract\nP ersistent homology is the central tool in modern applied topology. Briefly \, given a (finite) sample from a distribution on a topological space embe dded in a metric space\, one builds a multi-scale combinatorial representa tion of the sample called a filtered Vietoris-Rips complex. Applying homol ogy\, we summarize this multi-scale structure as an object called a persis tence module. When the samples come from real-world data\, practitioners a pply domain knowledge and ad hoc reasoning to understand how the persisten ce module reflects organizational principles of the system of interest.\n\ nIf we wish to formalize this reasoning process\, or apply more sophistica ted methods from algebraic topology to data analysis\, a first step is to develop a notion of functoriality for persistent homology. This pipeline i nherits the usual functoriality of homology\, taking maps of simplicial co mplexes to maps on persistence modules\, and substantial progress has been made in cycle registration\, a formalism for comparing persistence module s using this structure. However\, in practice one usually compares samples from unknown spaces\; there are relatively few settings where the require d map of the combinatorial encodings (or underlying spaces) is likely to b e known. In this talk\, we describe our recent efforts to develop techniqu es that provide a notion of "induced map" using the kind of data reasonabl y available in applied settings\, and the challenges that remain in develo ping a full categorical framework for applied topology. Various parts of t his work are joint with Iris Yoon\, Robert Ghrist\, Niko Schonsheck\, Greg ory Henselman-Petrusek\, and Lori Ziegelmeier\, amongst others.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /95/ END:VEVENT BEGIN:VEVENT SUMMARY:Elaine Landry DTSTART:20230525T170000Z DTEND:20230525T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/96 DESCRIPTION:Title: As If Category Theory were a Foundation\nby E laine Landry as part of Topos Institute Colloquium\n\n\nAbstract\nThe aim of this talk is to show that when we shift our focus from solving philosop hical problems to solving mathematical ones\, we see that an as-if interpr etation of mathematics can be used to provide an account of both the pract ice and the applicability of mathematics. I begin first with Plato to show that much philosophical milk has been spilt owing to our conflating the m ethod of mathematics with the method of philosophy. I then use my reading of Plato to develop what I call as-ifism\, the view that\, in mathematics\ , we treat our hypotheses as if they were true first principles and we do this with the purpose of solving mathematical problems not philosophical o nes. I next extend as-ifism to modern mathematics wherein the method of ma thematics becomes the axiomatic method\, noting that this engenders a shif t from as-if hypotheses to as-if axioms. I next distinguish as-ifism from if-thenism\, and use this to develop my structural as-ifist position. I en d by showing that taking a methodological as-ifist route\, by placing our focus on what is needed for the practice and applicability of mathematics\ , we are neither committed to the unconditional consistency of our mathema tical axioms nor the unconditional truth of our background meta-mathematic al theory. Simply\, it is methodological considerations\, and not metaphys ical ones\, that “condition” our as if assumptions of both the consist ency of our mathematical axioms and the truth of our background meta-mathe matical theory. Finally\, I use my methodological as-ifism to reconsider t he “foundations debate”\, specifically\, that between set theory and c ategory theory.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /96/ END:VEVENT BEGIN:VEVENT SUMMARY:Tom Hirschowitz DTSTART:20230608T170000Z DTEND:20230608T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/97 DESCRIPTION:Title: Abstraction in programming language theory: Howe' s method\nby Tom Hirschowitz as part of Topos Institute Colloquium\n\n \nAbstract\nResearch in programming languages mostly proceeds language by\ nlanguage. This in particular means that key ideas are often introduced\nf or one typical language\, and must then be adapted to other languages.\n\n A prominent example of this is Howe's method for proving that\napplicative bisimilarity\, a notion of program equivalence in\ncall-by-name λ-calcul us\, is a congruence. This method has been adapted\nto call-by-value λ-ca lculus\, PCF\, λ-calculus with delimited\ncontinuations\, higher-order π -calculus\,…\n\nIn this work\, using category theory\, we establish an a bstract congruence\ntheorem for applicative bisimilarity\, of which most e xisting adaptations\nof Howe's method are instances.\n\nThis is joint work with Ambroise Lafont.\n\nSee also Ugo Dal Lago\, Francesco Gavazzo\, and Paul Levy. Effectful applicative bisimilarity: Monads\, relators\, and How e’s method. LICS 2017. Extended version: https://arxiv.org/abs/1704.0464 7 .\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /97/ END:VEVENT BEGIN:VEVENT SUMMARY:Taco Cohen DTSTART:20230615T170000Z DTEND:20230615T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/98 DESCRIPTION:Title: Categorical Causality & Systems Theory\nby Ta co Cohen as part of Topos Institute Colloquium\n\n\nAbstract\nCategorical Systems theory is a general framework for modelling systems whose state ev olves depending on some inputs or actions\, and which produce some observa ble outputs. This framework is general enough to describe arbitrary classi cal physical systems\, and generalizes the Partially Observed Markov Decis ion Process commonly used in AI. Causal models\, formalized as string diag rams in CD-categories\, provide a convenient high-level framework for reas oning about how intervening on some outcome variables would affect others. In this talk I will provide a high-level introduction to both frameworks\ , and discuss their relations. In particular we ask when a system can be a ccurately described by a causal model\, and show that this is not generall y possible\, thus highlighting the limitations of existing causal modellin g frameworks.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /98/ END:VEVENT BEGIN:VEVENT SUMMARY:Clark Barrett DTSTART:20230518T170000Z DTEND:20230518T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/99 DESCRIPTION:Title: Proof Certificates in Satisfiability Modulo Theor ies\nby Clark Barrett as part of Topos Institute Colloquium\n\n\nAbstr act\nSatisfiability modulo theories (SMT) is an automated reasoning paradi gm that can automatically prove a wide variety of first-order logic theore ms relating to theories that commonly occur when reasoning about computer systems (e.g.\, arithmetic\, arrays\, strings\, etc.). Together with my c olleagues at U Iowa\, Bar-Ilan\, and UF Minas Gerais\, we have for the pas t few years been developing a way to produce proof certificates from the c vc5 SMT solver. These proof certificates provide enough detail to allow a n independent proof checker to confirm the correctness of the theorem prov ed. The obvious benefit is that this drastically reduces the code that mu st be trusted to ensure correct results. A less obvious benefit is that p roof certificates open up the possibility of integrating SMT solvers into skeptical proof assistants such as Coq\, Isabelle/HOL\, or Lean. In this talk\, I will give an overview of the proof production and proof checking mechanisms we are developing for cvc5 and explain how we are leveraging th ese to provide trusted SMT automation in proof assistants.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /99/ END:VEVENT BEGIN:VEVENT SUMMARY:Alex Martsinkovsky DTSTART:20230601T170000Z DTEND:20230601T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/100 DESCRIPTION:Title: How to interpret cotorsion\nby Alex Martsink ovsky as part of Topos Institute Colloquium\n\n\nAbstract\nTwo important f eatures of a linear control system are its controllability and observabili ty. \nFrom the algebraic prospective\, a system is a module over a ring of differential operators (with constant\, polynomial\, or analytic coeffic ients). The part of the system that cannot be controlled \nis called the a utonomy of the system. In the algebraic language\, this is just the torsio n submodule \nof the module. Thus the controllable part is described by th e torsion-free quotient of the module. \n\nThere is a duality between the controllability of the system and the observability of the dual \nsystem. The goal of this talk is to propose a conjectural algebraic analog of the observability\, \ncalled cotorsion. As a justification for the conjecture\ , we will see a duality between cotorsion \nand torsion\, effected by the Auslander-Gruson-Jensen functor. The latter seems to be a \nrecurring them e\, found in a variety of functor categories. It is to be hoped that\, des pite the \nalgebraic nature of this talk\, the non-algebraic members of th e audience would recognize \nfamiliar (enriched) categorical patterns.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /100/ END:VEVENT BEGIN:VEVENT SUMMARY:Jared Culbertson DTSTART:20230622T170000Z DTEND:20230622T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/101 DESCRIPTION:Title: Applying Categorical Thinking to Practical Domai ns\nby Jared Culbertson as part of Topos Institute Colloquium\n\n\nAbs tract\nEmbracing a categorical perspective has proven to be a useful way t o formalize many intuitive and ad hoc compositional approaches across a di verse set of practical fields. In this talk\, we will discuss work in thre e primary domains including probabilistic modeling\, hierarchical clusteri ng\, and robotics. After briefly surveying prior work in the first two\, w e will focus on formalizing what it means to "apply a behavior" in a very concrete context of legged robots whose controllers are modeled as hybrid dynamical systems. Central to this approach is developing a common framewo rk for describing (i) sequential composition of hybrid systems (enabled by a cospan description of interfaces and a generalization of Conley's (epsi lon\,T)-chains to the hybrid setting)\; (ii) transformations of hybrid sys tems (modeled as hybrid semiconjugacies and integrated with sequential com position via a double category)\; and (iii) hierarchical composition of hy brid systems (where hybrid subdivisions satisfying a certain fiber product condition enable composing spans of template/anchor pairs). Throughout\, we will highlight some specific practical lessons that were learned in app lying categorical formalisms to these real-world problem domains.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /101/ END:VEVENT BEGIN:VEVENT SUMMARY:Nathaniel Osgood DTSTART:20230629T170000Z DTEND:20230629T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/103 DESCRIPTION:Title: Towards Compositional System Dynamics for Public Health\nby Nathaniel Osgood as part of Topos Institute Colloquium\n\n \nAbstract\nFor decades\, System Dynamics (SD) modeling has served as a pr ominent\, diagram-centric methodology used for public health modeling. Muc h of its strength arises from its versatile use of 3 types of diagrams\, w ith each serving both to elevate transparency across the interdisciplinary teams responsible for most impactful models\, and to reason about pattern s of system behavior. Causal loop diagrams (CLDs) are used in semi-qualita tive processes early in the modeling process and seek to support insight i nto feedback structure\, behavioral modes\, and leverage points. As model ing proceeds\, system structure diagrams further distinguish stocks (accum ulations) from flows and material from informational dependencies. Stock & flow diagrams build on that representation to characterize mathematical d ependencies\, quantify parameters and initial values for stocks\, and have been particularly widely used in scenario simulation in public health and mathematical epidemiology. While ubiquitous use of diagrams renders SD m odeling markedly effective in supporting team science and shaping stakehol ders’ mental models\, existing tools suffer from a number of shortcoming s. These include poor support for modularity\, cumbersome and obscurant m odel stratification\, and an inability to capture the relationships betwee n the 3 diagram types. Within this talk\, we describe initial progress tow ards creating a framework for compositional System Dynamics\, including th eory\, API support via StockFlow.jl within AlgebraicJulia\, and ModelColla b -- a real-time collaborative tool to support interdisciplinary teams in modularly building\, composing and flexibly analyzing Stock & Flow diagram s. Our approach separates syntax from semantics\, and characterizes diagra ms using copresheaves with a schema category. Diagram composition draws on the theory of structured cospans and undirected wiring diagrams\, and emp loys pullbacks for model stratification. Model interpretation is achieved via functorial semantics\, with ordinary differential equations being just one of several semantic domains supported. After describing the current s tate of implementation\, we describe plans for future work\, including enr iching support for CLDs\, and adding support for several computational sta tistics algorithms and additional types of structurally-informed model ana lyses. This is joint work with John Baez\, Evan Patterson\, Nicholas Mead ows\, Sophie Libkind\, Alex Alegre and Eric Redekopp.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /103/ END:VEVENT BEGIN:VEVENT SUMMARY:Urs Schreiber DTSTART:20230824T170000Z DTEND:20230824T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/104 DESCRIPTION:Title: Quantum Programming via Linear Homotopy Types\nby Urs Schreiber as part of Topos Institute Colloquium\n\n\nAbstract\nT he intricacies of realistic — namely: of classically controlled and\n(to pologically) error-protected — quantum algorithms arguably make\ncompute r-assisted verification a practical necessity\; and yet a\nsatisfactory th eory of dependent quantum data types had been missing\,\ncertainly one tha t would be aware of topological error-protection.\n\nTo solve this problem we present Linear homotopy type theory (LHoTT)\nas a programming and cert ification language for quantum computers with\nclassical control and topol ogically protected quantum gates\, focusing\non (1.) its categorical seman tics\, which is a homotopy-theoretic\nextension of that of Proto-Quipper a nd a parameterized extension of\nAbramsky et al.'s quantum protocols\, (2. ) its expression of quantum\nmeasurement as a computational effect induced from dependent linear\ntype formation and reminiscent of Lee at al.‘s d ynamic lifting monad\nbut recovering the interacting systems of Coecke et al.‘s "classical\nstructures" monads.\n\nNamely\, we have recently shown that classical dependent type theory in\nits novel but mature full-blown form of Homotopy Type Theory (HoTT) is\nnaturally a certification language for realistic topological logic\ngates. But given that categorical semant ics of HoTT is famously\nprovided by parameterized homotopy theory\, we ha d argued earlier\n[Sc14] for a quantum enhancement LHoTT of classical HoTT \, now with\nsemantics in parameterized stable homotopy theory. This linea r\nhomotopy type theory LHoTT has meanwhile been formally described\; here \nwe explain it as the previously missing certified quantum language\nwith monadic dynamic lifting\, as announced in.\n\nConcretely\, we observe tha t besides its support\, inherited from HoTT\,\nfor topological logic gates \, LHoTT intrinsically provides a system of\nmonadic computational effects which realize what in algebraic topology\nis known as the ambidextrous fo rm of Grothendieck’s “Motivic Yoga”\;\nand we show how this naturall y serves to code quantum circuits subject\nto classical control implemente d via computational effects. Logically\nthis emerges as a linearly-typed q uantum version of epistemic modal\nlogic inside LHoTT\, which besides prov iding a philosophically\nsatisfactory formulation of quantum measurement\, makes the language\nvalidate the quantum programming language axioms prop osed by Staton\;\nnotably the deferred measurement principle is verified b y LHoTT.\n\nFinally we indicate the syntax of a domain-specific programmin g\nlanguage QS (an abbreviation both for “Quantum Systems” and for “ QS^0\n-modules” aka spectra) which sugars LHoTT to a practical quantum\n programming language with all these features\; and we showcase\nQS-pseudoc ode for simple forms of key algorithm classes\, such as\nquantum teleporta tion\, quantum error-correction and\nrepeat-until-success quantum gates.\n \n(This is joint work with D. J. Myers\, M. Riley and H. Sati.\nSlides wil l be available at:\nncatlab.org/schreiber/show/Quantum+Certification+via+L inear+Homotopy+Types)\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /104/ END:VEVENT BEGIN:VEVENT SUMMARY:Jonathan Sterling DTSTART:20230928T170000Z DTEND:20230928T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/105 DESCRIPTION:Title: Synthetic Domains in the 21st Century\nby Jo nathan Sterling as part of Topos Institute Colloquium\n\n\nAbstract\nIt is easy to teach a student how to give a naïve denotational semantics to a typed lambda calculus without recursion\, and then use it to reason about the equational theory: a type might as well be a set\, and a program might as well be a function\, and equational adequacy at base type is establish ed using a logical relation between the initial model and the category of sets. Adding any non-trivial feature to this language (e.g. general recurs ion\, polymorphism\, state\, etc.) immediately increases the difficulty be yond the facility of a beginner: to add recursion\, one must replace sets and functions with domains and continuous maps\, and to accommodate polymo rphism and state\, one must pass to increasingly inaccessible variations o n this basic picture.\n\nThe dream of the 1990s was to find a category tha t behaves like SET in which even general recursive and effectful programmi ng languages could be given naïve denotational semantics\, where types ar e interpreted as “sets” and programs are interpreted as a “functions ”\, without needing to check any arduous technical conditions like conti nuity. The benefit of this synthetic domain theory is not only that it loo ks “easy” for beginners\, as more expert-level constructions like powe rdomains or even domain equations for recursively defined semantic worlds become simple and direct. Although there have been starts and stops\, the dream of synthetic domain theory is alive and well in the 21st Century. To day’s synthetic domain theory is\, however\, both more modular and more powerful than ever before\, and has yielded significant results in program ming language semantics including simple denotational semantics for an sta te of the art programming language with higher-order polymorphism\, depend ent types\, recursive types\, general reference types\, and first-class mo dule packages that can be stored in the heap.\n\nIn this talk\, I will exp lain some important classical results in synthetic domain theory as well a s more recent results that illustrate the potential impact of “naïve de notational semantics” on the life of a workaday computer scientist.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /105/ END:VEVENT BEGIN:VEVENT SUMMARY:Nat Shankar DTSTART:20230831T170000Z DTEND:20230831T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/106 DESCRIPTION:Title: Abstraction Engineering with the Prototype Verif ication System (PVS)\nby Nat Shankar as part of Topos Institute Colloq uium\n\n\nAbstract\nLogic has always played a central role in computing. One successful\napplication of logic is its use in specifying and modeling \ncomputational behavior\, and in proving properties of computation\nsyste ms. SRI's PVS was released thirty years ago with the goal of\ndemocratizi ng interactive theorem proving by combining an expressive\nformalism with powerful automated reasoning tools for building and\nmaintaining complex f ormalizations and proofs. We describe some of\nthe features of PVS for de fining and reasoning with mathematical\nabstractions and bridging the gap between informal and formalized\nmathematical discourse. PVS features an expressive-order logic with\nalgebraic/coalgebraic datatypes\, dependent p redicate subtypes\, and\nparametric theories. The interactive theorem pro ver employs a range\nof automated proof strategies for simplification\, re writing\, and case\nanalysis\, along with built-in decision procedures for SAT and SMT\nsolving. The applicative fragment of PVS can be viewed as a \nfunctional programming language\, and efficient executable code can be\n generated in Common Lisp and C\, among other languages. PVS includes\next ensive libraries spanning a range of topics in mathematics and\ncomputing. The talk is an informal overview of the underlying\ntheoretical foundati ons\, and the proof and code generation\ncapabilities of PVS.\n\nBio: Dr. Natarajan Shankar is a Distinguished Senior Scientist and SRI\nFellow at t he SRI Computer Science Laboratory. He received a\nB.Tech. degree in Elec trical Engineering from the Indian Institute of\nTechnology\, Madras\, and Ph.D. in Computer Science from the University\nof Texas at Austin. He is the author of the book\, "Metamathematics\,\nMachines\, and Godel's Proof "\, published by Cambridge University Press.\nDr. Shankar is the co-develo per of a number of technologies including\nthe PVS interactive proof assis tant\, the SAL model checker\, the Yices\nSMT solver\, and the Arsenal sem antic parser. He is a co-recipient of\nthe 2012 CAV Award and the recipie nt of the 2022 Herbrand Award.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /106/ END:VEVENT BEGIN:VEVENT SUMMARY:Brandon Shapiro DTSTART:20231102T170000Z DTEND:20231102T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/107 DESCRIPTION:Title: (Higher) category theory in Cat^#\nby Brando n Shapiro as part of Topos Institute Colloquium\n\n\nAbstract\nThe double category Cat^#\, which can be built out of polynomial comonads\, provides a computation-friendly mathematical language for categorical database theo ry\, effects handlers in programming\, and discrete open dynamical systems . It has categories as objects\, cofunctors as arrows\, and prafunctors as pro-arrows. Monads among prafunctors\, such as the free category monad on graphs\, have algebras including categories\, n-categories (strict or wea k)\, double categories\, multicategories (symmetric or plain)\, monoids\, monoidal categories (of nearly any variety)\, and in fact any algebraic no tion of higher category whose definition is of a particular form. I will i ntroduce the Cat^# approach to defining (higher) categories and survey som e constructions from (higher) category theory that can be expressed in the language of Cat^#\, including higher categorical nerves and "algebraic pr afunctors" such as the free monoidal category monad on Cat.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /107/ END:VEVENT BEGIN:VEVENT SUMMARY:Simona Paoli DTSTART:20231019T170000Z DTEND:20231019T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/108 DESCRIPTION:Title: Simplicial delta versus fat delta in higher cate gory theory\nby Simona Paoli as part of Topos Institute Colloquium\n\n \nAbstract\nMany structures in higher category theory have been described using the combinatorics of simplicial objects\, based on the category simp licial delta. A prototype example is that a category can be described as a simplicial set satisfying appropriate conditions (the so called Segal con ditions) via the nerve functor.\nIn dimension two\, simplicial objects in Cat can be used to describe strict 2-categories and double categories. Amo ng the latter\, one can identity the category of weakly globular double ca tegories which gives a model of weak 2-categories via a new paradigm to we aken higher categorical structures: the notion of weak globularity.\nThe f at delta\, introduced by Joachim Kock\, carries some intuition similar to the simplicial delta\, yet it has a different and rich structure. Kock use d it to define fair 2-categories\, encoding weak 2-categories with strict composition laws.\nIn this talk I illustrate a direct comparison between f air 2-categories and weakly globular double categories which enables to in terpret the weak globularity condition in terms of weak units. This compar ison is based on a rich interplay between the simplicial delta and the fat delta\, and on several novel properties of the latter.\nI will finally ex plain the significance of this result in terms of potential higher dimensi onal generalizations.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /108/ END:VEVENT BEGIN:VEVENT SUMMARY:Julie Bergner DTSTART:20231207T170000Z DTEND:20231207T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/109 DESCRIPTION:Title: Models for (∞\,n)-categories with discreteness conditions\nby Julie Bergner as part of Topos Institute Colloquium\n\ n\nAbstract\nThere are two ways of turning Segal spaces into models for up -to-homotopy categories\, or (∞\,1)-categories: either asking that the s pace of objects be discrete\, or requiring Rezk's completeness condition. When generalizing to higher (∞\,n)-categories\, both of these approache s have been taken to multisimplicial models\, in the form of Segal n-categ ories and n-fold complete Segal spaces\, but models given by Θ_n-diagrams have focused on the completeness conditions. In this talk\, we'll discus s how to get a Θ_n-model with discreteness conditions\, but also address the question of when these conditions can be mixed and matched with one an other.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /109/ END:VEVENT BEGIN:VEVENT SUMMARY:Leonardo de Moura DTSTART:20230907T170000Z DTEND:20230907T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/110 DESCRIPTION:Title: Lean 4: Empowering the Formal Mathematics Revolu tion and Beyond\nby Leonardo de Moura as part of Topos Institute Collo quium\n\n\nAbstract\nThis talk presents Lean 4\, the latest version of the Lean proof assistant\, and its impact on the mathematical community. We f irst introduce the project's design and objectives\, followed by the missi on of the newly established Lean Focused Research Organization (FRO).\nThe advent of Lean and similar proof assistants has sparked a transformation in mathematical practice\, an era we refer to as the "Formal Mathematics R evolution". We'll explore how Lean 4 contributes to this revolution\, with its tools and structures enabling mathematicians to formalize complex the ories and proofs with unprecedented ease. A key aspect of our philosophy i s facilitating decentralized innovation. We discuss the strategies employe d to empower a diverse community of researchers\, developers\, and enthusi asts to contribute to formalized mathematics.\nWe will also delve into the usage of Lean as a functional programming language. With Lean 4\, we have not only created an environment for formalizing mathematics but also an e ffective tool for writing software\, enabling a smooth interaction between mathematical and computational aspects. Finally\, we will look ahead\, sh aring our vision and planned steps for the future of Lean 4 and the Lean F RO. We'll discuss how we aim to further grow the user base\, continue impr oving usability\, and deepen the reach of formal methods into mathematics and computer science.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /110/ END:VEVENT BEGIN:VEVENT SUMMARY:Dominic Orchard DTSTART:20231012T170000Z DTEND:20231012T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/111 DESCRIPTION:Title: Programming for the Planet\nby Dominic Orcha rd as part of Topos Institute Colloquium\n\n\nAbstract\nClimate change is one of the greatest challenges of our time. Assessing its risks and our pr ogress towards mitigating its worst effects requires a wealth of data abou t our natural environment that we rapidly process into accurate indicators \, assessments\, and predictions\, with sufficient trust in the resulting insights to make decisions that affect the lives of billions worldwide\, b oth now and in the future. However\, in the last decade\, climate modellin g has faced diminishing returns from current hardware trends and software techniques. Furthermore\, developing the required models and analysis tool s to effectively process\, explore\, archive\, and derive policy decisions \, with a high degree of transparency and trust\, remains difficult. I arg ue that more cross-disciplinary effort between mathematics\, computer scie nce\, software engineering\, and data science is needed to help close the gap between where we are and where we need to be. I will discuss our work at the Institute of Computing for Climate Science and the critical role of programming in addressing the needs of climate science. I will also make connections to relevant areas of category theory which could be leveraged to develop more flexible climate models in the future.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /111/ END:VEVENT BEGIN:VEVENT SUMMARY:Michael Levin DTSTART:20230921T170000Z DTEND:20230921T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/112 DESCRIPTION:Title: Emergent Selves and Unconventional Intelligences : where philosophy and engineering meet\nby Michael Levin as part of T opos Institute Colloquium\n\n\nAbstract\nWe are composites\, made out an a gential material. In this talk\, I \nwill describe how molecular pathways\ , cells\, tissues\, and organs display \nintelligence - problem-solving an d creative behavior in a variety of \ndiverse problem spaces. I will descr ibe evolutionary aspects of this \namazing multiscale competency architect ure\, and how the cognition of \ncells scales up to the grandiose goals of morphogenetic\, behavioral\, and \nlinguistic collectives. I will show da ta from my lab that uses \ndevelopmental biophysics\, computer science\, a nd behavioral science to \nunderstand diverse intelligence and work toward s practical\, biomedical \napplications of these ideas (in areas of regene ration birth defects\, and \ncancer). I will also describe our synthetic l ife forms\, which we use to \nunderstand the latent space of goals for col lective systems without an \nevolutionary history.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /112/ END:VEVENT BEGIN:VEVENT SUMMARY:Tom Leinster DTSTART:20231026T170000Z DTEND:20231026T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/113 DESCRIPTION:Title: Entropy and diversity: the axiomatic approach\nby Tom Leinster as part of Topos Institute Colloquium\n\n\nAbstract\nEc ologists have been debating the best way to measure diversity for more\nth an 70 years. The concept of diversity is relevant not only in ecology\,\nb ut also in other fields such as genetics and economics\, as well as being\ nclosely related to information entropy. \n\nThe question of how best to q uantify diversity has surprising mathematical\ndepth. Indeed\, a general s tudy of invariants resembling cardinality and\nEuler characteristic led to the unifying notion of the magnitude of an\nenriched category - a quantit y which is also closely related to the maximum\ndiversity of a community o f prescribed species. I will give a high-level\noverview of the concepts o f entropy\, diversity and magnitude\, and how they\nfit together.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /113/ END:VEVENT BEGIN:VEVENT SUMMARY:Maurice Chiodo DTSTART:20231116T170000Z DTEND:20231116T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/114 DESCRIPTION:Title: Normalising ethical reasoning for mathematicians \nby Maurice Chiodo as part of Topos Institute Colloquium\n\n\nAbstrac t\nIn the past 10 years there has been a significant increase in the level of attention on issues of ethical and responsible development in mathemat ics. "Ethics in Mathematics" is now a recognised area of study\, and there are now substantially more resources to consult on this. However\, such u nderstanding has not yet permeated into the minds of the bulk of mathemati cians. Most either have minimal realisation of the need to consider ethica l and societal issues when carrying out mathematical work\, or lack the sk ill set needed to carry out such thinking in a thorough and systematic way . In short: most mathematicians either don't know how to spot ethical issu es\, or don't know what to do when they have.\nIn this talk I will aim to address both of these `blindspots' for mathematicians. I will present my " Teaching Resources for Embedding Ethics in Mathematics" (arXiv:2310.08467) \, which is a tool to embed ethics in mathematics teaching by way of mathe matical exercises that normalise ethical considerations. I will also prese nt my "Manifesto for the Responsible Development of Mathematical Works" (a rXiv:2306.09131)\, which is a tool to help mathematicians dissect their wo rkflow and identify the points at which their actions and choices may lead to harmful consequences. In short: train mathematicians to think about et hics all the time\, then educate them on what to do when they identify suc h issues.\nThese are joint works with Dennis Müller\, and form part of th e Cambridge University Ethics in Mathematics Project (ethics.maths.cam.ac. uk).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /114/ END:VEVENT BEGIN:VEVENT SUMMARY:John Cartmell DTSTART:20240118T170000Z DTEND:20240118T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/115 DESCRIPTION:Title: Aspects of a Mathematical Theory of Data\nby John Cartmell as part of Topos Institute Colloquium\n\n\nAbstract\nI will discuss significant aspects of a theory of data and what may be achieved by representing data specifications as sketches of Range Categories with additional structure. I will discuss the distinction between relational an d non-relational physical data specifications and contrast physical and lo gical data specifications. I will discuss goodness criteria for such speci fications and define some specific criteria which generalise the classic r elational goodness criteria i.e. the so called normal forms of Codd\, Fagi n\, Ling and Goh and others.\n\nMy goal for a fully elaborated Mathematica l Theory of Data is to effect a change in what is considered best practice for the way in which data is specified and programmed as as to enable bes t practice to be shifted from being at the level that data is physically r epresented and communicated to being at the more abstract level of its log ical structure.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /115/ END:VEVENT BEGIN:VEVENT SUMMARY:Minhyong Kim DTSTART:20231130T170000Z DTEND:20231130T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/116 DESCRIPTION:Title: Who Owns Mathematics: A Question of Identity \nby Minhyong Kim as part of Topos Institute Colloquium\n\n\nAbstract\nAt a recent conference on the global history of mathematics\, a question was raised about the recurrence of Euclid in a number of the talks and the 'We stern' bias that seemed to appear in a meeting that was concerned with glo bal history. In this talk\, I will discuss the misconceptions around the i dentities of historical figures like Euclid\, the deep-rooted confusion su rrounding ancient identities in general\, and why it might be important fo r mathematicians of our times to be aware of them.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /116/ END:VEVENT BEGIN:VEVENT SUMMARY:Susan Niefield DTSTART:20240208T170000Z DTEND:20240208T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/117 DESCRIPTION:Title: Cauchy Completeness and Adjoints in Double Categ ories\nby Susan Niefield as part of Topos Institute Colloquium\n\n\nAb stract\nIn his 1973 paper (TAC Reprints\, 2002)\, Lawvere observed that a metric space Y is a category enriched in the extended reals\, and showed t hat Y is Cauchy complete if and only if every bimodule (i.e.\, profunctor) with codomain Y has a right adjoint. More recently\, Paré (2021) conside red adjoints and Cauchy completeness in double categories\, and showed tha t an (S\,R)-bimodule M has a right adjoint in the double category of commu tative rings if and only if it is finitely generated and projective as an S-module. It is well known that the latter property characterizes the exis tence of a left adjoint to tensoring with M on the category of S-modules\, and this was generalized to rigs and quantales in a 2017 paper by Wood an d the speaker.\n\nThis talk consists of two parts. First\, after recalling the relevant definitions\, we present examples of Cauchy complete objects in some "familiar" double categories. Second\, we incorporate the two abo ve mentioned projectivity results into a version of the 2017 theorem with Wood which we then apply to (not-necessarily commutative) rings\, rigs\, a nd quantales.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /117/ END:VEVENT BEGIN:VEVENT SUMMARY:Juan Pablo Vigneaux DTSTART:20240125T170000Z DTEND:20240125T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/118 DESCRIPTION:Title: Cohomological aspects of information\nby Jua n Pablo Vigneaux as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk will discuss the cohomological aspects of information functions with in the framework of information cohomology (first introduced by Baudot and Bennequin in 2015). Several known functionals can be identified as cohomo logy classes in this framework\, including the Shannon entropy of discrete probability measures and the differential entropy and underlying dimensio n of continuous measures. I’ll try to provide an accessible overview of the foundations of the theory\, which should require only a basic familiar ity with category theory and homological algebra\, and survey the main kno wn results. Finally\, I'll discuss some perspectives and open problems: fi rstly in connection with Renyi's information dimension and other (possibly geometric) invariants of laws taking values on manifolds\, and secondly w ith notions of entropy for categories (akin to Leinster's diversity of met ric spaces).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /118/ END:VEVENT BEGIN:VEVENT SUMMARY:André Joyal DTSTART:20231214T170000Z DTEND:20231214T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/119 DESCRIPTION:Title: Higher topos theory and Goodwillie Calculus\ nby André Joyal as part of Topos Institute Colloquium\n\n\nAbstract\nLuri e's higher topos theory is a vast extension of Grothendieck's topos theory . I will compare the two theories\, stressing similarities and differences . The fact that the ∞-category of parametrised spectra is a higher topos has no analog in Grothendieck topos theory. It is the first stage of the Goodwillie tower associated to any left exact localization of a higher top os. The tower can be understood in analogy with the completion tower of a n ideal in a commutative ring. For many purposes\, a topos has the dual as pects of a space (the topos) and of a ring (the logos). The category of lo goi (=the opposite of the category of topoi) has many properties in common with the category of commutative rings.\n\nIn collaboration with Mathieu Anel\, Georg Biedermann and Eric Finster.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /119/ END:VEVENT BEGIN:VEVENT SUMMARY:Robert Paré DTSTART:20240111T170000Z DTEND:20240111T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/120 DESCRIPTION:Title: The functorial difference operator\nby Rober t Paré as part of Topos Institute Colloquium\n\n\nAbstract\nAs a tool for studying the structure of endofunctors F of Set\, \nwe introduce the diff erence operator△\n\n△[F](X) = F(X + 1) \\ F(X).\n\nThis is analogous t o the classical difference operator for real\nvalued functions\, a discret e form of the derivative.\n\nThe \\ above is set difference and can't be expected to be functorial\,\nbut it is for a large class of functors\, th e taut functors of Manes\, \nwhich include polynomial functors and many mo re.\n\nWe obtain combinatorial versions of classical identities\, often\n' 'improved'. Many examples will be given.\n\nThe talk should be accessible to everyone. The only prerequisite \nis some very basic category theory.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /120/ END:VEVENT BEGIN:VEVENT SUMMARY:André Joyal DTSTART:20240215T170000Z DTEND:20240215T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/121 DESCRIPTION:Title: Free bicompletion of categories revisited (part 1)\nby André Joyal as part of Topos Institute Colloquium\n\n\nAbstrac t\nWhitman's theory of free lattices can be extended to free lattices enri ched over a quantales\, to free bicomplete enriched categories and even to free bicomplete enriched oo-categories. It has applications to the semant ic of Linear Logic (Hongde Hu and J.)\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /121/ END:VEVENT BEGIN:VEVENT SUMMARY:Joachim Kock DTSTART:20240222T170000Z DTEND:20240222T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/122 DESCRIPTION:Title: Polynomial functors — from elementary arithmet ic to infinity-operads\nby Joachim Kock as part of Topos Institute Col loquium\n\n\nAbstract\nIn their simplest form\, polynomial functors are en dofunctors of the category of sets built from sums and products. At first they can be considered a categorification of the notion of polynomial func tion\, but it has turned out the theory of polynomial functors is more gen erally an efficient toolbox for dealing with induction\, nesting\, and sub stitution. The talk will highlight some of these aspects in combinatorics\ , logic\, and homotopy theory.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /122/ END:VEVENT BEGIN:VEVENT SUMMARY:Steven Clontz DTSTART:20240328T170000Z DTEND:20240328T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/123 DESCRIPTION:Title: Sociotechnical infrastructure for mathematics re search\nby Steven Clontz as part of Topos Institute Colloquium\n\n\nAb stract\nThe National Science Foundation defines "cyberinfrastructure" as " the hardware\, software\, networks\, data and people that underpin today's advanced computing technology"\, particularly technologies that advance s cientific discovery. In particular\, this infrastructure is incomplete wit hout its "people"\, leading some to prefer the terminology "sociotechnical infrastructure" to emphasize the importance of how these technologies con nect human researchers\, and how human researchers in turn use and develop these technologies in order to create new knowledge. In mathematics resea rch\, even theoretical mathematics\, we use many technologies\, and engage with many different communities\, but there is little scholarship on the ad hoc research infrastructure itself that we implicitly rely on from day to day. This talk will provide an overview of some of the work I've done a s part of my spring 2024 sabbatical dedicated to the research and developm ent of improved sociotechnical infrastructure for mathematics research.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /123/ END:VEVENT BEGIN:VEVENT SUMMARY:Po-Shen Loh DTSTART:20240404T170000Z DTEND:20240404T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/124 DESCRIPTION:Title: Uniting Game Theory\, Math Stars\, and Actors To Build Human Intelligence in the AI Age\nby Po-Shen Loh as part of Top os Institute Colloquium\n\n\nAbstract\nOne of the central challenges of be yond-standard-curriculum instruction (such as "gifted" education) is how t o achieve equitably-distributed scale. Making matters worse\, generative AI such as ChatGPT is increasingly adept at solving standard curricular ta sks\, so it is urgent to scalably deliver teaching that goes beyond curren t standards. Fortunately\, there is an area close to math which devises so lutions in which problems solve themselves even through self-serving human behavior: Game Theory.\n\nThe speaker will describe his recent work\, whi ch uses Game Theory to create a novel alignment of incentives\, which conc urrently solves pain points in disparate sectors. At the heart of the inno vation is a new\, mutually-beneficial cooperation between high school math stars and professionally trained actors and comedians. This creates a hig hly scalable community of extraordinary coaches with sufficient capacity t o teach large numbers of middle schoolers seeking to learn critical thinki ng and creative analytical problem solving (https://live.poshenloh.com). A t the same time\, it creates a new pathway for high school math stars to s ignificantly strengthen their emotional intelligence. The whole program is conducted virtually\, so it reaches through geographical barriers. The sp eaker will also share his experience extending this work to build talent d evelopment pipelines in underprivileged communities\, identifying and supp orting highly motivated middle school students who otherwise did not have access to coaching.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /124/ END:VEVENT BEGIN:VEVENT SUMMARY:Rodrigo Ochigame DTSTART:20240815T170000Z DTEND:20240815T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/125 DESCRIPTION:Title: The Automation of Mathematics from an Anthropolo gical Perspective\nby Rodrigo Ochigame as part of Topos Institute Coll oquium\n\n\nAbstract\nThis talk will examine some aspects of the ongoing a utomation of mathematical research from an anthropological perspective. It will first address the diversity of practical standards of proof (across fields\, places\, and times)\, the longstanding tension between “underst anding” and mechanical “checking\,” and the persistent need for soci al adjudication even for computer-encoded (“formal”) proofs. It will t hen discuss how automation might affect divisions of labor\, economies of credit\, institutional hierarchies\, and structures of incentive and rewar d in professional research. The talk will also draw comparisons to current debates about automation and machine learning in other fields of science\ , such as experimental physics.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /125/ END:VEVENT BEGIN:VEVENT SUMMARY:Gioele Zardini DTSTART:20240425T170000Z DTEND:20240425T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/126 DESCRIPTION:Title: Co-Design of Complex Systems: From Autonomy to F uture Mobility\nby Gioele Zardini as part of Topos Institute Colloquiu m\n\n\nAbstract\nWhen designing complex systems\, we need to consider mult iple trade-offs at various abstraction levels and scales\, and choices of single components need to be studied jointly. For instance\, the design of future mobility solutions (e.g.\, autonomous vehicles\, micromobility) an d the design of the mobility systems they enable are closely coupled. Inde ed\, knowledge about the intended service of novel mobility solutions woul d impact their design and deployment process\, while insights about their technological development could significantly affect transportation manage ment policies. Optimally co-designing sociotechnical systems is a complex task for at least two reasons. On one hand\, the co-design of interconnect ed systems (e.g.\, large networks of cyber-physical systems) involves the simultaneous choice of components arising from heterogeneous natures (e.g. \, hardware vs. software parts) and fields\, while satisfying systemic con straints and accounting for multiple objectives. On the other hand\, compo nents are connected via collaborative and conflicting interactions between different stakeholders (e.g.\, within an intermodal mobility system). In this talk\, I will present a framework to co-design complex systems\, leve raging a monotone theory of co-design and tools from applied category theo ry. The framework will be instantiated in the task of designing future mob ility systems\, all the way from the policies that a city can design\, to the autonomy of vehicles as part of an autonomous mobility-on-demand servi ce. Through various case studies\, I will show how the proposed approaches allow one to efficiently answer heterogeneous questions\, unifying differ ent modeling techniques and promoting interdisciplinarity\, modularity\, a nd compositionality. I will then discuss open challenges for compositional systems design optimization\, and present my agenda to tackle them.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /126/ END:VEVENT BEGIN:VEVENT SUMMARY:Mason Porter DTSTART:20240627T170000Z DTEND:20240627T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/127 DESCRIPTION:Title: Topological Data Analysis of Spatial Systems \nby Mason Porter as part of Topos Institute Colloquium\n\n\nAbstract\nI w ill discuss topological data analysis (TDA)\, which uses ideas from topolo gy to quantify the "shape" of data. I will focus in particular on persiste nt homology (PH)\, which one can use to find "holes" of different dimensio ns in data sets. I will briefly introduce these ideas and then discuss a s eries of examples of TDA of spatial systems. The examples that I'll discus s include voting data\, the locations of polling sites\, and the webs of s piders under the influence of various drugs.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /127/ END:VEVENT BEGIN:VEVENT SUMMARY:Nicola Gambino DTSTART:20240523T170000Z DTEND:20240523T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/128 DESCRIPTION:Title: Monoidal bicategories\, differential linear logi c\, and analytic functors\nby Nicola Gambino as part of Topos Institut e Colloquium\n\n\nAbstract\nThe aim of this talk is to present bicategoric al counterparts of the notions of a linear explonential comonad\, as consi dered in the study of linear logic\, and of a codereliction transformation \, introduced in the study of differential linear logic via differential c ategories. As an application\, the differential calculus of Joyal's analyt ic functors will be extended to analytic functors between presheaf categor ies\, in a way that is analogous to how ordinary calculus extends from a s ingle variable to many variables. This is based on joint work with Marcelo Fiore and Martin Hyland (https://arxiv.org/abs/2405.05774).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /128/ END:VEVENT BEGIN:VEVENT SUMMARY:Spencer Breiner DTSTART:20240905T170000Z DTEND:20240905T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/129 DESCRIPTION:Title: Polynomial Interfaces\nby Spencer Breiner as part of Topos Institute Colloquium\n\n\nAbstract\nI will argue that appli ed category theory would benefit\, both practically and strategically\, fr om greater attention to user interface. Starting from some very basic exam ples\, I will discuss some of the conceptual challenges in this area and e xplain how they map onto categorical structures like monads\, comonads and polynomial functors. I will close with a discussion of the Semagrams use r interface library\, its goals and future prospects.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /129/ END:VEVENT BEGIN:VEVENT SUMMARY:Eugenio Moggi DTSTART:20240509T170000Z DTEND:20240509T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/130 DESCRIPTION:Title: Categories of Classes for Collection Monads\ nby Eugenio Moggi as part of Topos Institute Colloquium\n\n\nAbstract\nIn 1998 Manes introduced the notion of collection monad on the category of se ts as a suitable semantics for collection types. The canonical example of collection monad is the finite powerset monad.\n\nIn order to account for the algorithmic aspects the category of sets should be replaced with othe r categories\, whose arrows are maps computable by "low complexity" algori thms.\n\nWe extends Manes' definition of collection monad to models for we ak versions of Algebraic Set Theory (AST). AST was proposed by Joyal and Moerdijk in the '90 as a category-theoretic counterpart of Bernays' set th eory based on classes.\n\nWe give a systematic way to construct such model s\, which include\ncategories whose arrows are "low complexity" functions between countable sets.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /130/ END:VEVENT BEGIN:VEVENT SUMMARY:Will Crichton DTSTART:20240822T170000Z DTEND:20240822T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/131 DESCRIPTION:Title: How to Make Mathematicians Into Programmers (And Vice Versa)\nby Will Crichton as part of Topos Institute Colloquium\n \n\nAbstract\nTools for formalized mathematics (FM)\, such as proof assist ants and model checkers\, are increasingly capable of handling the real-wo rld problems of both mathematicians and software developers. Yet\, these t ools are only as effective as the people who use them. The FM community cl early needs to invest in better education and better tooling. But... which curricula are actually effective for learners? What tooling will actually make users more productive? In this talk\, I will lay out some preliminar y ideas for how to systematically investigate these questions\, i.e.\, dev elop a science of human factors for FM. My core proposal is to combine exp erimental psychological methods (e.g.\, lab studies\, IDE telemetry) and c ognitive theories (e.g.\, working memory\, mental models) to study how peo ple use FM tools. Then that understanding can be applied to make principle d predictions about the efficacy of curricula\, tooling\, and language des ign.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /131/ END:VEVENT BEGIN:VEVENT SUMMARY:Elena Di Lavore DTSTART:20240516T170000Z DTEND:20240516T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/132 DESCRIPTION:Title: Effectful trace semantics via effectful streams< /a>\nby Elena Di Lavore as part of Topos Institute Colloquium\n\n\nAbstrac t\nEffectful streams are a coinductive semantic universe for effectful dat aflow programming and traces. As an example\, we formalise the stream ciph er cryptographic protocol. In monoidal categories with conditionals and ra nges\, effectful streams particularize to families of morphisms satisfying a causality condition. Effectful streams allow us to develop notions of t race and bisimulation for effectful Mealy machines\; bisimulation implies effectful trace equivalence.\n\nThis is recent joint work with Filippo Bon chi and Mario Román.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /132/ END:VEVENT BEGIN:VEVENT SUMMARY:Edward Lee DTSTART:20240418T170000Z DTEND:20240418T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/133 DESCRIPTION:Title: Certainty or Intelligence: Pick One!\nby Edw ard Lee as part of Topos Institute Colloquium\n\n\nAbstract\nMathematical models can yield certainty\, as can probabilistic models where the probabi lities degenerate. The field of formal methods emphasizes developing such certainty about engineering designs. In safety critical systems\, such cer tainty is highly valued and\, in some cases\, even required by regulatory bodies. But achieving reasonable performance for sufficiently complex envi ronments appears to require the use of AI technologies\, which resist such certainty. This talk suggests that certainty and intelligence may be fund amentally incompatible.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /133/ END:VEVENT BEGIN:VEVENT SUMMARY:Steve Vickers DTSTART:20240530T170000Z DTEND:20240530T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/134 DESCRIPTION:Title: The Fundamental Theorem of Calculus: point-free< /a>\nby Steve Vickers as part of Topos Institute Colloquium\n\n\nAbstract\ nPoint-free topology is known in various guises (locales\, formal topology )\, but can be boiled down to a procedure of defining the points of a spac e not (“point-set”) as elements of a set\, but as models of a logical theory. This is for a constrained “geometric” logic\, so that the open s of the space correspond to propositional formulae derived from the theor y: thus the theory defines both the points and the topology. Then continui ty of maps just means that they are constructed in accordance with the con straints of the logic.\n\nWhy bother to do topology that way? After all\, the logic is even more constrained than constructive reasoning\, and we st ill don’t know how far it reaches.\n\nThe first reason is that it quite painlessly extends to toposes\, viewed as generalized spaces. This uses th e machinery of classifying toposes\, but only in an unobtrusive way [1]. M any proper classes can then be viewed as point-free spaces - just write do wn a geometric theory whose models are the elements of the class.\n\nThe s econd reason follows from the first but can then be applied back to ungene ralized spaces in a very natural treatment of bundles. Theory presentation s can themselves be described as the models of a geometric theory\, and th is allows us to view bundles as continuously mapping base points to spaces (the fibres). For physics in particular\, this invites exploration of how much can be done using geometric methods. See eg [2].\n\nMeanwhile\, ther e is the question of how much ordinary mathematics\, and in particular rea l analysis\, can be done in this style. I present as a case study the Fund amental Theorem of Calculus [3]. This illustrates some typically geometric features of the reasoning\, such as attention paid to one-sided reals and the use of hyperspaces and their analogues\, and some exploitation of the geometric fact that everything is continuous\, as well as a cute new tric k using uniform probability measures.\n\n[1] Steven Vickers “Topical cat egories of domains”\, Mathematical Structures in Computer Science 9 (199 9)\n[2] Bas Spitters\, Steven Vickers and Sander Wolters “Gelfand spectr a in Grothendieck toposes using geometric mathematics"\, Electronic Procee dings in Theoretical Computer Science 158 (2014)\n[3] Steven Vickers “Th e Fundamental Theorem of Calculus point-free\, with applications to expone ntials and logarithms"\, arXiv:2312.05228\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /134/ END:VEVENT BEGIN:VEVENT SUMMARY:Alex Simpson DTSTART:20240606T170000Z DTEND:20240606T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/135 DESCRIPTION:Title: Three toposes for probability and randomness \nby Alex Simpson as part of Topos Institute Colloquium\n\n\nAbstract\nI s hall give a brief guided tour of three toposes that have arisen in a resea rch programme to model aspects of probability and randomness from a topos perspective. The first topos of "probability sheaves" supports a syntheti c style of probabilistic reasoning about random variables. The second "ran dom topos" makes sense of the notion of "random element" and models a wor ld in which all sets are measurable. The third topos of "random probabilit y sheaves" combines the previous two and provides a home for a more radica l style of "synthetic probability theory" expunged of all concerns about s igma-algebras\, measurability and the like.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /135/ END:VEVENT BEGIN:VEVENT SUMMARY:Kathrin Stark DTSTART:20240801T170000Z DTEND:20240801T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/136 DESCRIPTION:Title: On Taming Differentiable Logics\nby Kathrin Stark as part of Topos Institute Colloquium\n\n\nAbstract\nFor performance and verification in machine learning\, new methods have recently been pro posed that optimise learning systems to satisfy formally expressed logical properties. Among these methods\, differentiable logics (DLs) are used to translate propositional or first-order formulae into loss functions deplo yed for optimisation in machine learning. At the same time\, recent attemp ts to give programming language support for verification of neural network s showed that DLs can be used to compile verification properties to machin e-learning backends. This situation is calling for stronger guarantees abo ut the soundness of such compilers\, the soundness and compositionality of DLs\, and the differentiability and performance of the resulting loss fun ctions. In this talk\, I report on recent work to 1.) give uniform semanti cs to and 2.) to formalise existing DLs using the Mathematical Components library in the Coq proof assistant. This work is meant as a stepping stone for the development of programming language support for verification of m achine learning.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /136/ END:VEVENT BEGIN:VEVENT SUMMARY:Filippo Bonchi DTSTART:20240502T170000Z DTEND:20240502T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/137 DESCRIPTION:Title: Diagrammatic Algebra of First Order Logic\nb y Filippo Bonchi as part of Topos Institute Colloquium\n\n\nAbstract\nWe i ntroduce the calculus of neo-Peircean relations\, a string diagrammatic ex tension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. The axioms are obtained by combining two well known categorical structures: cartesia n and linear bicategories.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /137/ END:VEVENT BEGIN:VEVENT SUMMARY:Bartosz Milewski DTSTART:20240613T170000Z DTEND:20240613T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/139 DESCRIPTION:Title: Parametric Profunctor Preoptics\nby Bartosz Milewski as part of Topos Institute Colloquium\n\n\nAbstract\nLocally grad ed categories and parametric optics provide a compositional model of neura l networks. I will show how to generalize this approach to pre-optics. I'l l introduce a parametric profunctor representation of preoptics and use it to implement a perceptron in Haskell.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /139/ END:VEVENT BEGIN:VEVENT SUMMARY:Cyrus Omar DTSTART:20240829T170000Z DTEND:20240829T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/140 DESCRIPTION:Title: Totally Live Programming and Proving in Hazel\nby Cyrus Omar as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk will review progress on the Hazel programming environment and its un derlying theoretical developments. Hazel is the first totally live typed g eneral-purpose programming environment\, meaning that it deploys error loc alization and recovery mechanisms\, rooted in language-theoretic developme nts\, that ensure that every editor state is syntactically well-structured and statically and dynamically meaningful. The talk will review the under lying theory and include a live demonstration of various Hazel features\, including its editor\, training mode\, and its stepper\, which is forming the basis for ongoing work on a Hazel-based theorem prover. The talk will also discuss various other ongoing and future directions of interest to th e community\, including our vision for a "computational commons" that oper ates like a planetary-scale live program.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /140/ END:VEVENT BEGIN:VEVENT SUMMARY:Seth Frey DTSTART:20240926T170000Z DTEND:20240926T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/141 DESCRIPTION:Title: Online communities as model systems for commons governance\nby Seth Frey as part of Topos Institute Colloquium\n\n\nAb stract\nThe best citizens of a large-scale democracy are those who have bu ilt and broken several small ones to see how they work. By empowering peop le to build any kind of community together\, the Internet has become a lab oratory for self-governance experimentation. Groups who start online commu nities must overcome the challenges of recruiting finite resources around difficult common goals. Fortunately\, they can draw on a growing range of support technologies\, peer networks\, and scholarship. With their transp arency\, the Internet's millions of online communities can be surveyed for insights into their design and functioning. Looking at three large platfo rms for small self-governing online communities\, we will pose several que stions of institutional processes at the population level\, as drawn from the literatures on common-pool resource management and institutional analy sis and design.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /141/ END:VEVENT BEGIN:VEVENT SUMMARY:Arthur J Parzygnat DTSTART:20240808T170000Z DTEND:20240808T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/142 DESCRIPTION:Title: A generalization of inversion using Bayes' rule with applications to quantum\nby Arthur J Parzygnat as part of Topos I nstitute Colloquium\n\n\nAbstract\nBayes' rule has recently been given a c ategorical definition in terms of string diagrams due to Cho and Jacobs. T his definition of Bayesian inversion\, however\, is not robust enough for categories that include reasoning about quantum systems due to the no-clon ing theorem. In this talk\, I will explain how semi-cartesian categories ( which have less structure than Markov categories) provide a suitable frame work to define Bayesian inversion categorically. In particular\, I will pr ovide axioms for such an abstract form of Bayesian inversion. It remains a n open question whether these axioms characterize Bayesian inversion for q uantum systems.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /142/ END:VEVENT BEGIN:VEVENT SUMMARY:Fabio Gadducci DTSTART:20240711T170000Z DTEND:20240711T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/143 DESCRIPTION:Title: From gs-monoidal to cartesian categories: a stru ctural analysis\nby Fabio Gadducci as part of Topos Institute Colloqui um\n\n\nAbstract\nIt is now folklore that cartesian categories can be view ed as symmetric monoidal ones equipped with two natural transformations\, modelling diagonals and projections. In this talk we explore the taxonomy obtained by relaxing the naturality requirement\, from gs-monoidal/cd-cate gories to restriction and Markov ones. We show how these possibly order-en riched categories are related by suitable commutative monads and the shape of the arrows of the free categories generated by an algebraic signature. \n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /143/ END:VEVENT BEGIN:VEVENT SUMMARY:Amélia Liao DTSTART:20241003T170000Z DTEND:20241003T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/145 DESCRIPTION:Title: Cubical types for the working formalizer\nby Amélia Liao as part of Topos Institute Colloquium\n\n\nAbstract\nCubical type theory is an extension of dependent type theory designed\n to make t he univalence principle *provable*\, rather than an axiom.\n Then\, by wha t is essentially a happy coincidence\, it also provides a\n design for wor king with higher inductive types and with coinductive\n types.\n\n However \, the tradeoff for these features is a hit to usability: In\n practice\, the user of cubical type theory is directly exposed to the\n complicated p rimitive operations that let us implement these higher\n features\, even i f they're working on set-level mathematics. Worse\, any\n implementation o f HoTT imposes additional proof obligations to stay in\n the realm of sets rather than escaping off into coherence purgatory.\n\n This talk discusse s the experience of using cubical type theory to\n build the 1Lab— in pa rticular\, the automation we've been building so\n the end-user of the lib rary does not have to memorise the cubical type\n theory papers if all the y want is to formalise traditional\,\n low-homotopy level mathematics.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /145/ END:VEVENT BEGIN:VEVENT SUMMARY:Thomas Powell DTSTART:20241016T170000Z DTEND:20241016T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/146 DESCRIPTION:Title: Quantitative results for stochastic processes\nby Thomas Powell as part of Topos Institute Colloquium\n\n\nAbstract\nI t is an elementary fact from real analysis that any monotone bounded seque nce of real numbers converges. It turns out that the monotone convergence theorem can be given an equivalent finitary formulation: roughly that any sufficiently long monotone bounded sequence experiences long regions where the sequence is metastable. This so-called "finite convergence principle" is carefully motivated and discussed by Terence Tao in a 2007 blog post ( 'Soft analysis\, hard analysis\, and the finite convergence principle')\, but was already known to proof theorists\, where the use of logical method s to both finitize infinitary statements and provide uniform quantitative information for the finitary versions plays a central role in the so-calle d proof mining program.\n\nThe goal of my talk is to discuss how methods f rom proof mining can be applied to the theory of stochastic processes\, an area of mathematics hitherto unexplored from this perspective. I will beg in by discussing the simple monotone convergence principle\, and will then focus on how everything I mentioned above can be generalised to the analo gous result in the stochastic setting: Doob's martingale convergence theor ems. This then sets the groundwork for new applications of proof theory in stochastic optimization\, and I will give a high level overview of some w ork in progress in this direction\, including a quantitative analysis of t he famous Robbins-Siegmund lemma. This is all joint work with my PhD stude nt Morenikeji Neri.\n\nIn giving the talk I will not assume any knowledge of proof theory\, just some elementary analysis and probability theory.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /146/ END:VEVENT BEGIN:VEVENT SUMMARY:Christine Tasson DTSTART:20240912T170000Z DTEND:20240912T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/149 DESCRIPTION:Title: Semantics for Reactive Probabilistic Programming \nby Christine Tasson as part of Topos Institute Colloquium\n\n\nAbstr act\nSynchronous languages are now a standard industry tool for critical e mbedded systems. Designers write high-level specifications by composing st reams of values. These languages have been extended with Bayesian reasonin g to program state-space models which compute a stream of distributions gi ven a stream of observations [1].\n\nThis talk aims at describing semantic s for probabilistic synchronous languages\, based on a joint work with Gui llaume Baudart and Louis Mandel [2]. The key idea is to interpret probabil istic expressions as a stream of un-normalized density functions which map s random variable values to a result and positive score. Two equivalent se mantics are presented: the co-iterative semantics is executable while the relational semantics is easy to use for proving program equivalence. The s emantical framework is then applied to prove the correctness of a program transformation required to run an optimized inference algorithm.\n\n[1] Re active Probabilistic Programming\, Guillaume Baudart et al\, PLDI 2020\n[2 ] Density-Based Semantics for Reactive Probabilistic Programming\, Guillau me Baudart\, Louis Mandel\, Christine Tasson\, arxiv:2308.01676\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /149/ END:VEVENT BEGIN:VEVENT SUMMARY:Chris Fields DTSTART:20240919T170000Z DTEND:20240919T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/150 DESCRIPTION:Title: What is the Identity operator?\nby Chris Fie lds as part of Topos Institute Colloquium\n\n\nAbstract\nThe idea that obj ects have associated Identity morphisms\, or operators\, is fundamental to mathematics\, physics\, and the theory of Active Inference. All of these\ , moreover\, support the idea that identity can be maintained via multiple paths. We will explore the relationship between the idea of identity and the notions of space\, time\, and memory\, with an emphasis on how these l atter three relate to the idea of an object in both physical theory and ac tive inference.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /150/ END:VEVENT BEGIN:VEVENT SUMMARY:Mario Román DTSTART:20241031T170000Z DTEND:20241031T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/151 DESCRIPTION:Title: Partial Markov Categories\nby Mario Román a s part of Topos Institute Colloquium\n\n\nAbstract\nPartial Markov categor ies are an algebra and syntax for Bayesian inference. They use a string di agrammatic syntax—with a formal correspondence to programs—to reason a bout continuous and discrete probability\, decision problems (Monty Hall\, Newcomb's)\, the compositional properties of normalization\, and an abstr act Bayes' theorem.\n\nPartial Markov categories are a careful blend of Ma rkov categories (from categorical probability theory) and cartesian restri ction categories (from the algebraic theory of partial computations). We w ill discuss the construction\, theory\, and applications of partial Markov categories.\n\nThis is joint work with Elena Di Lavore. It is based on "E vidential Decision Theory via Partial Markov Categories"\, presented at Li CS'23 (https://arxiv.org/abs/2301.12989).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /151/ END:VEVENT BEGIN:VEVENT SUMMARY:Carl Miller DTSTART:20241107T170000Z DTEND:20241107T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/152 DESCRIPTION:Title: Graphical Methods in Quantum Cryptography\nb y Carl Miller as part of Topos Institute Colloquium\n\n\nAbstract\nMathema tical security proofs are crucial in the field of cryptography: they allow us to base the theoretical security of a particular protocol on a set of simply-stated assumptions. However\, a major challenge (in both education and research) is managing the complexity of these proofs. Fully rigorous security proofs can occupy a lot of space even when the underlying ideas are relatively simple. In the subfield of quantum cryptography\, which in corporates quantum states and processes\, this challenge has additional co mplications.\n\nVisual reasoning helps illuminate proofs in cryptography\, and in some cases\, visual reasoning can actually serve as a replacement for symbolic reasoning. In this talk I will discuss how picture-proofs\, based on categorical quantum mechanics\, can be incorporated into quantum cryptography.\n\nReferences:\n\n- Breiner\, Spencer\, Carl A. Miller\, and Neil J. Ross. "Graphical methods in device-independent quantum cryptograp hy." Quantum 3 (2019): 146. arXiv:1705.09213\n\n- Breiner\, Spencer\, Ami r Kalev\, and Carl Miller. "Parallel Self-Testing of the GHZ State with a Proof by Diagrams." 15th International Conference on Quantum Physics and L ogic. Electronic Proceedings in Theoretical Computer Science (EPTCS)\, 201 8. arXiv:1806.04744\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /152/ END:VEVENT BEGIN:VEVENT SUMMARY:Arezoo Islami DTSTART:20241114T170000Z DTEND:20241114T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/153 DESCRIPTION:Title: Unravelling the "Unreasonable Effectiveness" of Mathematics\nby Arezoo Islami as part of Topos Institute Colloquium\n\ n\nAbstract\nThe Applicability Problem is the problem of explaining why ma thematics is applicable to the empirical sciences. This problem is revived and reformulated by the physicist Eugene Wigner under the striking title "The Unreasonable Effectiveness of Mathematics in the Natural Sciences". I n this influential work\, Wigner argues that the applicability of mathemat ics is a miracle\, "a wonderful gift which we neither understand nor deser ve". Responses to this problem range from metaphysical claims about the ma thematical structure of the universe to epistemic claims about the nature of human cognition\, as well as formalist views that characterize mathemat ics as a type of game.\n\nIn my view\, to find an explanation for this rel ationship\, we must first understand the explanandum itself. More fundamen tal than the why-question (why is mathematics applicable in the natural sc iences) is the how-question (how is mathematics applicable in the natural sciences). By examining how mathematics has been used across different era s and fields within the natural sciences\, we can begin to understand the relationship between mathematics and the sciences. More importantly\, this exploration allows us to address questions regarding the nature of mathem atics as it is used and practiced. By distinguishing pseudo-problems from the genuine problems of applicability\, we open new paths for philosophica l reflections on the nature of mathematics and the sciences.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /153/ END:VEVENT BEGIN:VEVENT SUMMARY:Matthew Akamatsu DTSTART:20241205T170000Z DTEND:20241205T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/156 DESCRIPTION:Title: Collective grassroots knowledge generation with lab discourse graphs\nby Matthew Akamatsu as part of Topos Institute C olloquium\n\n\nAbstract\nScientific research teams face persistent challen ges in coordinating their work and synthesizing collective knowledge into models across projects and labs. Discourse graphs offer a solution by bre aking scientific research into its atomic components - questions\, claims\ , and evidence - and connecting them in a semantic graph. In our cell bio logy lab\, we have implemented discourse graphs as a coordination layer fo r collective research and model building. Lab members use the graphs to i dentify open research questions\, maintain focus on their chosen hypothese s while documenting new results\, and share discrete findings with clear p rovenance and context. Researchers report streamlined thinking\, better o rientation toward their target question\, and a sense of accomplishment fr om contributing tangible\, reusable results. This collaborative approach h as allowed the lab to organically evolve its scientific models through bot tom-up knowledge synthesis. Our new user pilot aims to extend these benef its through accessible tooling and interoperable graphs\, thereby enabling collective grassroots knowledge generation and sensemaking across researc h communities.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /156/ END:VEVENT BEGIN:VEVENT SUMMARY:Eswaran Subrahmanian and Yves Keraron DTSTART:20241212T170000Z DTEND:20241212T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/157 DESCRIPTION:Title: Engineering practice and the potential role of C T in systems engineering\nby Eswaran Subrahmanian and Yves Keraron as part of Topos Institute Colloquium\n\n\nAbstract\nIn this talk\, we will i llustrate the role of information structures in engineering practices. In a particular case\, we will instantiate an example of the required structu res and their interaction in the systems engineering process. We will then identify Categorical representations that could formalize the models embe dded in systems engineering standards and support their composition. The t alk is not mathematical but an attempt to map the needs of systems enginee ring modeling to potential categorical representations that serve the purp ose of engineering practices.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /157/ END:VEVENT BEGIN:VEVENT SUMMARY:Nina Otter DTSTART:20250313T170000Z DTEND:20250313T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/158 DESCRIPTION:Title: (Co)algebraic analysis of social systems: from g raphs to hypergraphs\nby Nina Otter as part of Topos Institute Colloqu ium\n\n\nAbstract\nThe algebraic analysis of social systems\, or algebraic social network analysis\, refers to a collection of methods designed to e xtract information about the structure of social systems modelled as direc ted graphs. Central among these are methods to determine the roles that ex ist within a given system\, namely compound relations\, and the social pos itions\, which one can think of as groups of similarly connected actors. I n these methods the focus is on pairwise relationships between social acto rs\, which are modelled through directed graphs. \nThe importance of highe r-order relationships in the modelling of social systems has received cons iderable interest in recent years. In this talk I will explain how we can use the theory of universal coalgebra to formalise these notions for graph s\, generalise them to models of social systems that also take into accoun t higher-order interactions between social actors\, such as hypergraphs\, and finally tie together the analyses of social roles and positions throug h a functoriality result. \n\nThe talk is based on joint work with Nima Mo tamed and Emily Roff.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /158/ END:VEVENT BEGIN:VEVENT SUMMARY:Paul-Andre Mellies DTSTART:20250206T170000Z DTEND:20250206T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/159 DESCRIPTION:Title: The rabbit calculus: convolution products on dou ble categories and categorification of rule algebra\nby Paul-Andre Mel lies as part of Topos Institute Colloquium\n\n\nAbstract\nReporting on rec ent joint work with Nicolas Behr and Noam Zeilberger\, I will describe the rabbit calculus\, a convolution product over presheaves of double categor ies motivated by term and graph rewriting. As I will explain\, the convolu tion product generalizes to any double category the usual Day tensor produ ct of presheaves of monoidal categories. An interesting aspect of the cons truction is that the resulting convolution product is in general only opla xl associative. Therefore\, I will identify several classes of double cate gories for which the convolution product is not only oplax associative\, b ut fully associative. These include framed bicategories on the one hand\, and double categories of term and graph rewriting on the other. For the la tter\, we establish a formula that justifies the view that the convolution product categorizes the rule algebra product\, and captures the basic int uitions of causality in rewriting theory.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /159/ END:VEVENT BEGIN:VEVENT SUMMARY:Jason Gross DTSTART:20241024T170000Z DTEND:20241024T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/160 DESCRIPTION:Title: Compact Proofs: Measuring Quality of Understandi ng with a Compression-Based Metric\nby Jason Gross as part of Topos In stitute Colloquium\n\n\nAbstract\nThe field of mechanistic interpretabilit y – techniques for reverse engineering model weights into human-interpre table algorithms – seeks to compress explanations model behavior. By stu dying tiny transformers trained to perform algorithmic tasks\, we can make rigorous the extent to which various understandings of a model permit com pressing an explanation of its behavior.\n\nIn this talk\, I’ll discuss how we prototyped this approach in our paper where formally proved lower b ounds on the accuracy of 151 small transformers trained on a Max-of-K task \, creating 102 different computer-assisted proof strategies to assess the ir length and tightness of bound on each of our models. Using quantitative metrics\, we found that shorter proofs seem to require and provide more m echanistic understanding. Moreover\, we found that more faithful mechanist ic understanding leads to tighter performance bounds.\n\nWe identified com pounding structureless noise as the leading obstacle to generating more co mpact proofs of tighter performance bounds. I plan to discuss ongoing work to address this challenge by either relaxing the worst-case constraint en forced by using proofs\; or by fine-tuning partially-interpreted models to align more closely with our explanations.\n\nI’ll conclude by discussin g the roadmap I see to scaling the compact proofs approach to rigorous mec h interp up to frontier models.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /160/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrew Dudzik DTSTART:20250213T170000Z DTEND:20250213T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/161 DESCRIPTION:Title: Tensor Species: The Theory and Practice of Neura l Networks\nby Andrew Dudzik as part of Topos Institute Colloquium\n\n \nAbstract\nAs category theory grows in popularity within the machine lear ning community\, those of us interested in both theory and practice are fa ced with the question: which abstractions are directly useful when innovat ing in the design of neural networks? We explain why this is a hard proble m\, while making use of Joyal’s theory of species to give a down-to-eart h description of the data types we see in contemporary neural networks\, p aying close attention to performance.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /161/ END:VEVENT BEGIN:VEVENT SUMMARY:Adrian Miranda DTSTART:20250130T170000Z DTEND:20250130T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/162 DESCRIPTION:Title: Kleisli constructions for pseudomonads\nby A drian Miranda as part of Topos Institute Colloquium\n\n\nAbstract\nThe pas sage from a monad (A\,S) to its category of algebras (resp. category of fr ee algebras) can be seen as a V = Cat weighted limit (resp. colimit) const ruction [1]. The colimit case also has a description involving maps of the form X -->SY and the so-called Kleisli composition. \n\nWhen we move to t he two-dimensional setting\, the 2-category of pseudoalgebras can be seen as a V= Gray enriched weighted limit [2]\, but neither of the familiar des criptions of the Kleisli category categorify to give a weighted colimit [3 ]. We give a third\, less well-known description of the Kleisli category w hich does categorify to the pseudomonad setting to give a weighted colimit . We show that comparisons induced by pseudoadjunctions splitting the pseu domonad are biequivalences if and only if their left pseudoadjoints are bi essentially surjective on objects. This allows the more familiar Kleisli c onstructions for pseudomonads to be seen as tricategorical colimits\, and for the development of the formal theory of pseudomonads pt. 2.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /162/ END:VEVENT BEGIN:VEVENT SUMMARY:B. Scot Rousse DTSTART:20250320T170000Z DTEND:20250320T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/163 DESCRIPTION:Title: Language\, Technology\, & Care\nby B. Scot R ousse as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk explo res "care" as a missing dimension in contemporary discussions on technolog y\, using debates around LLMs and AI alignment as a case study. Our civili zation’s technological prowess is largely identified with abstraction an d optimization—powers that have yielded immense benefits but which have also reshaped our relationship with reality. Increasingly\, our drive to a bstract and optimize takes on a life of its own\, leading both technologis ts and non-technologists alike to engage with the world primarily through questions of modeling\, measurement\, and control. But what we care about cannot be appropriately tended to in such an instrumental framework\, for it lacks a defined ultimate goal\, a why for which we model\, measure\, an d control. Our challenge is designing how to pursue technological progress within a broader context of care\, not mere "values" that are relative to imperatives of efficiency and optimization.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /163/ END:VEVENT BEGIN:VEVENT SUMMARY:Nathanael Arkor DTSTART:20250403T170000Z DTEND:20250403T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/164 DESCRIPTION:Title: A (virtual) double category theorist's perspecti ve on polynomials\nby Nathanael Arkor as part of Topos Institute Collo quium\n\n\nAbstract\nI shall tell the tale of how I came to understand pol ynomials. In doing so\, I will exhibit a novel universal property of the d ouble category of polynomials in a locally cartesian closed category. In f act\, we shall see how polynomials may be liberated from the assumption of exponentiability entirely. This talk is based on joint work with Bryce Cl arke.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /164/ END:VEVENT BEGIN:VEVENT SUMMARY:Joe Moeller DTSTART:20250227T170000Z DTEND:20250227T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/165 DESCRIPTION:Title: A categorical approach to Lyapunov stability \nby Joe Moeller as part of Topos Institute Colloquium\n\n\nAbstract\nIn h is 1892 thesis\, Lyapunov developed a method for certifying the stability of an equilibrium point $x^*$ of a dynamical system without actually havin g to solve the differential equations. He showed that if you can construct a function $V$ (now called a *Lyapunov function*) on the state space whic h is both positive definite relative to $x^*$ and always decreasing in the direction the system is pointing\, then $x^*$ is necessarily (asymptotica lly) stable. The theory and methodology built on Lyapunov's theorem form t he foundations for modern nonlinear control.\n\nIn this talk\, we present a categorical framework in which we can develop a generalization of Lyapun ov theory. This comes in two parts: coalgebras of an endofunctor play the role of dynamical systems in a category\, and internal monoid actions play the role of solutions of these systems. We prove a generalization of Lyap unov's theorem in this framework\, namely\, that an equilibrium point of a coalgebra is stable if there is a *Lyapunov morphism*. This generalizatio n allows us to recover both the classical continuous and discrete time ver sions of Lyapunov's theorem\, as well as for dynamics in Lawvere metric sp aces and more generally quantale-enriched categories.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /165/ END:VEVENT BEGIN:VEVENT SUMMARY:Matteo Capucci DTSTART:20250306T170000Z DTEND:20250306T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/166 DESCRIPTION:Title: Representable Behaviour in Double Categorical Sy stems Theory\nby Matteo Capucci as part of Topos Institute Colloquium\ n\n\nAbstract\nCategory theory has a long history of being applied to the study of general systems. Double Categorical Systems Theory (DCST) condens es many lessons learned along the way regarding compositional structures f or the representation of systems\, their behaviour and the interaction of these two aspects. In this talk I'll revisit old and new wisdom regarding functorial behaviour of systems represented by a category of timepieces\, and prove old and new compositionality theorems for them.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /166/ END:VEVENT BEGIN:VEVENT SUMMARY:Kate Fleming DTSTART:20250410T170000Z DTEND:20250410T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/167 DESCRIPTION:Title: Beyond Tech Solutionism: Challenges of unlocking under-served community knowledge\nby Kate Fleming as part of Topos In stitute Colloquium\n\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /167/ END:VEVENT BEGIN:VEVENT SUMMARY:Kristine Bauer DTSTART:20250501T170000Z DTEND:20250501T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/168 DESCRIPTION:Title: Distillation systems as models of homotopy colim its\nby Kristine Bauer as part of Topos Institute Colloquium\n\n\nAbst ract\nThis is joint work with Kathryn Hess\, Brenda Johnson and Julie Rasm usen.\n\nColimits (and limits) are among the most fundamental notions in c ategory theory\, and also among the most useful of the basic structures. I n topology\, colimits are used to “glue” spaces together. However\, pr oblems arise when we try to work with spaces as they continuously deform\, because colimits are not invariant under such deformations. In this case\ , one uses a related notion called a homotopy colimit. But what are these\ , really? Homotopy colimits do not satisfy a universal property\, even in the homotopy category\, and are usually defined by the way they are comput ed in particular types of categories\, such as model categories. In joint work\, Hess and Johnson identified a list of properties that one would exp ect homotopy limits to satisfy in any homotopical category. These properti es were chosen carefully because they are needed to perform certain constr uctions in functor calculus. Building on their work\, we have identified t he categorical structures that govern these properties. A distillation sys tem relates two actions of the category of small categories on the categor y of categories through a lax linear functor. In this talk\, I will define distillation systems and explain when they do and don’t recover homotop y colimits.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /168/ END:VEVENT BEGIN:VEVENT SUMMARY:Juergen Jöst DTSTART:20250327T170000Z DTEND:20250327T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/169 DESCRIPTION:Title: Geometric principles of data visualization\n by Juergen Jöst as part of Topos Institute Colloquium\n\n\nAbstract\nMany machine learning algorithms try to visualize high dimensional metric data in 2D in such a way that the essential geometric and topological features of the data are highlighted. Recent schemes like the popular UMAP depend on sophisticated mathematical tools from Riemannian geometry and category theory. We develop and improve the mathematical theory in a rigorous way\, leading to an improved algorithm\, IsUMap. The category theoretical found ations include Spivak's fuzzy simplicial sets\, and they also offer a link to Topological Data Analysis. They provide a conceptual tool for merging different generalized metric structures\, and we will also put them in a w ider context.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /169/ END:VEVENT BEGIN:VEVENT SUMMARY:Robert Brandom DTSTART:20250619T170000Z DTEND:20250619T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/170 DESCRIPTION:Title: Articulating the Structure of Reasons: Logical E xpressivism and Implication-Space Semantics\nby Robert Brandom as part of Topos Institute Colloquium\n\n\nAbstract\nSemantic inferentialism unde rstands the propositional contents expressed by declarative sentences in t erms of the role those sentences play in the material relations of implica tion and incompatibility that are implicit in practices of offering some s entences as expressing reasons for or against others. Reason relations in this sense can be expressed mathematically both proof-theoretically and mo del-theoretically. Standard versions of these metainferential vocabularies depend on strong structural assumptions about the reason relations they c odify\, though. In particular\, specifically logical consequence is monoto nic and transitive. However\, those structural conditions incorporated in logical and semantic metavocabularies are not in general satisfied by the implication relations appealed to in reasoning outside of broadly mathemat ical contexts. \n\nI present both a sequent-calculus specifications of a v ersion of classical logic and an implication-space model-theoretic specifi cations of conceptual roles (based on Girard's phase-space semantics for l inear logic) that is sound and complete for that logic\, which have the ex pressive power to make explicit even radically substructural constellation s of reason relations. A top-down relational approach\, which starts with the goodness of implications and advances to their ranges of subjunctive r obustness\, turns out to be much more expressively powerful in substructur al contexts than a bottom-up atomistic approach that begins with truth val ues of sentences and advances to their truth conditions.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /170/ END:VEVENT BEGIN:VEVENT SUMMARY:Bart Jacobs DTSTART:20250417T170000Z DTEND:20250417T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/172 DESCRIPTION:Title: Update rules of Pearl and Jeffrey\nby Bart J acobs as part of Topos Institute Colloquium\n\n\nAbstract\nThis presentati on describes the two different rules for probabilistic updating\, associat ed with Pearl and with Jeffrey. The difference emerges in the presence of updating with multiple data items that one wishes to learn from (update wi th). It will be sketched how Jeffrey's rule is used in a classical algorit hm in machine learning\, namely Expectation Maximisaton.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /172/ END:VEVENT BEGIN:VEVENT SUMMARY:Amar Hadzihasanovic DTSTART:20250508T170000Z DTEND:20250508T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/174 DESCRIPTION:Title: Combinatorial foundation for planar string diagr ams\nby Amar Hadzihasanovic as part of Topos Institute Colloquium\n\n\ nAbstract\nI will explain how diagrammatic sets can serve as a combinatori al and computational foundation for 2-dimensional string diagrams\, altern ative to and as expressive as the topological foundation given by Joyal an d Street. Since diagrammatic proofs formalised as diagrams in diagrammatic sets can be interpreted not just in a 2-category or bicategory\, but more generally in an (infty\, n)-category\, this is a painless way to extend t heir applicability.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /174/ END:VEVENT BEGIN:VEVENT SUMMARY:Samson Abramsky DTSTART:20250515T170000Z DTEND:20250515T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/175 DESCRIPTION:Title: Duality for complete atomic partial Boolean alge bras\nby Samson Abramsky as part of Topos Institute Colloquium\n\n\nAb stract\nPartial Boolean algebras are an abstraction of projectors on Hilbe rt space ("quantum propositions") introduced by Kochen and Specker in thei r fundamental work on contextuality and the non-classicality of quantum me chanics.\nRather than the orthomodular lattice structure emphasized in mos t work on quantum logic\, partial Boolean algebras reflect non-commutativi ty by partiality: conjunction is only defined for compatible elements (cor responding to commuting projectors).\n\nThe classic Stone-type duality res ults for Boolean algebras\, which build dual spaces of points\, do not ap ply to partial Boolean algebras\, since the import of the Kochen-Specker t heorem is precisely that in the cases of greatest interest\, they have no points.\nWe develop a novel duality theory for the case of (complete) atom ic Boolean algebras.\nWhereas the classical Lindenbaum-Tarski duality is b etween CABA and Set\, we build a duality between pCABA (complete atomic pa rtial Boolean algebras) and a certain category of exclusivity graphs. The total case corresponds to the complete graphs\, where the relation is clas sical apartness (the negation of equality). The morphisms are certain rela tions between these graphs\, again specializing to the usual total case of functions.\nThis can be seen as a form of non-commutative duality.\n\nWe discuss the wider context of these results\, and prospects for a fully com positional quantum logic.\n\n(Joint work with Rui Soares Barbosa)\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /175/ END:VEVENT BEGIN:VEVENT SUMMARY:Daniel Polani DTSTART:20250529T170000Z DTEND:20250529T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/176 DESCRIPTION:Title: Organisation of the Information Flow in the Perc eption-Action Loop\nby Daniel Polani as part of Topos Institute Colloq uium\n\n\nAbstract\nAgents interact with their environment primarily throu gh their perception-action loop. One way to look at this interaction is to consider it as the exchange of information\, specifically\, Shannon infor mation. In my talk\, I will discuss how that is done\, how this relates to the structure of how the agent interacts with their environment (a high-l evel view of so-called "embodiment") and a number of phenomena that can be understood through this perspective. It turns out that the embodiment or agent/environment interaction imposes substantial structure onto the infor mation flow\, in addition to the fundamental structural constraints that d etermine the relation between the agent and its environment.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /176/ END:VEVENT BEGIN:VEVENT SUMMARY:Pierre-Louis Curien DTSTART:20250626T170000Z DTEND:20250626T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/177 DESCRIPTION:Title: Opetopic shapes\, combinatorially\nby Pierre -Louis Curien as part of Topos Institute Colloquium\n\n\nAbstract\n(dedica ted to the memory of Marek Zawadowski\, both a friend and a very smart sci entist)\n\nOpetopes and opetopic sets were introduced by Baez and Dolan at the end of the previous millenium as a framework for dealing with higher structures and higher coherences. \nThey are many-to-one shapes in all dim ensions and can be represented in different ways:\nabstractly through the iterated so-called plus or slice construction on polynomial monads\, and m ore concretely as zoom complexes (Kock-Joyal-Batanin-Mascari)\, or as some suitable oriented posets of faces as in the works of Zawadowski. In a ser ies of works\, Louise Leclerc\, and Louise Leclerc and myself have laid do wn precise isomorphisms between these combinatorial presentations\, adding one in the picture: opetopes as epiphytes\, which are recursively defined as trees whose nodes and edges are decorated with codimension 1 and 2 epi phytes\, respectively\, and are arguably most faithful to the original abs tract setting. The talk will offer a (gentle) journey through these (quite involved) combinatorial descriptions (epiphytes\, zoom complexes\, orient ed face structures).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /177/ END:VEVENT BEGIN:VEVENT SUMMARY:Brendan Fong DTSTART:20250710T170000Z DTEND:20250710T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/178 DESCRIPTION:Title: Abstractions for Real People\nby Brendan Fon g as part of Topos Institute Colloquium\n\n\nAbstract\nComputing is built on abstractions. Abstractions forget details\, so that we can focus on wha t is important. What happens\, however\, when we forget something of value ? I argue that certain risks and fears around AI today result from action informed by abstractions that diverge from what matters in their context o f use. Moreover\, I suggest that building better societal practices of abs traction is a task to which mathematicians – especially category theoris ts – are well placed to contribute. To begin a conversation\, I envision a practice of abstraction that prizes accessibility\, responsiveness\, an d pluralism. I’ll illustrate this practice via ongoing work at Topos\, e specially our collaborative modelling platform CatColab.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /178/ END:VEVENT BEGIN:VEVENT SUMMARY:Rory Lucyshyn-Wright DTSTART:20250424T170000Z DTEND:20250424T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/179 DESCRIPTION:Title: V-graded categories as a setting for enrichment and actions of monoidal categories V\nby Rory Lucyshyn-Wright as part of Topos Institute Colloquium\n\n\nAbstract\nEnriched categories have hom- objects in a monoidal category V\, but their theory is usually formulated under the assumption that V is biclosed and so is enriched in itself. Cate gories equipped with an action of V (or V-actegories) provide a related se tting with the advantage that an arbitrary monoidal category V can always be regarded as a V-actegory. Richard Wood delineated a setting subsuming b oth V-enriched categories and V-actegories by considering V-graded categor ies\, which are categories enriched in a monoidal category of presheaves o n V but admit also a direct and elementary definition in terms of a notion of morphism with an additional parameter in V. Graded categories have als o been called procategories (by Kelly-Labella-Schmitt-Street) and locally V-graded categories (by Levy).\n\nIn this talk\, we introduce V-graded cat egories and their basic theory\, with an emphasis on how V-graded categori es provide a foundational setting generalizing V-enrichment for arbitrary monoidal categories V. We also discuss the speaker's recent work that prov ides a way of defining V-graded functor categories and bifunctors for arbi trary monoidal categories V\, by involving a notion of bigraded category\, of which V is always an example. This contrasts with the familiar setting s of enriched category theory where the use of functor categories and bifu nctors demands a symmetry on V\, or more generally a normal duoidal struct ure on V as studied by Garner and López Franco. We discuss how V-graded m odules or profunctors for an arbitrary monoidal category V are examples of graded bifunctors.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /179/ END:VEVENT BEGIN:VEVENT SUMMARY:Dario Stein DTSTART:20250522T170000Z DTEND:20250522T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/180 DESCRIPTION:Title: Random Variables\, Independence Structures and D agger Categories of Relations\nby Dario Stein as part of Topos Institu te Colloquium\n\n\nAbstract\nRandom variables are a central notion of prob ability theory\, but they are defined with reference to an elusive sample space existing the background. Alex Simpson pioneered the use sheaves over sample spaces to make this dependence explicit. The resulting sheaf topos comes with a notion of random variable and thus probability built-in. It turns out that sample spaces can be generalized to a wide variety of proba bility-like phenomena\, such as nondeterminism or fresh name generation. T he probability sheaf construction hinges on a notion of independence struc ture where certain squares of sample spaces are distinguished as independe nt.\n\nI will give a tour of these abstract samples and then discuss the r ich interplay between sample spaces and couplings. These categories determ ine each other in a precise sense\, where couplings behave like relations over sample spaces and compose via independent pullback.\n\nJoint work wit h Chris Heunen\, Matthew Di Meglio and Paolo Perrone\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /180/ END:VEVENT BEGIN:VEVENT SUMMARY:Fosco Loregian DTSTART:20250925T170000Z DTEND:20250925T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/181 DESCRIPTION:Title: A double category of transducers\nby Fosco L oregian as part of Topos Institute Colloquium\n\n\nAbstract\nWe define a b icategory 𝟚TDX whose 1-cells provide a categorification of transducers\ , computational devices extending finite-state automata with output capabi lities. This bicategory is a mathematically interesting object: among many equivalent characterizations\, given an input category 𝒜 and an output category ℬ\, its 1-cells (𝒬\, t) : 𝒜 ⇝ ℬ can be seen as “fa milies of profunctors over 𝒬\, indexed over 𝒜\, and enriched over (a universal monoidal category obtained from) ℬ”\; more precisely\, 2-tr ansducers are functors of type\n\n  t : 𝒜 × 𝒬ᵒᵖ × 𝒬 × (ℬ* )ᵒᵖ ⟶ Set\n\nwhere ℬ* denotes the free monoidal category ove r ℬ. Extending t to 𝒜*\, in the obvious way\, for each “word” 𝑎̲ in 𝒜* we obtain an endoprofunctor over a category 𝒬 of “sta tes” and enriched in presheaves over the free monoidal category ℬ*.\n\ nWe discuss a number of other characterizations of 𝟚TDX(𝒜\, ℬ) in detail\; we establish a Kleisli-like universal property for 𝟚TDX(𝒜\, ℬ) and explore the connection of 𝟚TDX to other bicategories of compu tational models\, such as Walters’ “bicategory of circuits”. It is c onvenient to regard 𝟚TDX as the loose bicategory of a double category 𝔻TDX\; the bicategory (resp. double category) of profunctors is natural ly contained in the bicategory (resp. double category) 𝟚TDX (resp. 𝔻 TDX)\; we study the completeness and cocompleteness properties of 𝔻TDX\ , as well as monads\, adjunctions\, and other structures/properties that n aturally arise from the definition.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /181/ END:VEVENT BEGIN:VEVENT SUMMARY:Aleks Kissinger DTSTART:20250703T170000Z DTEND:20250703T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/182 DESCRIPTION:Title: ZX Calculus and Fault-tolerant quantum computing \nby Aleks Kissinger as part of Topos Institute Colloquium\n\n\nAbstra ct\nQuantum computers are highly susceptible to noise due to interactions with environment and tiny imperfections in the physical implementations of basic operations like gates and measurements. Fault tolerant quantum comp uting encodes quantum data with some redundancy\, which can be exploited t o detect and correct errors throughout a computation. This is a huge area with many hard problems and fascinating techniques. In this talk\, I will survey some of the ways we have been chipping away at those problems using compositional ideas\, and in particular the ZX calculus\, a graphical lan guage for representing and reasoning about quantum computations. I will as sume no prior knowledge of quantum computing\, only complex linear algebra and the tensor product.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /182/ END:VEVENT BEGIN:VEVENT SUMMARY:Kevin Carlson DTSTART:20251002T170000Z DTEND:20251002T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/183 DESCRIPTION:Title: Instances of models of double theories\nby K evin Carlson as part of Topos Institute Colloquium\n\n\nAbstract\nI'll int roduce the notion of instance of a model of a double theory. I'm motivated by the analogy that\, as a category $C$ is to its $C$-sets\, so a model o f an arbitrary double theory $\\mathbb{D}$ (that is\, a lax double functor $\\mathbb{D}\\to\\mathbb{S}\\mathbf{pan}$) is to its instances. The motiv ating case of the analogy arises precisely when we set $\\mathbb{D}$ to be the terminal double theory.\n\nThus the theory of instances can be seen a s a chapter of categorical database theory. Beyond the most fundamental ca se\, introduced by Spivak and Kent\, of a database schema as a small categ ory $C$ of "types" and "attributes"\, or "tables" and "foreign keys"\, and a database as a $C$-set\, the concept of instance encompasses such known extensions as to Baas\, Fairbanks\, Lynch\, and Patterson's attributed $C$ -sets\, as well as to Schultz\, Spivak\, Vasilakopoulou\, and Wisknesky's algebraic profunctors. From broader motivations\, such structures as multi functors from a multicategory to $\\mathbf{Set}$ and models of a Lawvere t heory are also instances of "instances." \n\nI'll describe the category of instances of models of simple double theories\, as well\, hopefully\, as introducing the story for models of the modal double theories recently int roduced into our CatColab tool as our main approach for handling categoric al structures including multi-ary operations. I'll aim to explain how quit e a lot of the standard theory of $C$-sets generalizes beyond the terminal double theory. For instance\, I'll give a comprehensive factorization sys tem on the category of models of a double theory\, together with a Grothen dieck construction giving an equivalence between the category of discrete opfibrations over a model $X$ and the category of $X$-instances.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /183/ END:VEVENT BEGIN:VEVENT SUMMARY:Mohamed Barakat DTSTART:20250717T170000Z DTEND:20250717T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/184 DESCRIPTION:Title: CAP — a categorical (re)organization of comput er algebra\nby Mohamed Barakat as part of Topos Institute Colloquium\n \n\nAbstract\nIn this talk I will introduce CAP (Categories\, Algorithms a nd Programming)\, a multi-package open-development software project for al gorihmic category theory. CAP is currently loosely organized by the 3-cate gory of “doctrines". By a doctrine we mean a 2-category of structured ca tegories\, structure-preserving 2-functors\, and natural transformations b etween them. Compositions of such 2-functors applied to a specific categor y give rise to what we call "categorical towers"\, a highly economic and m odular way to create various computational contexts in computer algebra. S uch modular code cannot be optimized by hand for comptutational performanc e as it would require breaking the modularity: Each layer in the tower tre ats the layer below merely as a blackbox. This forced us to develop Compil erForCAP\, a category-theory-aware compiler that is able to get rid of the entire categorical abstraction and produce efficient low-level code which is almost impossible to write by hand\, let alone error-free.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /184/ END:VEVENT BEGIN:VEVENT SUMMARY:Nathaniel Virgo DTSTART:20250904T170000Z DTEND:20250904T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/185 DESCRIPTION:Title: Towards a mathematical theory of intentional sys tems\nby Nathaniel Virgo as part of Topos Institute Colloquium\n\n\nAb stract\nWhat does it mean for a system to have "beliefs" and take "actions " in service of "goals"? Philosophy and cognitive science have offered a v ariety of answers to this question\, including Dennett's intentional stanc e\, the Bayesian brain hypothesis\, and various forms of 'enactivism'\, am ong many others. I will talk about several closely related approaches to t elling these stories\, or simplified versions of them\, in a mathematical way. Surprisingly (to me at least)\, doing so makes them seem much more co mpatible and closely related than they might at first appear.\n\nDennett's core idea is that the key question to ask about a system is not whether i t is an agent or not\, but whether its behaviour can be well described by treating it as one. This entails ascribing beliefs and goals to it\, and p redicting its behaviour by assuming it will take actions that would bring the goals about if the beliefs were true. For some systems this yields exc ellent predictions of their behaviour\, and the behavioural patterns that enable this can be said to be a real property of the system.\n\nMathematic ally this suggests a paradigm where instead of starting with a problem and asking what systems can solve it\, we start with a system and ask what pr oblems it can solve. In doing this we are forced to grapple with questions such as what exactly constitutes a belief\; how should beliefs change ove r time in response to new information\; what happens if two different beli ef attributions give rise to the same behaviour\; and where should we draw the boundary of a system\, if we want to treat it as an agent? Ideas from categorical systems theory and category-theoretic probability are used th roughout the work.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /185/ END:VEVENT BEGIN:VEVENT SUMMARY:Eric Finster DTSTART:20250911T170000Z DTEND:20250911T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/186 DESCRIPTION:Title: Dependetopes and Higher Generalized Algebraic Th eories\nby Eric Finster as part of Topos Institute Colloquium\n\n\nAbs tract\nMany of the classical tools of categorical algebra can be generaliz ed\nto the world of higher algebra\, that is\, the study of algebraic\nstr uctures on homotopy types. Indeed we can talk about ∞-Lawvere\ntheories\ , ∞-finite limit theories\, classifying ∞-topoi\, ∞-operads and\nso on. That we can define and reason about such higher algebraic\ntheories i s a result of the well-developed theory of (∞\,1)-categories\nof Joyal a nd Lurie\, and ultimately relies on the tractability of\nworking combinato rially with simplices.\n\nType theorists and computer scientists often wor k with presentations\nof algebraic theories using dependent types\, so-cal led "Generalized\nAlgebraic Theories"\, exactly because they have convenie nt syntactic\ndescriptions which lend themselves to computer implementatio n. We can\ngeneralize the categorical semantics of these theories to the higher\nsetting using the tools above\, but doing so renders the connectio n to\nconcrete syntax somewhat tenuous.\n\nIn this talk I'll introduce a m ethod for recovering a more syntactic\ndescription of the notion of higher generalized algebraic theory by\nintroducing the category of dependetopes . The name derives from the\nfact that the dependetopes can be understood as a dependently typed\nextension of Baez-Dolan's notion of opetope which captures the higher\ngeometry of type-dependency. In addition to their def inition\, I will\nexplain how the dependetopes come with a concrete syntax arising from\ntype theory\, which can be used to define and manipulate th em.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /186/ END:VEVENT BEGIN:VEVENT SUMMARY:Barbara König DTSTART:20251009T170000Z DTEND:20251009T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/187 DESCRIPTION:Title: Behavioural Metrics via Functor Lifting – A Co algebraic Approach\nby Barbara König as part of Topos Institute Collo quium\n\n\nAbstract\nBehavioural distances of transition systems modelled via coalgebras for\nendofunctors generalize traditional notions of behavio ural equivalence\nto a quantitative setting\, in which states are equipped with a measure\nof how (dis)similar they are. Endowing transition systems with such\ndistances essentially relies on the ability to lift functors d escribing\nthe one-step behavior of the transition systems to the category of\npseudometric spaces. We consider the category theoretic generalizatio n\nof the Kantorovich/Wasserstein lifting from transportation theory to th e\ncase of lifting functors to pseudo-metric spaces. We also consider\ncom positionality results which are essential ingredients for adapting\nup-to- techniques to the case of behavioural distances. Up-to techniques\nare a w ell-known coinductive technique for efficiently showing lower\nbounds for behavioural metrics. We illustrate the method with a case\nstudy on probab ilistic automata.\n\nThis is joint work with Paolo Baldan\, Filippo Bonchi \, Henning Kerstan\,\nDaniela Petrisan\, Keri D'Angelo\, Sebastian Gurke\, Johanna Maria Kirss\,\nMatina Najafi\, Wojciech Rozowski and Paul Wild.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /187/ END:VEVENT BEGIN:VEVENT SUMMARY:Maru Sarazola DTSTART:20250918T170000Z DTEND:20250918T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/188 DESCRIPTION:Title: Double categorical equivalences\nby Maru Sar azola as part of Topos Institute Colloquium\n\n\nAbstract\nDouble categori es are a flexible 2-dimensional setting that allows us to encode two types of morphisms between objects\, as well as a notion of higher cells. Surpr isingly\, unlike most categorical structures\, there is no canonical notio n of “equivalence of double categories”\, as it seems that every possi ble definition requires us to make a choice. In this talk we will illustra te the issue that arises when defining double-categorical equivalences. Th en\, we will show how we can use homotopy theory to give a decisive answer as to who the “canonical double categorical equivalences” should be: the gregarious equivalences introduced by Campbell. In the process\, we wi ll show how to construct a plethora of model structures on double categori es whose homotopy theories encode different 2-dimensional structures.\n\nB ased on work in preparation joint with Lyne Moser and Paula Verdugo.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /188/ END:VEVENT BEGIN:VEVENT SUMMARY:Rune Haugseng DTSTART:20251106T170000Z DTEND:20251106T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/190 DESCRIPTION:Title: Commutative rings\, bispans\, and their equivari ant analogues\nby Rune Haugseng as part of Topos Institute Colloquium\ n\n\nAbstract\nCommutative monoids in a category with finite products can be\nidentified with product-preserving functors from spans of finite\nsets . Similarly\, we can describe commutative semirings as\nproduct-preserving functors from "bispans" (or "polynomial diagrams")\nin finite sets. I wil l outline a proof of this comparison that also\nworks in the ∞-categoric al setting\, and then discuss its G-equivariant\nanalogue for a finite gro up G. In sets\, this amounts to an\nidentification of Tambara functors as G-commutative algebras in Mackey\nfunctors (first proved by R. Hoyer)\, wh ile in ∞-groupoids it gives a\nconcrete description of "genuine" commuta tive rings in connective\nG-spectra as homotopy-coherent Tambara functors. This is joint work\nwith B. Cnossen\, T. Lenz\, and S. Linskens.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /190/ END:VEVENT BEGIN:VEVENT SUMMARY:Alex Kavvos DTSTART:20251113T170000Z DTEND:20251113T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/191 DESCRIPTION:Title: Two-dimensional Kripke Semantics\nby Alex Ka vvos as part of Topos Institute Colloquium\n\n\nAbstract\nThe study of mod al logic has witnessed tremendous development following the introduction o f Kripke semantics. However\, recent developments in programming languages and type theory have led to a second way of studying modalities\, namely through their categorical semantics. We show how the two correspond.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /191/ END:VEVENT BEGIN:VEVENT SUMMARY:John Baez DTSTART:20251211T170000Z DTEND:20251211T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/192 DESCRIPTION:Title: Cospans of finite sets\nby John Baez as part of Topos Institute Colloquium\n\n\nAbstract\nCospans of finite sets are t he morphisms in a bicategory\, not really a category\, because composition of cospans is associative only up to natural isomorphism. How can we char acterize this bicategory abstractly? There's a category of finite sets and *isomorphism classes* of cospans. Steve Lack gave a beautiful characteriz ation of this\, which I will explain\, and Fong and Spivak used this categ ory to clarify the concept of "hypergraph category". But what about the *b icategory* of finite sets\, cospans\, and maps between cospans? I will sta te a guess that I haven't proved.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /192/ END:VEVENT BEGIN:VEVENT SUMMARY:Cole Comfort DTSTART:20251016T170000Z DTEND:20251016T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/193 DESCRIPTION:Title: Syntax and semantics for mechanical processes\nby Cole Comfort as part of Topos Institute Colloquium\n\n\nAbstract\nIn this talk I will review how certain classes of quantum and classical mech anical processes can be represented in terms of affine Lagrangian relation s between finite-dimensional vector spaces (the semantics)\; which comes e quipped with a ZX-calculus-style graphical language (the syntax). \n\nI w ill discuss how both the syntax and semantics can be extended to more expr essive settings: on the one hand with Gaussian probabilistic behaviour\, a nd on the other hand with discrete-time-evolution.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /193/ END:VEVENT BEGIN:VEVENT SUMMARY:Xiao-Gang Wen DTSTART:20251023T170000Z DTEND:20251023T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/194 DESCRIPTION:Title: Symmetry beyond group and its description by bra ided fusion category\nby Xiao-Gang Wen as part of Topos Institute Coll oquium\n\n\nAbstract\nThe conventional understanding\, which describes sym metry using group theory\, is insufficient\, because symmetry can be anoma lous\, higher-group\, and/or non-invertible (those symmetries are called a lgebraic higher symmetries in the paper). We find that all such finite sym metries - when considered up to holo-equivalence - are precisely classifie d by topological orders in one higher dimension (that can host a gappable boundary). This fundamentally shifts our perspective: symmetry is not inhe rently about groups\, but is more naturally described by the mathematics o f braided fusion higher categories.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /194/ END:VEVENT BEGIN:VEVENT SUMMARY:Slim Lim DTSTART:20251204T170000Z DTEND:20251204T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/195 DESCRIPTION:Title: Concrete syntax matters\, actually\nby Slim Lim as part of Topos Institute Colloquium\n\n\nAbstract\nToo many programm ing languages researchers dismiss concrete syntax as an afterthought: arbi trary\, superficial\, or distracting from matters of “actual” (semanti c) importance. This received view ignores a critical factor: the human at the computer. Concrete syntax defines the principal interface through whic h programmers interact with the vast majority of programming languages. Mo reover\, this interface is hardly decoupled from semantics\; even trivial- seeming differences in keywords\, sigils\, and indentation can affect how programmers utilize and reason about language behavior. Using examples fro m asynchronous control flow\, gradual subtyping\, first-class functions\, and more\, I will make a case for the importance of concrete syntax\, why language designers often overlook it\, and what this implies for those of us who care about the usability of abstractions. Finally\, I will describe some preliminary work evaluating the role of lexical ambiguity in program mer comprehension of type system features.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /195/ END:VEVENT BEGIN:VEVENT SUMMARY:Terry Winograd DTSTART:20251030T170000Z DTEND:20251030T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/197 DESCRIPTION:Title: What's up with AI?\nby Terry Winograd as par t of Topos Institute Colloquium\n\n\nAbstract\nThe current boom in AI has been accompanied by tremendous hype\, both\nnegative and positive. My goa l is to go beneath this surface and\nprovide a better understanding of wha t AI systems are actually doing\,\nand what concerns we should have about where they are going.\nI am neither a doomer nor a booster. The very real problems created by AI today\nand in the foreseeable future need to be app roached by considering the\nways we (as a society) choose to apply it and the ways in which\nit can fit into our world. The bottom line is that we need to approach\nall of the issues with the recognition that large langua ge models and\nsimilar systems have no real understanding or intention\, e ven though\nthey often promote the illusion that they do. They can still be useful\nin many contexts\, as long as we recognize the need for humans to\nalways provide the foundation of care.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /197/ END:VEVENT BEGIN:VEVENT SUMMARY:Benjamin Pierce DTSTART:20260226T170000Z DTEND:20260226T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/199 DESCRIPTION:Title: Properties for the People\nby Benjamin Pierc e as part of Topos Institute Colloquium\n\n\nAbstract\nProperty-Based Test ing (PBT) is a lightweight formal method offering an attractive blend of t he abstract (formal specification) and the concrete (executability). Its p opularity in the functional programming community has grown steadily over the past 25 years\, and it is poised to play a key role in the larger soft ware industry\, mediating between human programmers and their AI collabora tors. I'll describe a collection of recent advances and remaining challeng es in this space.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /199/ END:VEVENT BEGIN:VEVENT SUMMARY:Marcelo Aguiar DTSTART:20260305T170000Z DTEND:20260305T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/200 DESCRIPTION:Title: The Eckmann-Hilton argument in duoidal categorie s\nby Marcelo Aguiar as part of Topos Institute Colloquium\n\n\nAbstra ct\nWe will go over the basics of duoidal categories\, illustrating with a number of examples. As monoidal categories provide a context for monoids\ , duoidal categories provide one for duoids and bimonoids. Our main goal i s to discuss a number of versions of the classical Eckmann-Hilton argument which may be formulated in this setting. As an application we will obtain the commutativity of the cup product on the cohomology of a bimonoid with coefficients in a duoid\, an extension of a familiar result for group and bialgebra cohomology with trivial coefficients.\n\nThe talk borrows on ea rlier work in collaboration with Swapneel Mahajan on the foundations of du oidal categories (2010). The main results are from ongoing work with Javie r Coppola. We also rely on work of Richard Garner and Ignacio López-Franc o (2016).\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /200/ END:VEVENT BEGIN:VEVENT SUMMARY:Jean-Simon Lemay DTSTART:20250612T170000Z DTEND:20250612T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/201 DESCRIPTION:Title: Cartesian Fermat Categories\, a new class of Car tesian Differential Categories\nby Jean-Simon Lemay as part of Topos I nstitute Colloquium\n\n\nAbstract\nCartesian differential categories (intr oduced by Blute\, Cockett\, and Seely) provide a categorical framework fo r differential calculus\, and also provide the categorical foundations for the differential lambda calculus\, differentiable programming\, and certa in automatic differentiation techniques used for machine learning. Another approach to the categorical foundations of differentiation are Fermat the ories (introduced by Dubuc and Kock)\, which are Lawvere theories that hav e Hadamard’s Lemma as an axiom. It is already known that every Fermat th eory is a Cartesian differential category. However\, the definition of a F ermat theory is heavily dependent on 1) being a Lawvere theory and 2) bein g able to multiply maps\, which are two things that are not assumed for Ca rtesian differential categories. In this talk\, we will introduce Cartesia n Fermat categories\, the proper Fermat theory analogue of a Cartesian dif ferential category\, with the main result being that Cartesian Fermat cate gory is a Cartesian differential category. This talk will also include a f riendly introduction to Cartesian differential categories\, and thus will be accessible to anyone\, including newcomers\, interested in differential categories.\n\nThis talk is based on joint work with Carlos Pascual Miral les.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /201/ END:VEVENT BEGIN:VEVENT SUMMARY:Dan Ghica DTSTART:20260205T170000Z DTEND:20260205T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/202 DESCRIPTION:Title: Designing and developing an industrial-strength programming language: Stories from the trenches\nby Dan Ghica as part of Topos Institute Colloquium\n\n\nAbstract\nFor the last five years I hav e been working as one of the architects of a new programming language call ed Cangjie (CJ). CJ is part of a new open-source ecosystem for Huawei devi ces which has the HarmonyOS operating system at its core. I will discuss s ome of the innovations adopted by CJ such as effect handlers (released) an d modal types (work in progress) and comment on my personal experience as a 'theory person' now involved in developing a language for a wide audienc e\, which includes some of the top Chinese tech companies.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /202/ END:VEVENT BEGIN:VEVENT SUMMARY:Patrick Shafto DTSTART:20260219T170000Z DTEND:20260219T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/203 DESCRIPTION:Title: Autoformalization and the future of math and sci ence\nby Patrick Shafto as part of Topos Institute Colloquium\n\n\nAbs tract\nAdvances in autoformalization suggest the possibility of automatic translation between natural language mathematics and formal verification p rogramming languages. We'll chart this recent progress in mathematics. We will consider implications for mathematics\, and science more broadly.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /203/ END:VEVENT BEGIN:VEVENT SUMMARY:Paul Levy DTSTART:20260312T170000Z DTEND:20260312T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/204 DESCRIPTION:Title: What is a monoid?\nby Paul Levy as part of T opos Institute Colloquium\n\n\nAbstract\nIn many situations one encounters an entity that resembles a monoid. It consists of a carrier and two opera tions that resemble a unit and a multiplication\, subject to three equatio ns that resemble associativity and left and right unital laws. The questio n then arises whether this entity is\, in fact\, a monoid in a suitable se nse.\n\nCategory theorists have answered this question by providing a noti on of monoid in a monoidal category\, or more generally in a multicategory . While these encompass many examples\, there remain cases which do not f it into these frameworks\, such as the notion of relative monad\, and the modelling of call-by-push-value sequencing. In each of these examples\, t he leftmost and/or the rightmost factor of a multiplication or associativi ty law seems to be distinguished. \n\nTo include such examples\, we gener alize the multicategorical framework in two stages. \n\nFirstly\, we move to the framework of a left-skew multicategory (due to Bourke and Lack)\, which generalizes both multicategory and left-skew monoidal category. The notion of monoid in this framework encompasses examples where only the le ftmost factor is distinguished\, such as the notion of relative monad.\n\n Secondly\, we consider monoids in the novel framework of a bi-skew multica tegory. This encompasses examples where both the leftmost and the rightmo st factor are distinguished\, such as the notion of a category on a span\, and the modelling of call-by-push-value sequencing.\n\nIn the bi-skew fra mework (which is the most general)\, we give a coherence result saying tha t a monoid corresponds to an unbiased monoid\, i.e. a map from the termina l bi-skew multicategory.\n\nThis is joint work with Morgan Rogers\, and wa s presented at the POPL 2026 conference. See the paper at https://dl.acm. org/doi/10.1145/3776727\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /204/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrej Bauer DTSTART:20260402T170000Z DTEND:20260402T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/205 DESCRIPTION:Title: Classically laughable theorems\nby Andrej Ba uer as part of Topos Institute Colloquium\n\n\nAbstract\nIn intuitionistic mathematics one encounters theorems that may seem strange\, even laughabl e\, to a classically trained mathematician. Yet\, interpreted internally i n toposes and other non-classical models\, they carry genuine mathematical content. For example\, Lawvere’s fixed-point theorem says that if there is a surjection $A \\to B^A$\, then every endomap on $B$ has a fixed poin t\; classically the precondition forces $B$ to be a singleton. Likewise\, a statement that is false in classical set theory can be meaningful intern ally: in the effective topos there exists a set that is neither finite nor infinite. In the talk we will try not to laugh\, and instead explain how such claims acquire substance once the viewpoint expands beyond classical mathematics.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /205/ END:VEVENT BEGIN:VEVENT SUMMARY:Robin Piedeleu DTSTART:20260416T170000Z DTEND:20260416T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/206 DESCRIPTION:Title: The Algebra of Probabilistic Boolean Circuits\nby Robin Piedeleu as part of Topos Institute Colloquium\n\n\nAbstract\n Boolean algebra gives us a complete and elegant way to reason algebraicall y about propositional logic and simple circuits. But what happens when we introduce randomness?\nIn this talk\, we will see how to extend Boolean ci rcuits with probabilistic primitives\, obtaining probabilistic Boolean cir cuits that combine logical operations with random choice and conditioning. We will formalise these as string diagrams and give them two functorial s emantics: one in terms of (sub)stochastic maps\, and another in which subd istributions are identified up to normalisation. We will then present a so und and complete equational theory for each possible interpretation. Time allowing\, we will also cover the relationship with probabilistic programm ing and extensions of the diagrammatic calculus to mixtures of Gaussians. \n\nNote these developments are of interest for the development of probabi lity theory in Markov categories: our results give a presentation by gener ators and equations of the symmetric monoidal category of stochastic maps (with the cartesian product as monoidal product) restricted to objects tha t are powers of the two-element set.\n\nBased on joint work with Mateo Tor res-Ruiz\, Alexandra Silva\, and Fabio Zanasi: https://doi.org/10.1007/978 -3-031-91121-7_9\, arXiv: https://arxiv.org/abs/2408.14701\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /206/ END:VEVENT BEGIN:VEVENT SUMMARY:Chris Heunen DTSTART:20260423T170000Z DTEND:20260423T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/207 DESCRIPTION:Title: Control\, Complete\, Compute: Rig Categories in Quantum Computing\nby Chris Heunen as part of Topos Institute Colloqui um\n\nInteractive livestream: https://topos-institute.zoom.us/j/8439252373 6?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nView-only li vestream: https://www.youtube.com/live/jiCiuCQQ2Jo\n\nAbstract\nWe present a categorical axiomatisation of quantum computation based on free constru ctions. Starting from a PROP of base circuits\, we introduce a theory of c omputational control given by eight natural equations\, and show that adjo ining control syntactically corresponds semantically to completing the PRO P to its free rig category. Next\, we show that two further generators and three further equations suffice to fully characterise quantum computing. The resulting free model replaces the usual linear-algebraic semantics wit h a purely symbolic\, combinatorial one. We argue that this gives a concep tually simpler foundation for quantum computing that isolates quantum adva ntage in a precise categorical sense. (Based on joint work https://doi.org /10.1073/pnas.2510881123 and https://arxiv.org/abs/2510.05032 with Robin K aarsgaard\, Louis Lemonnier\, Neil Julien Ross\, Amr Sabry\, and Jacques C arette.)\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /207/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 URL:https://www.youtube.com/live/jiCiuCQQ2Jo END:VEVENT BEGIN:VEVENT SUMMARY:Chad Nester DTSTART:20260212T170000Z DTEND:20260212T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/208 DESCRIPTION:Title: Combinatory Completeness in Structured Multicate gories\nby Chad Nester as part of Topos Institute Colloquium\n\n\nAbst ract\nCombinatory logic was introduced more than a century ago in pursuit of logical syntax without bound variables. Its power and simplicity have m ade it a subject of enduring interest\, and it has played a foundational r ole in logic and computer science. A combinatory algebra is an algebraic m odel of combinatory logic. Concretely\, such an algebra consists of a set equipped with a binary operation satisfying a condition called combinatory completeness. This condition is rather complex\, but is equivalent to the existence of elements of the carrier set satisfying certain simple equati ons.\n\nThis talk concerns a more general notion of combinatory completene ss relative to a certain well-behaved collections of functions between fin ite sets\, called faithful Cartesian clubs. The classical notion of combin atory completeness corresponds to the club consisting of all such function s. Moreover\, the equivalence of combinatory completeness with the existen ce of elements satisfying simple equations holds in some form for a number instances of the more general notion. These results hold in settings beyo nd the usual category of sets and functions\, and their technical developm ent takes place in a multicategory equipped with an action of the faithful Cartesian club in question. These structured multicategories are a natura l setting in which to study (variations of) combinatory algebras.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /208/ END:VEVENT BEGIN:VEVENT SUMMARY:Danel Ahman DTSTART:20260409T170000Z DTEND:20260409T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/209 DESCRIPTION:Title: Containers and Comodule Representations of Secon d-Order Functionals\nby Danel Ahman as part of Topos Institute Colloqu ium\n\n\nAbstract\nIn information-theoretic terms\, a map is continuous wh en a finite\namount of information about its input suffices for computing a finite\namount of information about its output. Already Brouwer observed that\nthis allows one to represent a continuous functional from sequences to\nnumbers with a certain well-founded question-answer tree.\n\nIn type theory\, a second-order functional is a (dependently typed) map\n\nF : ( ∏(a : A) . P a) → (∏(b : B) . Q b).\n\nIts continuity is once again witnessed by B-many well-founded trees\nwhose nodes are “questions” a : A\, the branches are indexed by\n“answers” p : P a\, and the leaves are “results” Q b. In this work\, we\nobserve that such tree represent ations can be expressed in purely\ncategory-theoretic terms\, using the no tion of right T-comodules for\nthe monad T of well-founded trees on the ca tegory of containers. A\ntree representation for F is then just a Kleisli map for the monad T.\n\nDoing so exposes a rich underlying structure\, and immediately suggests\ngeneralisations: any right T-comodule for any monad T on containers\ngives rise to a corresponding representation theorem for second-order\nfunctionals. We give several examples of these\, ranging fr om finitely\nsupported functionals\, to functionals that can query their i nput just\nonce (or sometimes not at all)\, to functionals that can additi onally\ninteract with their environment\, to partial functionals\, to obse rving\nthat any functional can be trivially represented by itself.\n\nThis is joint work with Andrej Bauer from the University of Ljubljana.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /209/ END:VEVENT BEGIN:VEVENT SUMMARY:Christoph Benzmueller DTSTART:20260507T170000Z DTEND:20260507T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/210 DESCRIPTION:Title: Many Logics\, One Methodology — On the Virtues of LogiKEy in Computational Metaphysics and Ontology\nby Christoph Be nzmueller as part of Topos Institute Colloquium\n\nInteractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhTdGh vZ3pUdz09\nPassword hint: 65537\n\nAbstract\nThis talk advances the case f or logical pluralism at the object logic level within a unifying meta-logi cal framework. While modern proof assistant systems often enforce a single foundational logic — a tendency we may call logical imperialism — suc h rigidity impedes the kind of interdisciplinary reuse that robust knowled ge representation demands. Our proposed alternative is LogiKEy: a logic-pl uralistic methodology for knowledge representation and reasoning in which object logics are treated as first-class\, analyzable entities\, with appl icability across many fields\, including but not limited to computational metaphysics and ontology.\n\nThe virtues of LogiKEy are illustrated throug h a concrete case study: Gödel's modal ontological argument and Dana Scot t's variant of it. Supported by experimental studies in a proof assistant system for classical higher-order logic\, we demonstrate how the framework promotes interdisciplinary research and education on logical foundations and philosophical arguments\, while also yielding new formal insights into these landmark arguments\, and we address some questions accumulated over the past decade.\n\nThis is partly joint work with Dana Scott.\n\nReferen ce: Notes on Gödel's and Scott's Variants of the Ontological Argument\, C hristoph Benzmüller\, Dana S. Scott · Monatshefte für Mathematik 208\, 569–611. Doi: https://doi.org/10.1007/s00605-025-02078-x\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /210/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Jeremy Gibbons DTSTART:20260430T170000Z DTEND:20260430T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/211 DESCRIPTION:Title: Total Functional Programming\, Reloaded\nby Jeremy Gibbons as part of Topos Institute Colloquium\n\nInteractive livest ream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QU hTdGhvZ3pUdz09\nPassword hint: 65537\nView-only livestream: https://www.yo utube.com/live/0WBLvstjZ4I\n\nAbstract\nMathematically structured function al programming presents its practitioners with a dilemma. On the one hand\ , it is very appealing to model programs taking typed inputs to typed outp uts as total functions between sets. Then standard constructions satisfy s imple but powerful universal properties\, giving rise to a useful body of laws for program calculation\; everything fits neatly together. On the oth er hand\, this appealing model is too simplistic: it cannot address the po ssibility of non-productive non-termination\, so in particular rules out a rbitrary recursive definitions. Accommodating such extra expressivity enta ils switching the setting from total functions between sets to continuous functions between CPOs\; many of the laws are weakened\, or complicated th rough strictness side-conditions. Ideally we would work in an intermediate setting\, encompassing well-founded generative recursion (such as divide- and-conquer algorithms and the hylomorphism pattern) while still excluding ill-founded general recursion. What is the right path towards this ideal world? I have been exploring this question while writing my forthcoming bo ok Patterns in Functional Programming. I don't have any answers\, but I do have some options\, suggestions\, and challenges.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /211/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 URL:https://www.youtube.com/live/0WBLvstjZ4I END:VEVENT BEGIN:VEVENT SUMMARY:Stefan Milius DTSTART:20260521T170000Z DTEND:20260521T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/212 DESCRIPTION:by Stefan Milius as part of Topos Institute Colloquium\n\nInte ractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdV S09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /212/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:James Hefford DTSTART:20260319T170000Z DTEND:20260319T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/213 DESCRIPTION:Title: BV-Categories and Higher-Order Quantum Theory\nby James Hefford as part of Topos Institute Colloquium\n\n\nAbstract\nB V-logic is an extension of multiplicative linear logic which adds an addit ional non-commutative connective representing sequential composition. BV-c ategories have been suggested as potential models of this logic and I will show how they arise as pseudomonoids in a bicategory of *-autonomous cate gories while discussing their relation to self-dual duoidal categories. Th is allows us to lift the Chu construction to this setting and use it to co freely construct many examples of BV-categories. One notable application i s to models of higher-order quantum theory\, quantum supermaps and indefin ite causal orders and I will discuss how these structures can be modelled by passing to the strong Hyland envelope of a category.\n\nThis is joint w ork with Matt Wilson\, based on https://dl.acm.org/doi/abs/10.1145/3661814 .3662123 and https://arxiv.org/abs/2502.19022.\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /213/ END:VEVENT BEGIN:VEVENT SUMMARY:Simon Willerton DTSTART:20260514T170000Z DTEND:20260514T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/214 DESCRIPTION:by Simon Willerton as part of Topos Institute Colloquium\n\nIn teractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bj dVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /214/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Helle Hvid Hansen DTSTART:20260604T170000Z DTEND:20260604T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/215 DESCRIPTION:by Helle Hvid Hansen as part of Topos Institute Colloquium\n\n Interactive livestream: https://topos-institute.zoom.us/j/84392523736?pwd= bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /215/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Joe Moeller DTSTART:20260611T170000Z DTEND:20260611T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/216 DESCRIPTION:by Joe Moeller as part of Topos Institute Colloquium\n\nIntera ctive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS0 9wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /216/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Inna Zakharevich DTSTART:20260129T170000Z DTEND:20260129T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/217 DESCRIPTION:Title: The category of schemes is abelian (and other ob viously-false true things)\nby Inna Zakharevich as part of Topos Insti tute Colloquium\n\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /217/ END:VEVENT BEGIN:VEVENT SUMMARY:Richard Blute DTSTART:20260618T170000Z DTEND:20260618T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/218 DESCRIPTION:by Richard Blute as part of Topos Institute Colloquium\n\nInte ractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdV S09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /218/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Astra Kolomatskaia DTSTART:20260625T170000Z DTEND:20260625T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/219 DESCRIPTION:by Astra Kolomatskaia as part of Topos Institute Colloquium\n\ nInteractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd =bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /219/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Matt Prewitt DTSTART:20260702T170000Z DTEND:20260702T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/220 DESCRIPTION:by Matt Prewitt as part of Topos Institute Colloquium\n\nInter active livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS 09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /220/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Mike Stay DTSTART:20260709T170000Z DTEND:20260709T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/221 DESCRIPTION:by Mike Stay as part of Topos Institute Colloquium\n\nInteract ive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09w ZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /221/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Marie Kerjean DTSTART:20260910T170000Z DTEND:20260910T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/222 DESCRIPTION:by Marie Kerjean as part of Topos Institute Colloquium\n\nInte ractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdV S09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /222/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Thierry Coquand DTSTART:20261001T170000Z DTEND:20261001T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/224 DESCRIPTION:by Thierry Coquand as part of Topos Institute Colloquium\n\nIn teractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bj dVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /224/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Jiří Rosický DTSTART:20260917T170000Z DTEND:20260917T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/225 DESCRIPTION:by Jiří Rosický as part of Topos Institute Colloquium\n\nIn teractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bj dVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /225/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Kris Brown DTSTART:20260903T170000Z DTEND:20260903T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/226 DESCRIPTION:by Kris Brown as part of Topos Institute Colloquium\n\nInterac tive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09 wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /226/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Timothy Campion DTSTART:20260716T170000Z DTEND:20260716T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/227 DESCRIPTION:by Timothy Campion as part of Topos Institute Colloquium\n\nIn teractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bj dVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /227/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:David Ayala DTSTART:20261105T170000Z DTEND:20261105T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/228 DESCRIPTION:by David Ayala as part of Topos Institute Colloquium\n\nIntera ctive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS0 9wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /228/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Andrew Pitts DTSTART:20261022T170000Z DTEND:20261022T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/229 DESCRIPTION:by Andrew Pitts as part of Topos Institute Colloquium\n\nInter active livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS 09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /229/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Dominik Trnka DTSTART:20261008T170000Z DTEND:20261008T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/230 DESCRIPTION:by Dominik Trnka as part of Topos Institute Colloquium\n\nInte ractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdV S09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /230/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT BEGIN:VEVENT SUMMARY:Alexandra Silva DTSTART:20261015T170000Z DTEND:20261015T180000Z DTSTAMP:20260416T215515Z UID:ToposInstituteColloquium/231 DESCRIPTION:by Alexandra Silva as part of Topos Institute Colloquium\n\nIn teractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bj dVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nAbstract: TBA\n LOCATION:https://stable.researchseminars.org/talk/ToposInstituteColloquium /231/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT END:VCALENDAR