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:20260423T094652Z UID:ToposInstituteColloquium/1 DESCRIPTION:Title: Poly: a category of remarkable abundance\nby David Sp ivak as part of Topos Institute Colloquium\n\nAbstract: TBA\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/1/ END:VEVENT BEGIN:VEVENT SUMMARY:Richard Garner DTSTART:20210211T210000Z DTEND:20210211T220000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/2 DESCRIPTION:Title: Comodels of an algebraic theory\nby Richard Garner as part of Topos Institute Colloquium\n\n\nAbstract\nIn 1991 Eugenio Moggi i ntroduced the monadic approach to computational effects\; this is the mech anism by which purely functional programming languages such as Haskell can express computations with side-effects such as output\, input\, or intera ction with an external store.\n\nAround 2000\, Plotkin and Power refined t he Moggi perspective by looking not at monads\, but the equational algebra ic theories which generate them: this amounts to specifying not just a kin d of side-effect\, but a set of primitive operations by which one can prog ram with these side-effects.\n\nAlgebraic theories have models\, not only in the category of sets\, but also in any category with finite products. I n particular\, one can look at comodels of a theory: a model in the opposi te of the category of sets. A crucial insight of Power and Shkaravska is t hat\, if T is a theory encoding interaction with an environment\, then a T -comodel is a state machine providing an instance of the environment with which T interacts.\n\nThe objective of this talk is to explain this histor y\, and to prove a new result: the category of comodels of any algebraic t heory T is a presheaf category [B\,Set]\, where B is a small category\, wh ich can be computed explicitly\, that encodes the static and dynamic prope rties of the side-effects encoded by T.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/2/ END:VEVENT BEGIN:VEVENT SUMMARY:Gunnar E. Carlsson DTSTART:20210218T170000Z DTEND:20210218T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/3 DESCRIPTION:Title: Relative topology\, motion planning\, and coverage proble ms\nby Gunnar E. Carlsson as part of Topos Institute Colloquium\n\n\nA bstract\nAlgebraic topology produces invariants that capture aspects of th e shape of a space\, or in the case of topological data analysis. Although these invariants are in general quite rich\, they are somewhat sparse in low dimensions. On the other hand\, it is possible to consider comma categ ories of spaces\, for example the category of spaces with reference to a f ixed base space and morphisms respecting the reference map. When one 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 sen sor nets and more general motion planning problems.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/3/ END:VEVENT BEGIN:VEVENT SUMMARY:Samson Abramsky DTSTART:20210311T170000Z DTEND:20210311T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/4 DESCRIPTION:Title: The logic of contextuality\nby Samson Abramsky as par t of Topos Institute Colloquium\n\n\nAbstract\n(joint work with Rui Soares Barbosa)\n\nContextuality is a key signature of quantum non-classicality\ , which has been shown to play a central role in enabling quantum advantag e for a wide range of information-processing and computational tasks.\nWe study the logic of contextuality from a structural point of view\, in the setting of partial Boolean algebras introduced by Kochen and Specker in th eir seminal work.\nThese contrast with traditional quantum logic a la Birk hoff--von Neumann\nin that operations such as conjunction and disjunction are partial\, only being defined in the domain where they are physically m eaningful.\n\nWe study how this setting relates to current work on context uality such as the sheaf-theoretic and graph-theoretic approaches.\nWe int roduce a general free construction extending the commeasurability relation on a partial Boolean algebra\, i.e. the domain of definition of the binar y logical operations.\nThis construction has a surprisingly broad range of uses.\nWe apply it in the study of a number of issues\, including:\n\n- e stablishing the connection between the abstract measurement scenarios stud ied in the contextuality literature and the setting of partial Boolean alg ebras\;\n\n- formulating various contextuality properties in this setting\ , including probabilistic contextuality as well as the strong\, state-inde pendent notion of contextuality given by Kochen--Specker paradoxes\, which are logically contradictory statements validated by partial Boolean algeb ras\, specifically those arising from quantum mechanics\;\n\n- investigati ng a Logical Exclusivity Principle\, and its relation to the Probabilistic Exclusivity Principle widely studied in recent work on contextuality\nas a step towards closing in on the set of quantum-realisable correlations\;\ n\n- developing some work towards a logical characterisation of the Hilber t space tensor product\, using logical exclusivity to capture some of its salient quantum features.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/4/ END:VEVENT BEGIN:VEVENT SUMMARY:John Baez DTSTART:20210325T180000Z DTEND:20210325T190000Z DTSTAMP:20260423T094652Z 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 o f a bigger transformation in which humanity realizes that the Earth is a f inite system and that no physical quantity can grow exponentially forever. This transformation may affect mathematics — and be affected by it — just as dramatically as the agricultural and industrial revolutions did. A fter a review of the problems\, we discuss how mathematicians can help mak e this transformation a bit easier\, and some ways in which mathematics ma y change.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/5/ END:VEVENT BEGIN:VEVENT SUMMARY:Dan Christensen DTSTART:20210401T170000Z DTEND:20210401T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/6 DESCRIPTION:Title: Reasoning in an ∞-topos with homotopy type theory\n by Dan Christensen as part of Topos Institute Colloquium\n\n\nAbstract\nTh is 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 for what these mean homotopically.  I will end by giving examples of results pro ved in homotopy type theory that tell us new results in any ∞-topos.   No prior knowledge of type theory or ∞-category theory will be assumed. \n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/6/ END:VEVENT BEGIN:VEVENT SUMMARY:Joachim Kock DTSTART:20210408T170000Z DTEND:20210408T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/7 DESCRIPTION:Title: Noncrossing hyperchords and free probability\nby Joac him Kock as part of Topos Institute Colloquium\n\n\nAbstract\nFree probabi lity is a noncommutative probability theory introduced by Voiculescu in th e 1980s\, motivated by operator algebras and free groups\, and useful in r andom matrix theory. Where classical independence relates to the tensor pr oduct of algebras\, free independence relates to the free product of algeb ras. Speicher discovered the combinatorial substrate of the theory: noncro ssing partitions. He derived the free cumulant-moment relations from Möbi us inversion in the incidence algebra of the lattice of noncrossing partit ions\, and used it\, via two reduction procedures\, to model free multipli cative convolution. A crucial ingredient\, which has no analogue in the cl assical setting\, is the notion of Kreweras complement of a noncrossing pa rtition. In this talk\, after a long introduction to these topics\, I will explain some more categorical viewpoints. A first step is an operad of no ncrossing partitions. A second step is a decomposition space (2-Segal spac e) Y of noncrossing hyperchords\, whose simplicial structure encodes highe r versions of Kreweras complementation. The incidence bialgebra of Y is a direct combinatorial model for free multiplicative convolution. It is rela ted to the previous models by the standard simplicial notion of decalage: the first decalage of Y gives the (two-sided bar construction of the) oper ad\, and the second decalage gives the lattice. These two decalages encode precisely Speicher's two reductions.\n\nThis is joint work with Kurusch E brahimi-Fard\, Loïc Foissy\, and Frédéric Patras.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/7/ END:VEVENT BEGIN:VEVENT SUMMARY:Emily Riehl DTSTART:20210506T170000Z DTEND:20210506T180000Z DTSTAMP:20260423T094652Z 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 someth ing to exist uniquely? Classically\, to say that a set A has a unique elem ent means that there is an element x of A and any other element y of A equ als x. When this assertion is applied to a space A\, instead of a mere set \, and interpreted in a continuous fashion\, it encodes the statement that the space A is contractible\, i.e.\, that A is continuously deformable to a point. This talk will explore this notion of contractibility as uniquen ess and its role in generalizing from ordinary categories to infinite-dime nsional categories.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/8/ END:VEVENT BEGIN:VEVENT SUMMARY:Maria Emilia Maietti DTSTART:20210513T170000Z DTEND:20210513T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/9 DESCRIPTION:Title: Quotient completions for topos-like structures\nby Ma ria Emilia Maietti as part of Topos Institute Colloquium\n\n\nAbstract\nIn this talk we report fundamental results concerning free completions with quotients of specific Lawvere doctrines for building toposes\, quasi-topos es and predicative versions of them. Our final goal is to use such complet ions for modelling foundations of constructive and classical mathematics w hich are predicative in the sense of Poincaré\, Weyl and Feferman\, inclu ding that in [M09]. We first recall how the tool of completing an elementa ry existential Lawvere doctrine with exact quotients is the fundamental co nstruction behind the tripos-to-topos construction in [HJP80] beside inclu ding as instances both the exact completion of a regular category and that of a weakly lex finite product category\, as reported in [MR15]. We then describe recent work with Fabio Pasquali and Pino Rosolini where we show h ow the elementary quotient completion of an elementary Lawvere doctrine in [MR13] is the fundamental construction behind a tripos-to-quasi-topos con struction including toposes as exact completions of a left exact category in [Me03] as instances. We also mention a joint work with Davide Trotta wh ere we extend results in [MPR17] about tripos-to-topos constructions coinc iding with exact completions of a left exact category. We end by applying the elementary quotient completion to build examples of predicative topo ses including the Effective Predicative Topos in [MM21].\n\nReferences\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. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pu re and Applied Logic\, 160(3): 319-354\, 2009\n\n[MR13] M.E. Maietti and G . Rosolini. Elementary quotient completion. Theory and Applications of Cat egories\, 27(17): 445–463\, 2013\n\n[MR15 ] M.E. Maietti and G. Rosolini . Unifying Exact Completions. Applied Categorical Structures 23(1): 43-52\ , 2015\n\n[MPR17] M.E. Maietti\, F. Pasquali and G. Rosolini. Triposes\, e xact completions\, and Hilbert's ε-operator. Tbilisi Mathematical Journal . 10(3): 141-66\, 2017\n\n[Me03] M. Menni. A characterization of the left exact categories whose exact completions are toposes. Journal of Pure and Applied Algebra\, 3(177): 287-301\, 2003\n\n[MM21] M.E. Maietti\, S. Masch io. A predicative variant of Hyland's Effective Topos. To appear in The Jo urnal of Symbolic Logic\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/9/ END:VEVENT BEGIN:VEVENT SUMMARY:Tobias Fritz DTSTART:20210520T170000Z DTEND:20210520T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/10 DESCRIPTION:Title: The law of large numbers in categorical probability\ nby Tobias Fritz as part of Topos Institute Colloquium\n\n\nAbstract\nThe law of large numbers (in its various guises) can be regarded as the most c entral result of probability theory\, and any serious axiomatic system for probability must reproduce it in some form. After a general introduction to categorical probability in terms of Markov categories\, I will explain how to formulate a form of the strong law of large numbers within this fra mework\, namely the Glivenko-Cantelli theorem on the convergence of the em pirical distribution. I will also sketch how to use this statement in orde r to derive other laws of large numbers from it.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/10/ END:VEVENT BEGIN:VEVENT SUMMARY:Michael Shulman DTSTART:20210527T170000Z DTEND:20210527T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/11 DESCRIPTION:Title: Two-dimensional semantics of homotopy type theory\nb y Michael Shulman as part of Topos Institute Colloquium\n\n\nAbstract\nThe general higher-categorical semantics of homotopy type theory involves ( ∞\,1)-toposes and Quillen model categories. However\, for many applicati ons it suffices to consider (2\,1)-toposes\, which are reasonably concrete categorical objects built out of ordinary groupoids. In this talk I'll d escribe how to interpret homotopy type theory in (2\,1)-toposes\, and some of the applications we can get from\nsuch an interpretation. I will assum e a little exposure to type theory\, as in Dan Christensen's talk from Apr il\, but no experience with higher toposes or homotopy theory. This talk w ill also serve as an introduction to some basic notions of Quillen model c ategories\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/11/ END:VEVENT BEGIN:VEVENT SUMMARY:Steve Awodey DTSTART:20210603T170000Z DTEND:20210603T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/12 DESCRIPTION:Title: Model Structures from Models of HoTT\nby Steve Awode y 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 Quillen model category\, even if only implicitly. From the interpretation of identitie s between terms as paths in an abstract space\, to the univalence principl e identifying identities of types with homotopy equivalences of spaces\, t he standard tools of abstract homotopy theory provide the means to make ri gorous the basic intuition behind the homotopical interpretation of the fo rmal 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 categori cal model of HoTT of an appropriate kind\, one can construct from it a ful l Quillen model structure on the underlying category. This can be seen as a further strengthening of the idea of HoTT as the internal language of a n $\\infty$-topos.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/12/ END:VEVENT BEGIN:VEVENT SUMMARY:Kathryn Hess DTSTART:20210624T180000Z DTEND:20210624T190000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/13 DESCRIPTION:Title: From comonads to calculus\nby Kathryn Hess as part o f Topos Institute Colloquium\n\n\nAbstract\nAbstracting the framework comm on to most flavors of functor calculus\, one can define a calculus on a ca tegory M equipped with a distinguished class of weak equivalences to 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 testing whe ther morphisms in M are weak equivalences.\n\nIn this talk\, after making the definition above precise\, I will describe a machine for creating calc uli on functor categories Fun (C\,M) that is natural in both the source C and the target M. Our calculi arise by comparison of the source category C with a tower of test categories\, equipped with cubical structure of prog ressively higher dimension\, giving rise to sequences of resolutions of fu nctors from C to M\, built from comonads derived from the cubical structur e on the test categories. The stages of the towers of functors that we ob tain measure how far the functor we are analyzing deviates from being a co algebra over each of these comonads. The naturality of this construction makes it possible to compare both different types calculi on the same func tor 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://researchseminars.org/talk/ToposInstituteColloquium/13/ END:VEVENT BEGIN:VEVENT SUMMARY:Asgar Jamneshan DTSTART:20210415T170000Z DTEND:20210415T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/14 DESCRIPTION:Title: Topos theory and measurability\nby Asgar Jamneshan a s part of Topos Institute Colloquium\n\n\nAbstract\nIn point-free (or abst ract) measure theory measurable spaces are replaced by $\\sigma$-complete Boolean algebras\, measurable functions by Boolean homomorphisms\, and mea sure spaces by measure algebras. This more general perspective has some ad vantages over the traditional pointwise approach to measure theory. For ex ample\, it facilitates the use of topos-theoretic techniques to study meas urability. To this effect\, a translation process between the internal lan guage/ logic of certain Boolean topoi and the "usual" external language/ l ogic is required which we can accomplish by using the formalism of conditi onal analysis. We illustrate this with some recent applications in ergodi c theory.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/14/ END:VEVENT BEGIN:VEVENT SUMMARY:Chris Heunen DTSTART:20210617T170000Z DTEND:20210617T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/15 DESCRIPTION:Title: Sheaf representation of monoidal categories\nby Chri s Heunen as part of Topos Institute Colloquium\n\n\nAbstract\nWouldn't it be great if monoidal categories were nice and easy? They are! We will disc uss how a monoidal category embeds into a "nice" one\, and how a "nice" mo noidal category consists of global sections of a sheaf of "easy" monoidal categories. This theorem cleanly separates "spatial" and "temporal" direct ions of monoidal categories.\n\nMore precisely\, "nice" means that certain morphisms into the tensor unit have joins that are respected by tensor pr oducts\, namely those morphisms that are central and idempotent with respe ct to the tensor product. By "easy" we mean that the topological space of which these central idempotents form the opens is a lot like a singleton s pace\, namely local.\n\nCategorifying flabby sheaves in the appropriate wa y makes the representation functorial from monoidal categories to schemes of local monoidal categories. The representation respects many properties of monoidal categories: if a monoidal category is closed/traced/complete/B oolean\, then so are its local stalks. As instances we recover the Lambek- Moerdijk-Awodey sheaf representation for toposes\, the Stone representatio n of Boolean algebras\, the representation by germs of open subsets of a t opological space\, and the Takahashi representation of Hilbert modules as continuous fields of Hilbert spaces.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/15/ END:VEVENT BEGIN:VEVENT SUMMARY:Shaowei Lin DTSTART:20210422T170000Z DTEND:20210422T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/16 DESCRIPTION:Title: Proofs as programs: challenges and strategies for progra m synthesis\nby Shaowei Lin as part of Topos Institute Colloquium\n\n\ nAbstract\nThe Curry-Howard correspondence between proofs and programs sug gests that we can exploit proof assistants for writing software. I will di scuss the challenges behind a naïve execution of this idea\, and some pre liminary strategies for overcoming them. As an example\, we will organize higher-order information in knowledge graphs using dependent type theory\, and automate the answering of queries using a proof assistant. In another example\, we will explore how decentralized proof assistants can enable m athematicians or programmers to work collaboratively on a theorem or appli cation. If time permits\, I will outline connections to canonical structur es (ssreflect)\, reflection (ssreflect)\, transport\, unification and univ erse management.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/16/ END:VEVENT BEGIN:VEVENT SUMMARY:Geoffrey Cruttwell DTSTART:20210708T170000Z DTEND:20210708T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/17 DESCRIPTION:Title: Categorical differential structures and their role in ab stract machine learning\nby Geoffrey Cruttwell as part of Topos Instit ute Colloquium\n\n\nAbstract\nA fundamental component of many machine lear ning algorithms is differentiation. Thus\, if one wishes to abstract and generalize aspects of machine learning\, it is useful to have an abstract perspective on differentiation. There has been much work on categorical d ifferential structures in the past few years with the advent of differenti al categories\, Cartesian differential categories\, and tangent categories . In this talk I'll focus on Cartesian reverse differential categories\, a recent variant of Cartesian differential categories\, and touch on how t hey can be used in abstract machine learning.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/17/ END:VEVENT BEGIN:VEVENT SUMMARY:Walter P Tholen DTSTART:20210722T170000Z DTEND:20210722T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/18 DESCRIPTION:Title: What is monoidal topology?\nby Walter P Tholen as pa rt of Topos Institute Colloquium\n\n\nAbstract\nMonoidal topology may be s een as being inspired by some visionary remarks in Hausdorff‘s „Grundz üge der Mengenlehre“ of 1914\, and it takes its modern lead from two di stinct seminal contributions of the early 1970s: the Manes-Barr presentati on of topological spaces in terms of ultrafilter convergence axioms\, and Lawvere’s presentation of metric spaces as small categories enriched in the extended non-negative half-line of the reals. Both types of spaces bec ome instances of small so-called (T\,V)-categories\, where T is a Set-mona d and V a (commutative) quantale\, i.e. a small\, thin and (symmetric) mon oidal-closed category. The setting therefore allows for a general study of „spaces“ that combines geometric and numerical aspects in a natural w ay.\n\nIn this talk we present some key elements of the theory and its app lications\, showing in particular how the strictification and inversion of some naturally occurring inequalities in this lax-monoidal setting leads to interesting topological properties and unexpected connections. Time pe rmitting\, we will also point to some on-going and future work in the area .\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/18/ END:VEVENT BEGIN:VEVENT SUMMARY:Marcy Robertson DTSTART:20210729T220000Z DTEND:20210729T230000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/19 DESCRIPTION:Title: Topological Inspiration for Infinity Modular Operads \nby Marcy Robertson as part of Topos Institute Colloquium\n\n\nAbstract\n A modular operad can be thought of as an undirected network which allows f or feedback “loops”. An infinity modular operad is such a network wher e 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 infinity modular operads\, focusing on the topological origins of the idea. The aud ience is not expected to be familiar with operads or topology. This talk w ill cover snippets of joint work with Luci Bonatto\, Pedro Boavida\, Phili p Hackney \, Geoffroy Horel and Donald Yau.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/19/ END:VEVENT BEGIN:VEVENT SUMMARY:Eugene Lerman DTSTART:20210610T170000Z DTEND:20210610T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/20 DESCRIPTION:Title: A category of hybrid systems\nby Eugene Lerman as pa rt of Topos Institute Colloquium\n\n\nAbstract\nHybrid systems are dynamic al systems that exhibit both continuous time evolution and abrupt transiti ons. Examples include mechanical systems (e.g.\, a ball bouncing off a flo or) and cyber-physical systems (e.g.\, a room with a thermostat). Definiti ons of a hybrid dynamical systems vary widely in literature but they usual ly include directed graphs\, spaces with vector fields attached to the nod es of graphs and partial maps or\, more generally\, relations attached to the edges of graphs. The vector fields are used to model continuous evolut ion and the relations the abrupt transitions.\n\nI wanted to understand if analogues of coupled cell networks of Golubitsky\, Stewart and their coll aborators (these are highly structured coupled systems of ODEs) make sense for hybrid dynamical systems. In order to do that I needed to make sense of open hybrid systems\, their interconnection\, networks of hybrid syste ms and maps between networks of hybrid systems.\n\nProceeding by analogy w ith continuous time systems I introduced the notion of a hybrid phase spac e and its underlying manifold. A hybrid phase space can be succinctly def ined as double functor. Hybrid phase spaces form a category HyPh with mo rphisms coming from vertical natural transformations. A hybrid dynamical s ystem is a pair (A\,X) where A is a hybrid phase space and X is a vector f ield on the manifold U(A) underlying A. I then constructed a category HyDS of hybrid dynamical system. The definition of HyDS passes a couple of san ity checks.\n\nUsing the foundation laid out above James Schmidt and I sho wed that one can also define hybrid surjective submersions\, hybrid open systems\, their interconnections and networks of hybrid systems. This way one can model systems of bouncing balls and several interconnected rooms with separate thermostats.\n\nReferences: arXiv:1612.01950 [math.DS] and a rXiv:1908.10447 [math.DS] (DOI: 10.1016/j.geomphys.2019.103582).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/20/ END:VEVENT BEGIN:VEVENT SUMMARY:Jonathan Gorard DTSTART:20210429T170000Z DTEND:20210429T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/21 DESCRIPTION:Title: Fast Diagrammatic Reasoning and Compositional Approaches to Fundamental Physics\nby Jonathan Gorard as part of Topos Institute Colloquium\n\n\nAbstract\nThe Wolfram Model — a discrete spacetime mode l based upon hypergraph rewriting — can be naively formalized as a conve ntional double-pushout rewriting system over a partial adhesive category o f (directed) hypergraphs. However\, the abstract rewriting structure of th e model also permits an elegant interpretation in terms of dagger compact categories\, with considerable formal analogies to FdHilb and the foundati ons of categorical quantum mechanics\, yet with an additional causal seman tics definable in terms of a second symmetric strict partial monoidal stru cture (such that the entire system can be formalized\, for instance\, in t erms of a double category or a weak 2-category). In addition to potentiall y defining a general categorical semantics for discrete models of quantum gravity\, this formalism presents a fundamentally new approach to performi ng efficient diagrammatic reasoning over combinatorial structures\, by sug gesting 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 making mo re explicit use of the causal structure of the abstract rewriting system i n the choice of which inference rules to apply. We show how this approach can be applied to the problem of enacting fast diagrammatic simplification of circuits in quantum information theory\, as well as (time-permitting) the problem of efficiently discretizing the Cauchy problem in numerical ge neral relativity\, showcasing comparisons against some existing software f rameworks and algorithms.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/21/ END:VEVENT BEGIN:VEVENT SUMMARY:Todd Trimble DTSTART:20210805T170000Z DTEND:20210805T180000Z DTSTAMP:20260423T094652Z 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 summarize som e aspects of recent work with John Baez and Joe Moeller\, which aims to ti e together representations of symmetric groups\, Schur functors\, and lamb da rings from the point of view of 2-rigs\, which are a categorification o f ordinary 'rigs' or rings without negatives. A common theme in this area is the notion of 'plethory'. We sketch how the archetypal plethory of lamb da rings arises simply and naturally from the simplest possible '2-plethor y'\, and applying decategorification to it.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/22/ END:VEVENT BEGIN:VEVENT SUMMARY:Pawel Sobocinski DTSTART:20210930T150000Z DTEND:20210930T160000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/23 DESCRIPTION:Title: Algebraic theories with string diagrams\nby Pawel So bocinski as part of Topos Institute Colloquium\n\n\nAbstract\nIn Lawvere t heories the central role is played by categories with finite products. The free category with finite products on one object (FinSet^op) is the Lawve re theory of the empty algebraic theory\, and the free category with finit e products on a signature (of an algebraic theory) has a concrete descript ion as a category of classical syntactic terms. But\, using a theorem due to Thomas Fox\, we can also capture these categories nicely using string d iagrams.\n\nThe string diagrammatic approach gets you further than ordinar y syntax. In a POPL 21 paper with Ivan Di Liberti\, Fosco Loregian and Cha d Nester\, we developed a Lawvere-style approach to algebraic theories wit h partially defined operations. It turns out that in this setting\, instea d of categories with finite products\, the relevant concept is discrete ca rtesian restriction categories (dcrc). And string diagrams are the right s yntax for this setting: they let us describe the free dcrc on an object an d the free dcrc on a signature. I will sketch some of our results and talk about some of the ramifications\, including a string diagrammatic descrip tion of categories with free finite limits.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/23/ END:VEVENT BEGIN:VEVENT SUMMARY:John Bourke DTSTART:20210909T170000Z DTEND:20210909T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/24 DESCRIPTION:Title: Tensor products\, multimaps and internal homs\nby Jo hn Bourke as part of Topos Institute Colloquium\n\n\nAbstract\nThe notions of monoidal category\, multicategory and closed category are closely rela ted\, with each having their own advantages. Considering the relationship between them leads naturally to skew variants — skew monoidal categorie s\, skew multicategories and skew closed categories — and I will explore some of these variants in this talk.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/24/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrew J. Blumberg DTSTART:20210923T170000Z DTEND:20210923T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/25 DESCRIPTION:Title: Abstract homotopy theory for topological data analysis\nby Andrew J. Blumberg as part of Topos Institute Colloquium\n\n\nAbstr act\nA starting point for the modern perspective on algebraic topology is the Eilenberg-Steenrod axioms characterizing homology theories. More gene rally\, there has been a great deal of work starting from insights of Verd ier\, Quillen\, and Dwyer-Kan that gives abstract characterizations of the structures of homotopy theory in terms of formal cylinder and suspension objects or mapping spaces. This talk will be about efforts to understand the invariants of topological data analysis from an abstract perspective. There will be many more questions than answers.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/25/ END:VEVENT BEGIN:VEVENT SUMMARY:Lawrence Paulson DTSTART:20210701T170000Z DTEND:20210701T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/26 DESCRIPTION:Title: Formalising Contemporary Mathematics in Simple Type Theo ry\nby Lawrence Paulson as part of Topos Institute Colloquium\n\n\nAbs tract\nA long-standing question in mathematics is the relevance of formali sation to practice. Rising awareness of fallibility among mathematicians s uggests 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 mathematic al topics have been formalised in simple type theory using Isabelle/HOL. T he partition calculus was introduced by Erdös and R. Rado in 1956 as the study of “analogues and extensions of Ramsey’s theorem”. Highly tech nical results were obtained by Erdös-Milner\, Specker and Larson (among m any others) for the case of ordinal partition relations\, which is concern ed with countable ordinals and order types. Much of this material was form alised last year (with the assistance of Džamonja and Koutsoukou-Argyraki ). \n\nGrothendieck's Schemes have also been formalised in Isabelle/HOL. T his achievement is notable because some prominent figures had conjectured that schemes were beyond the reach of simple type theory.\n\nSome highligh ts of this work will be presented along with general observations about ro le of type theory in the formalisation of mathematics.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/26/ END:VEVENT BEGIN:VEVENT SUMMARY:Jamie Vicary DTSTART:20210916T170000Z DTEND:20210916T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/27 DESCRIPTION:Title: Understanding free infinity-categories\nby Jamie Vic ary as part of Topos Institute Colloquium\n\n\nAbstract\nInfinity-categori es have a reputation for being difficult algebraic objects to define and w ork with. In this talk I will present a new definition of free infinity-ca tegory that demystifies them\, and makes them easy to understand from an a lgebraic perspective. The definition is given as a sequence of inductive-r ecursive data structures\, and we explore how this relates to Grothendieck 's original ideas on infinity-categories. No knowledge of infinity-categor ies is required to follow this talk!\n\nThis is joint work with Christophe r Dean\, Eric Finster\, Ioannis Markakis and David Reutter.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/27/ END:VEVENT BEGIN:VEVENT SUMMARY:Valeria de Paiva DTSTART:20210819T170000Z DTEND:20210819T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/28 DESCRIPTION:Title: Categorical Explicit Substitutions\nby Valeria de Pa iva as part of Topos Institute Colloquium\n\n\nAbstract\nThe advantages of functional programming are well-known: programs are easier to write\, und erstand and verify than their imperative counterparts. However\, functiona l languages tend to be more memory intensive and these problems have hinde red their wider use in industry. The xSLAM project tried to address these issues by using *explicit substitutions* to construct and implement more e fficient abstract machines\, proved correct by construction.\n\nIn this ta lk I recap two results from the xSLAM project which haven't been sufficien tly discussed. First\, we provided categorical models for the calculi of e xplicit substitutions (linear and cartesian) that we are interested in. No one else seems to have provided categorical models for explicit substitut ions calculi\, despite the large number of explicit substitutions systems available in the literature. Indexed categories provide models of cartesi an calculi of explicit substitutions. However\, these structures are inher ently non-linear and hence cannot be used to model *linear* calculi of exp licit substitutions. Our work replaces indexed categories with pre-sheave s\, thus providing a categorical semantics covering both the linear and ca rtesian cases. Our models satisfy soundness and completeness\, as expected . \n\nSecondly\, we recall a different linear-non-linear type theory\, bui lt from Barber and Plotkin DILL ideas\, which\, like DILL\, is better for implementations. Unlike DILL\, this type theory\, called ILT\, satisfies an internal language theorem. Thus we describe ILT\, show categorical sema ntics for it and sketch the proof of its internal language theorem\, thus justifying its use in implementations. These results are examples of `(ca tegorically) structured deep syntax'\, to borrow Hyland's characterizatio n.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/28/ END:VEVENT BEGIN:VEVENT SUMMARY:Anders Mortberg DTSTART:20211007T150000Z DTEND:20211007T160000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/29 DESCRIPTION:Title: Cubical Methods in Homotopy Type Theory and Univalent Fo undations\nby Anders Mortberg as part of Topos Institute Colloquium\n\ n\nAbstract\nOne of the aims of Homotopy Type Theory and Univalent Foundat ions (HoTT/UF) is to provide a practical foundation for computer formaliza tion of mathematics by building on deep connections between type theory\, homotopy theory and (higher) category theory. Some of the key inventions o f HoTT/UF include Voevodsky's univalence axiom relating equality and equiv alence of types\, the internal stratification of types by the complexity o f their equality\, as well as higher inductive types which allow synthetic reasoning about spaces in type theory. In order to provide computational support for these notions various cubical type theories have been invented . In particular\, the Agda proof assistant now has a cubical mode which ma kes it possible to work and compute directly with the concepts of HoTT/UF. In the talk I will discuss some of the mathematical ideas which motivate these developments\, as well as show examples of how computer mechanizatio n of mathematics looks like in Cubical Agda. I will not assume expert know ledge of HoTT/UF and key concepts will be introduced throughout the talk.\ n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/29/ END:VEVENT BEGIN:VEVENT SUMMARY:Andreas Blass DTSTART:20211014T170000Z DTEND:20211014T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/30 DESCRIPTION:Title: A topos view of axioms of choice for finite sets\nby Andreas Blass as part of Topos Institute Colloquium\n\n\nAbstract\nTarski proved (in set theory without choice) that if one assumes that\nall famil ies of 2-element sets have choice functions then one can\nprove that all f amilies of 4-element sets have choice functions.\nMostowski (1937) investi gated similar implications\, giving\nnumber-theoretic and group-theoretic conditions\, some necessary and\nsome sufficient for such implications. B ut some questions remained\nunsolved\, in particular: Do choice from 3-ele ment sets\, from 5-element\nsets\, and from 13-element sets together imply choice from 15-element\nsets. Gauntt (1970) resolved those remaining que stions\, 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://researchseminars.org/talk/ToposInstituteColloquium/30/ END:VEVENT BEGIN:VEVENT SUMMARY:Chris Kapulkin DTSTART:20211021T170000Z DTEND:20211021T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/31 DESCRIPTION:Title: Cubical setting for Discrete Homotopy Theory\nby Chr is Kapulkin as part of Topos Institute Colloquium\n\n\nAbstract\nDiscrete homotopy theory\, developed by H. Barcelo and collaborators\, is a homotop y theory of (simple) graphs. Homotopy invariants of graphs have found nume rous applications\, for instance\, in the theory of matroids\, hyperplane arrangements\, and time series analysis. Discrete homotopy theory is also a special instance of a homotopy theory of simplicial complexes\, develope d by R. Atkin\, to study social and technological networks.\n\nIn the talk \, I will introduce the main concepts and open problems of discrete homoto py theory. I will also report on the joint work with D. Carranza on develo ping a new foundation for discrete homotopy theory in the category of cubi cal sets\, which offers solutions to a number of long standing open proble ms in the field.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/31/ END:VEVENT BEGIN:VEVENT SUMMARY:Dorette Pronk DTSTART:20211028T170000Z DTEND:20211028T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/32 DESCRIPTION:Title: Doubly Lax Colimit of Double Categories with Application s\nby Dorette Pronk as part of Topos Institute Colloquium\n\n\nAbstrac t\nThus far\, lax and oplax pseudo colimits of double categories have been considered in two flavours [2]: horizontally lax and vertically lax\, bas ed on the notions of horizontal and vertical transformations (respectively ) between double functors. Also\, the diagrams of double categories have t ypically been indexed by a 2-category.\n\nIn this work we introduce diagra ms indexed by a double category\; in order to make sense of this we will m ap into a version of the quintets of the category of double categories\, b ecause this category itself is only enirched in double categories and is o ften taken as a 2-category. Between the new indexing functors we introduce a new notion of transformation\, namely doubly lax transformation. We the n introduce a double categorical version of the Grothendieck construction and show that it has a universal property as doubly lax colimit of the dia gram\; i.e.\, a colimit that is lax with respect to the new transformation s.\n\nAs applications we obtain:\n\n— a universal property as lax colimi t for the Grothendieck construction for bicategories described in [1]\;\n\ n— a universal property for the elements construction for double categor ies\;\n\n— a notion of fibration for double categories\, different from the internal one described by Street and others\;\n\n— a double categori cal generalization of the classical tom Dieck fundamental groupoid for a s pace with an action by a topological group.\n\nThis is joint work with Mar zieh Bayeh (University of Ottawa) and Martin Szyld (Dalhousie University). \n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/32/ END:VEVENT BEGIN:VEVENT SUMMARY:Kevin Buzzard DTSTART:20210812T170000Z DTEND:20210812T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/33 DESCRIPTION:Title: What is the point of Lean's maths library?\nby Kevin Buzzard as part of Topos Institute Colloquium\n\n\nAbstract\nLean is a co mputer proof checker developed by Microsoft Research. Over the last four y ears I have been part of a team of mathematicians and computer scientists who have got it into their heads that it is somehow "obviously" a good ide a to build a formally verified library of modern mathematics in Lean. You can think of it as a 21st century Bourbaki if you like\, although our plan s are actually far grander than Bourbaki's. I will talk about two things: (1) how it's going and (2) why we're doing it. No background in computer p roof checkers will be necessary to follow the talk.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/33/ END:VEVENT BEGIN:VEVENT SUMMARY:Conor McBride DTSTART:20210826T170000Z DTEND:20210826T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/34 DESCRIPTION:Title: Cats and Types: Best Friends?\nby Conor McBride as p art of Topos Institute Colloquium\n\n\nAbstract\nIntensional Type Theory a nd Category Theory ought to fit well together\, but the current practical experience of representing concepts from one with the tools of the other i s often quite strained. On the one hand\, fibrational approaches to depend ency often seem heavy. On the other hand\, definitional equality in type s ystems often falls way short of delivering even the simplest of coherences . In this talk\, I shall reflect on the problems and search for opportunit ies. What has to change to make type theoretic proof assistants a good med ium for categorical approaches to programming and proof? I wish I knew the answer to that question! I can at least offer a few clues. For example\, I shall exhibit a universe of indexed inductively defined datatypes which exhibit nontrivial presheaf structure by construction.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/34/ END:VEVENT BEGIN:VEVENT SUMMARY:Evan Patterson DTSTART:20211202T170000Z DTEND:20211202T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/35 DESCRIPTION:Title: Categories of diagrams in data migration and computation al physics\nby Evan Patterson as part of Topos Institute Colloquium\n\ n\nAbstract\nDiagrams are among the most fundamental and ubiquitous concep ts of category theory. Less appreciated are the several notions of morphis m between diagrams in a category. After reviewing the resulting categories of diagrams\, this talk will explain their central role in two recent pro jects by the author and collaborators. First\, due to their close connecti ons with limits and colimits\, the categories of diagrams provide a natura l syntax for defining flexible data migrations between categorical databas es. We describe a prototype implementation of this system in Catlab.jl. In the second part of the talk\, we explain how "Tonti diagrams\," diagramma tic presentations of physics equations expressed in vector calculus or ext erior calculus\, can be formalized using category-theoretic diagrams. When combined with a suitable discretization scheme\, such as the discrete ext erior calculus (DEC)\, the result is a diagrammatic and compositional appr oach to building numerical simulators of physical systems.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/35/ END:VEVENT BEGIN:VEVENT SUMMARY:Robert Harper DTSTART:20211209T170000Z DTEND:20211209T180000Z DTSTAMP:20260423T094652Z 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 with Jon Sterling and Yue Niu)\n\nThe informal phase distinction between compile-ti me and run-time in programming languages is formally manifested by the dis tinction between kinds\, which classify types\, and types\, which classify code. The distinction underpins standard programming methodology whereby code is first type-checked for consistency before being compiled for execu tion. When used effectively\, types help eliminate bugs before they occur. \n\nProgram modules\, in even the most rudimentary form\, threaten the dis tinction\, comprising as they do both types and programs in a single unit. Matters worsen when considerating "open" modules\, with free module varia bles standing for its imports. To maintain the separation in their presenc e it is necessary to limit the dependency of types\, the static parts of a module\, to their imported types. Such restrictions are fundamental for u sing dependent types to express modular structure\, as originally suggeste d by MacQueen.\n\nTo address this question Moggi gave an "analytic" formul ation of program modules in which modules are explicitly separated into th eir static and dynamic components using tools from category theory. Recent work by Dreyer\, Rossberg\, and Russo develops this approach fully in the ir account of ML-like module systems. In this talk we consider instead a " synthetic" formulation using a proposition to segregate the static from th e dynamic\, in particular to define static equivalence to manage type shar ing and type dependency\n\nRobert Harper is a Professor of Computer Scienc e at Carnegie Mellon\, where he\nhas been a member of faculty since 1988. He is past recipient of the Allen\nNewell Award for research excellence an d the Herbert Simon Award for teaching\nexcellence. He is author of Practi cal Foundations for Programming Languages\, a\ntextbook account of program ming language theory. His work focuses on the\napplication of type theory to program development\, language design\, compiler\nconstruction\, and m echanized proof.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/36/ END:VEVENT BEGIN:VEVENT SUMMARY:Paolo Perrone DTSTART:20211118T170000Z DTEND:20211118T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/37 DESCRIPTION:Title: The rise of quantitative category theory\nby Paolo P errone as part of Topos Institute Colloquium\n\n\nAbstract\nIn several dom ains of applications\, category theory can be useful to add conceptual cla rity and scalability to mathematical models.\nHowever\, ordinary categorie s often fail to grasp some quantitative aspects: the total cost of a certa in strategy\, the number of composite steps\, the discrepancy between a co ncrete construction and its ideal model\, and so on.\n\nIn order to incorp orate these aspects\, it is helpful to switch to a "quantitative" version of categories: weighted categories. These are particular enriched categori es where each arrow carries a number\, or "weight"\, as in a weighted grap h. The composition of paths comes with a triangle inequality\, analogous t o the one of metrics and norms\, which equips universal properties with qu antitative bounds. Most results in category theory have a weighted analogu e\, which often carries additional geometric or analytic significance.\nWe ighted categories have been around since early work of Lawvere\, but only in the last few years researchers are starting to recognize their importan ce. More and more recent papers are using them in fields as diverse as top ological data analysis\, geometry\, and probability theory\, some times ev en rediscovering the concepts independently.\n\nIn this talk we are going to see what it's like to work with weighted categories\, their relationshi p with graphs\, and the quantitative aspects about limits and colimits. We will also define a weighted analogue of lenses\, and use it to express li ftings of transport plans between probability measures.\n\nRelevant litera ture: arxiv.org/abs/2110.06591 and additional work in preparation.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/37/ END:VEVENT BEGIN:VEVENT SUMMARY:Florian Rabe DTSTART:20210902T170000Z DTEND:20210902T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/38 DESCRIPTION:Title: MMT: A UniFormal Approach to Knowledge Representation\nby Florian Rabe as part of Topos Institute Colloquium\n\n\nAbstract\nUn iFormal is the idea of representing all aspects of knowledge uniformly\, i ncluding narration\, deduction\, computation\, and databases.\nMoreover\, it means to abstract from the multitude of individual systems\, which not only often focus on just one aspect but are doing so in mutually incompati ble ways\, thus creating a universal framework of formal knowledge.\n\nMMT is a concrete representation language to that end.\nIt systematically abs tracts from assumptions typically inherent in the syntax and semantics of concrete systems\, and focuses on language-independence\, modularity\, and system interoperability.\nWhile constantly evolving in order to converge towards UniFormal\, its design and implementation have become very mature. \nIt is now a readily usable high-level platform for the design\, analysis \, and implementation of formal systems.\n\nThis talk gives an overview of the current state of MMT\, its existing successes and its future challeng es.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/38/ END:VEVENT BEGIN:VEVENT SUMMARY:Jeremy Avigad DTSTART:20211104T180000Z DTEND:20211104T190000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/39 DESCRIPTION:Title: Formal mathematics\, dependent type theory\, and the Top os Institute\nby Jeremy Avigad as part of Topos Institute Colloquium\n \n\nAbstract\nModern logic tells us that mathematics can be formalized\, i n principle. Computational proof assistants\, developed over the last half century\, make it possible to do so in practice. In this talk\, I will br iefly survey the state of the field today and discuss some of the reasons that formalization is desirable. I will discuss one particular proof assis tant\, Lean\, and its library\, mathlib. I will explain why dependent type theory\, Lean's underlying logical framework\, provides an attractive pla tform for formalization. Finally\, I will consider ways that formal mathem atics can support and enhance the Topos Institute's missions.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/39/ END:VEVENT BEGIN:VEVENT SUMMARY:David Danks DTSTART:20220217T170000Z DTEND:20220217T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/40 DESCRIPTION:Title: Ethics in AI\, not Ethics of AI\nby David Danks as p art of Topos Institute Colloquium\n\n\nAbstract\nDiscussions of the ethica l (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 irrelevant to research and development of AI systems. In contrast\, I will argue that ethical issues arise throughout every step of AI creation\, including res earch efforts that seem to be outside of the scope of ethics. That is\, et hics is an intrinsic part of AI\, not something that arises only after the fact. Throughout this argument\, I will provide examples of practical too ls and practices to improve the ethics in one’s AI systems. These insigh ts and examples will apply to technology development in general\, includin g fundamental mathematical research.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/40/ END:VEVENT BEGIN:VEVENT SUMMARY:Bob Coecke DTSTART:20220224T170000Z DTEND:20220224T180000Z DTSTAMP:20260423T094652Z 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-l evel and requires no prior technical background. We will introduce the no tion of compositional intelligence that my Oxford-based CQ-team is trying to achieve. \n\nIn particular\, starting from the compositional match bet ween natural language and quantum\, which also extends to other domains [1 ]\, we will argue that a new generation of AI can emerge when fully pushin g this analogy while exploiting the completeness of categorical quantum me chanics [2]. \n\nWe also discuss the notion of compositionality itself\, which takes many different forms within many different contexts\, and how the one we need goes beyond previous ones [3]. \n\n[1] Vincent Wang-Masci anica\, BC (2021) Talking Space: inference from spatial linguistic meaning s. https://arxiv.org/abs/2109.06554 \n\n[2] BC\, Dom Horsman\, Aleks Kiss inger\, Quanlong Wang (2021) Kindergarden quantum mechanics graduates (... or how I learned to stop gluing LEGO together and love the ZX-calculus). https://arxiv.org/abs/2102.10984\n\n[3] BC (2021) Compositionality as we s ee it\, everywhere around us. https://arxiv.org/abs/2110.05327\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/41/ END:VEVENT BEGIN:VEVENT SUMMARY:Maaike Zwart DTSTART:20220331T170000Z DTEND:20220331T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/43 DESCRIPTION:Title: Lessons from failing distributive laws\nby Maaike Zw art as part of Topos Institute Colloquium\n\n\nAbstract\nComposing monads via distributive laws is tricky business\, as too often small mistakes are overlooked. After failing to find a distributive law for the list monad o ver itself\, I started proving that finding such a distributive law is imp ossible. At the same time\, Dan Marsden was studying the famous counterexa mple by Gordon Plotkin that probability does not distribute over non-deter minism. Together we developed an algebraic method to find and generalise s uch counterexamples\, resulting in our no-go theorems. In this talk I will explain the main ideas behind our method\, illustrated by a proof that 'p lus does not distribute over times'. Then\, I will highlight some crucial steps in our method\, which tell us which type of monads are "high risk" i n 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://researchseminars.org/talk/ToposInstituteColloquium/43/ END:VEVENT BEGIN:VEVENT SUMMARY:Thierry Coquand DTSTART:20220602T170000Z DTEND:20220602T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/44 DESCRIPTION:Title: Sheaf Cohomology in Univalent Type Theory\nby Thierr y Coquand as part of Topos Institute Colloquium\n\n\nAbstract\nIn the intr oduction of his book on Higher Topos Theory\, Jacob Lurie motivates this t heory by the fact that it allows an elegant and general treatment of sheaf cohomology. It was realised early on that these ideas could be expressed in the setting of univalent foundations/homotopy type theory (cf. the 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 surprisingly direct way. Furthermore\, all this can be formulated in a constructive met a theory\, avoiding the non effective notion of injective resolutions.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/44/ END:VEVENT BEGIN:VEVENT SUMMARY:Zoé Christoff DTSTART:20220317T170000Z DTEND:20220317T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/45 DESCRIPTION:Title: The logic of social influence in networks\nby Zoé C hristoff as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk gi ves an introduction to the use of logical tools in understanding social in fluence and social networks phenomena. Individuals often form their opinio ns by interpreting the behavior of others around them\, and by reasoning a bout how those others have formed their opinions. This leads to several we ll-known herd phenomena\, such as informational cascades\, bystander effec t\, pluralistic ignorance\, bubbles\, and polarization. For instance\, in the case of informational cascades\, agents in a sequence imitate one anot her’s choices despite having diverging private evidence\, sometimes lead ing the whole community to make the worst possible choice. Similar cascadi ng mechanisms are at the heart of diffusion phenomena in social networks. \n\nI first show how an epistemic logic modeling allows to make precise th e conditions for such cascades to form\, as well as prove their inescapabi lity. I then turn to what logical tools can do for analysing information f low and influence in social networks. I illustrate how extremely simplifie d models can yield surprising new results\, for instance about stabilizati on conditions of diffusion processes. Finally\, I discuss how logic might help us further understand how social networks affect collective decision making processes.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/45/ END:VEVENT BEGIN:VEVENT SUMMARY:Giuseppe Rosolini DTSTART:20220407T170000Z DTEND:20220407T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/46 DESCRIPTION:Title: When an elementary quotient completion is a quasitopos\nby Giuseppe Rosolini as part of Topos Institute Colloquium\n\n\nAbstra ct\nThe elementary quotient completion of an elementary doctrine generalis es the exact completion of a category with finite products and weak equali sers. I intend to present a characterisation of those elementary quotient completions which produce a quasitopos. As a corollary one gets a characte risation of the elementary quotient completions which give an elementary t opos. Our work is reminiscent of\, and gathers ideas\, from others: in par ticular\, Carboni and Vitale’s characterisation of exact completions in terms of their projective objects\, Carboni and Rosolini’s characterisat ion of locally cartesian closed exact completions\, also in the revision b y Emmenegger\, and Menni’s characterisation of the exact completions whi ch are elementary toposes. This is joint work with Maria Emilia Maietti an d Fabio Pasquali.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/46/ END:VEVENT BEGIN:VEVENT SUMMARY:Tai-Danae Bradley DTSTART:20220526T170000Z DTEND:20220526T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/47 DESCRIPTION:Title: Entropy as an Operad Derivation\nby Tai-Danae Bradle y as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk features a small connection between information theory\, algebra\, and topology—n amely\, a correspondence between Shannon entropy and derivations of the op erad of topological simplices. We will begin with a brief review of operad s and their representations with topological simplices and the real line a s the main example. We then give a general definition for a derivation of an operad in any category with values in an abelian bimodule over the oper ad. The main result is that Shannon entropy defines a derivation of the op erad of topological simplices\, and that for every derivation of this oper ad there exists a point at which it is given by a constant multiple of Sha nnon entropy. We show this is compatible with\, and relies heavily on\, a well-known characterization of entropy given by Faddeev in 1956 and a rece nt variation given by Leinster.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/47/ END:VEVENT BEGIN:VEVENT SUMMARY:Dominic Verity DTSTART:20220324T200000Z DTEND:20220324T210000Z DTSTAMP:20260423T094652Z 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 he ard the rumour that ∞-category theory is “really just like category th eory with a little homotopy theory thrown in”. Inspired by that comment\ , 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 th at simple.\n\nFirstly you will have discovered that there is no universal agreement on what an ∞-category actually is. Instead\, you’ve been met with a proliferation of ∞-categorical models\; simplicially enriched ca tegories\, quasi-categories\, (iterated) complete Segal spaces\, complicia l sets\, Θ-spaces and so on. Then you discover\, to your horror\, that ea ch one of these models supports its own particular interpretations of comm on categorical concepts\, some of which appear far more familiar than othe rs. Finally\, you realise that the relationships between the category theo ries developed for each model are also much less than clear.\n\nIf this we ren’t enough to leave anyone reaching for the Aspirin bottle\, there is more bad news to come. It quickly becomes clear that there exists quite a large gap between the informal language used to describe ∞-categorical a rguments\, in blog posts and wiki articles\, and the corresponding formal arguments expressed in any particular model of ∞-categories. Most of the se are given either as concrete constructions with simplicial (or increasi ngly cubical) objects or as abstract model category theoretic arguments. N ow I have no doubt that we “all” love a good simplicial argument\, but encoding things in this way does very little to aid our categorical intui tion.\n\nThere must be a better way!\n\nIn this talk we discuss recent dev elopments in ∞-technology that seek to address these issues. Specificall y\, we review the current state of the art in model agnostic ∞-category theory [2]\, which seeks to provide a unified account of ∞-category theo ry freed from the straight jacket of a specific model. This allows both fo r the model independent\, synthetic development of ∞-categorical results and for the transport of analytically derived such results from one model to another. We shall also see how these techniques are rapidly being refr amed in type theoretic terms\, through the development of directed type th eory [1\,3]\, thereby promising a more natural language for the formal dev elopment of ∞-categorical concepts and results.\n\nReferences\n\n[1] E. Riehl\, M. Shulman\, A type theory for synthetic ∞-categories\, High. St ruct. 1 (2017) 147224.\n\n[2] E. Riehl\, D. Verity\, Elements of ∞-categ ory theory\, Cambridge University Press\, 2022.\n\n[3] J. Weinberger\, A s ynthetic perspective on (∞\,1)-category theory: Fibrational and semantic aspects\, arXiv Preprint arXiv:2202.13132. (2022).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/48/ END:VEVENT BEGIN:VEVENT SUMMARY:Glynn Winskel DTSTART:20220303T170000Z DTEND:20220303T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/50 DESCRIPTION:Title: Making concurrency functional\nby Glynn Winskel as p art of Topos Institute Colloquium\n\n\nAbstract\nThis talk bridges between two major paradigms in computation\, the *functional*\, at basis computat ion from input to output\, and the *interactive*\, where computation react s to its environment while underway. Central to any compositional theory of interaction is the dichotomy between a system and its environment. Conc urrent games and strategies address the dichotomy in fine detail\, very lo cally\, in a distributed fashion\, through distinctions between Player mov es (events of the system) and Opponent moves (those of the environment). A functional approach has to handle the dichotomy much more ingeniously\, t hrough its blunter distinction between input and output. This has led to a variety of functional approaches\, specialised to particular interactive demands. Through concurrent games we can more clearly see what separates and connects the differing paradigms\, and show how: \n\n\n— to lift fun ctions to strategies\; the "Scott order" intrinsic to \nconcurrent games p lays a key role in turning functional dependency to causal dependency. \n \n— several paradigms of functional programming and logic arise naturall y as subcategories of concurrent games\, \nincluding stable domain theory\ ; nondeterministic dataflow\; geometry of interaction\; the dialectica in terpretation\; lenses and optics\; and \ntheir extensions to containers in dependent lenses and optics. \n\n— to transfer enrichments of strateg ies (such as to probabilistic\, quantum or real-number computation) to f unctional cases.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/50/ END:VEVENT BEGIN:VEVENT SUMMARY:Leo McElroy DTSTART:20220414T170000Z DTEND:20220414T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/51 DESCRIPTION:Title: Making Microworlds: A Framework for Making Sense by Maki ng Things\nby Leo McElroy as part of Topos Institute Colloquium\n\n\nA bstract\nPeople learn best by making things they care about\, which they s hare with others. The role of an educational technologist is to communicat e this principle through tools provided to learners. A primary item in thi s toolmakers’ toolkit is the microworld\, a concept developed by Seymour Papert as a “growing place for a specific species of powerful ideas or intellectual structures.” A microworld presents someone with a small set of ideas in an explorable environment which helps the learner recompose t hose ideas for their own personal expression. Following the development of a collection of microworlds\, we will uncover the meta-structure of the “growing place” for intellectual structures\, with the aim of identify ing a framework for making tools\, for making sense\, by making things.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/51/ END:VEVENT BEGIN:VEVENT SUMMARY:Alexandra Silva DTSTART:20220519T170000Z DTEND:20220519T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/52 DESCRIPTION:Title: Learning Weighted Automata over Principal Ideal Domains< /a>\nby Alexandra Silva as part of Topos Institute Colloquium\n\n\nAbstrac t\nIn the first part of this talk\, we discuss active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin'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 probabilis tic automata\, and in particular discuss what the setup of the problem loo ks like and how that leads (or not) to impossibility results.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/52/ END:VEVENT BEGIN:VEVENT SUMMARY:Moshe Vardi DTSTART:20220623T170000Z DTEND:20220623T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/53 DESCRIPTION:Title: Ethics Washing in AI\nby Moshe Vardi as part of Topo s Institute Colloquium\n\n\nAbstract\nOver the past decade Artificial Inte lligence\, in general\, and Machine Laerning\, in particular\, have made i mpressive advancements\, in image recognition\, game playing\, natural-lan guage understanding and more. But there were also several instances where we saw the harm \nthat these technologies can cause when they are deployed too hastily. A Tesla crashed on Autopilot\, killing the driver\; a self-d riving Uber crashed\, killing a pedestrian\; and commercial face-recogniti on systems performed terribly in audits on dark-skinned people. In respons e to that\, there has been much recent talk of AI ethics. Many organizatio ns produced AI-ethics guidelines and companies publicize their newly estab lished responsible-AI teams.\n\nBut talk is cheap. "Ethics washing" — al so called “ethics theater” — is the practice of fabricating or exagg erating a company’s interest in equitable AI systems that work for every one. An example is when a company promotes “AI for good” initiatives w ith one hand\, while selling surveillance tech to governments and corporat e customers with the other. I will argue that the ethical lens is too narr ow. The real issue is how to deal with technology's impact on society. Tec hnology is driving the future\, but who is doing the steering?\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/53/ END:VEVENT BEGIN:VEVENT SUMMARY:Nicolas Behr DTSTART:20220609T170000Z DTEND:20220609T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/54 DESCRIPTION:Title: Fundamentals of Compositional Rewriting Theory\nby N icolas Behr as part of Topos Institute Colloquium\n\n\nAbstract\nThis pres entation is based upon [1] (joint work with R. Harmer and J. Krivine). \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 novel fou ndation for reasoning about rewriting theories via so-called compositional rewriting double categories (crDCs). The design principles followed in th is approach are the typical "unify and conquer" strategy of applied catego ry theory and a particular variant of the notion of compositionality. \n\n To wit\, crDCs permit to formulate a wide variety of categorical rewriting semantics uniformly\, whereby the horizontal category for a given semanti cs models the rewriting rules\, while the vertical category models matchin gs and co-matchings of rules into objects\, and where the squares model so -called direct derivations (i.e.\, individual rewriting steps). Even befor e considering compositionality\, it is already noteworthy that in order fo r crDCs to be well-defined\, strong constraints are imposed upon the horiz ontal and vertical categories and the squares of the crDC\, which in effec t suggest categories with adhesivity properties (e.g.\, toposses\, quasi-t oposses\, adhesive HLR categories\,...) as natural starting points for con structing crDCs. In this sense\, the notion of crDCs thus permits to justi fy the by now standard approach for categorical rewriting theories develop ed over the past 20 years as being based upon categories with adhesivity p roperties (starting with the seminal work of Lack and Sobocinski on adhesi ve categories) from a clear mathematical high-level perspective.\n\nCompos itionality\, on the other hand\, is a much deeper mathematical property th at a categorical rewriting theory may carry. This property entails the exi stence of so-called Concurrency and Associativity Theorems. The former con cerns being able to reason on two-step rewriting sequences via implementin g the overall effect of the two-step rewrite via a composite rule applied in a single rewrite step\, and vice versa. The Associativity Theorem then implies that the operation of forming compositions of rewriting rules is\, in a certain sense\, associative. Compositionality is a necessary and cru cial ingredient in the stochastic mechanics and rule algebra formalism dev eloped by Behr et al. since 2015\, and which permits to provide a mathemat ically fully consistent and universal formalism for continuous- [2] and di screte-time Markov Chains [3] (central to applications of rewriting to bio - and organo-chemistry\, social network modeling\, etc.) and rule-algebrai c combinatorics [4].\n\nA central result of [1] is then that a sufficient set of conditions on a double category to model a *compositional* rewritin g theory consists in requiring certain fibrational properties for the vert ical source and target functors from squares of the double categories\, i. e.\, that they are (residual) multi-opfibrations. I will sketch how these fibrational properties in conjunction with the other crDC axioms yield a c ompletely uniform proof of both the Concurrency and the Associativity Theo rems\, and\, time permitting\, how a large variety of categorical rewritin g semantics indeed fall under the umbrella of our novel crDC formalism. \n \nFinally\, I will provide an overview of open questions and potential fru itful cross-connections of crDC theory with the TIC and broader ACT commun ities.\n\n\n[1] N. Behr\, R. Harmer and J. Krivine\, "Fundamentals of Comp ositional Rewriting Theory"\, https://arxiv.org/abs/2204.07175 \n\n[2] N. Behr\, J. Krivine\, J.L. Andersen\, D. Merkle (2021)\, "Rewriting theory f or the life sciences: A unifying theory of CTMC semantics"\, https://doi.o rg/10.1016/j.tcs.2021.07.026\n\n[3] N. Behr\, B.S. Bello\, S. Ehmes\, R. Heckel (2021)\, "Stochastic Graph Transformation For Social Network Modeli ng"\, https://doi.org/10.4204/EPTCS.350.3\n\n[4] N. Behr (2021)\, "On Sto chastic Rewriting and Combinatorics via Rule-Algebraic Methods"\, http://d x.doi.org/10.4204/EPTCS.334.2\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/54/ END:VEVENT BEGIN:VEVENT SUMMARY:Martín Escardó DTSTART:20220428T170000Z DTEND:20220428T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/55 DESCRIPTION:Title: Compact totally separated types in constructive univalen t type theory\nby Martín Escardó as part of Topos Institute Colloqui um\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). Perhaps su rprisingly\, there are infinite types X for which this decision is constru ctively possible. We call such types compact. It turns out that there are plenty of infinite compact types in any 1-topos. A basic\, but perhaps sur prising\, example is the type ℕ∞ of decreasing infinite binary sequenc es. There are plenty more\, and the purpose of this talk is to exhibit the m. No matter how hard we tried to avoid that\, all searchable types we cou ld find happen to be well-ordered. But this is just as well\, because we c an use ordinals to measure how complicated the compact types that we can w rite down in constructive univalent type theory are. Much of the above dis cussion can be carried out in (the internal language of) a 1-topos. But th en some of our constructions go beyond that\, by considering the type of a ll ordinals in a universe\, which is itself an ordinal in the next univers e\, and requires univalence and hence moves us to the realm of ∞-toposes . It remains to address the notion of total separatedness of a type X. Thi s is the condition that there are plenty of maps X → 𝟚 to "separate t he points of X" in a suitable sense. I'll rigorously define this and exhib it plenty of compact\, totally separated\, well-ordered types in univalent type theory. I will mention Johnstone's topological topos as an example o f where "compact" and "totally separated" acquire their usual topological meaning. There is an old\, non-constructive\, theorem of topology that cha racterizes the compact countable Hausdorff spaces as the countable ordinal s with the interval topology. In the topological topos\, assuming a non-co nstructive meta-language to reason about it\, the searchable objects we ge t are of this form.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/55/ END:VEVENT BEGIN:VEVENT SUMMARY:Christoph Benzmueller DTSTART:20220616T170000Z DTEND:20220616T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/56 DESCRIPTION:Title: Logico-pluralistic exploration of foundational theories with computers\nby Christoph Benzmueller as part of Topos Institute Co lloquium\n\n\nAbstract\nSymbolic knowledge representation and reasoning (K R&R) is a key aspect of human intelligence. Among other things\, it enable s scientists to explore new theories\, declaratively describe them\, and s hare them with colleagues. In the natural sciences\, abstract theories oft en arise from observations and experiments\; in other fields\, such as met aphysics\, they may result from pure thought experiments\, possibly withou t data from which to start (and learn from). Strong AI without explicit s ymbolic KR&R capabilities thus seems unthinkable. But how can the explorat ion of abstract theories\, especially fundamental theories of metaphysics and mathematics\, including logical formalisms\, be fruitfully supported o n computers? \n\nIn this talk\, I review recent contributions in which a l ogico-pluralistic KR&R methodology and infrastructure\, called LogiKEy\, h as been successfully applied to the exploration and assessment of foundati onal theories in metaphysics and mathematics. One such exploratory study o n the axiomatic foundations of category theory\, conducted jointly with Da na Scott and students at FU Berlin\, will be described in some more detail . Since LogiKEy also supports exploration and assessment of ethical and le gal theories\, it also has applications in the areas of trusted AI and AI& Law.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/56/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrej Bauer DTSTART:20220512T170000Z DTEND:20220512T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/57 DESCRIPTION:Title: The countable reals\nby Andrej Bauer as part of Topo s Institute Colloquium\n\n\nAbstract\nJoint work with James E. Hanson from the University of Maryland\, https://james-hanson.github.io.\n\nIn 1874 G eorg Cantor published a theorem stating that every sequence of reals is av oided by some real\, thereby showing that the reals are not countable. Can tor's proof uses classical logic. There are constructive proofs\, although they all rely on the axiom of countable choice. Can the real numbers be s hown uncountable without excluded middle and without the axiom of choice? An answer has not been found so far\, although not for lack of trying.\n\n We show that there is a topos in which the real numbers are countable\, i. e.\, there is an epimorphism from the object of natural numbers to the obj ect of Dedekind reals. Therefore\, higher-order intuitionistic logic canno t show the reals to be uncountable.\n\nThe starting point of our construct ion is a sequence of reals\, shown to exist by Joseph S. Miller from Unive rsity of Wisconsin–Madison\, with a strong counter-diagonalization prope rty: if an oracle Turing machine computes a specific real number\, when gi ven any oracle representing Miller's sequence\, then the number appears in the sequence. One gets the idea that the reals ought to be countable in a realizability topos built from Turing machines with oracles for Miller's sequence. However\, we cannot just use ordinary realizability\, because al l realizability toposes validate countable choice and consequently the unc ountability of the reals.\n\nTo obtain a topos with countable reals\, we d efine a variant of realizability which we call parameterized realizability . First we define parameterized partial combinatory algebras (ppca)\, whic h are partial combinatory algebras whose evaluation depends on a parameter . We then define parameterized realizability toposes. In these realizers w itness logical statements uniformly in the parameters. The motivating exam ple is the parameterized realizability topos built from the ppca of oracle Turing machines parameterized by oracles for Miller's sequence. In this t opos\, Miller's sequence is the desired epimorphism from natural numbers t o Dedekind reals.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/57/ END:VEVENT BEGIN:VEVENT SUMMARY:John Terilla DTSTART:20220505T170000Z DTEND:20220505T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/58 DESCRIPTION:Title: Rethinking language\nby John Terilla as part of Topo s Institute Colloquium\n\n\nAbstract\nLanguage is essential to being human . Without it\, no aspect of modern life could exist. But what is languag e exactly? How precisely does meaning emerge from sequences constructed f rom a small collection of basic symbols or sounds? Biologists\, linguists \, and philosophers have been debating this question---still unanswered--- for thousands of years. \n\nNow\, at a pivotal moment when intelligent ma chines are beginning to acquire human language skills\, new insights into the nature of language are emerging. Some old beliefs about language can probably be cast aside and achievements in artificial intelligence are in spiring some new ways of thinking of language.\n\nI will present an argume nt for rethinking language and give a tour of some relevant mathematical i deas. The talk will be prepared keeping in mind the four themes of the To pos Institute Colloquium: ethics and societal impact of mathematics\, app lied category theory\, foundation models\, and technology and tools.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/58/ END:VEVENT BEGIN:VEVENT SUMMARY:Eduardo Dubuc DTSTART:20220915T170000Z DTEND:20220915T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/59 DESCRIPTION:Title: On localizations via homotopies\nby Eduardo Dubuc as part of Topos Institute Colloquium\n\n\nAbstract\n(joint work with J. Gil abert based on work by Descotte-Dubuc-Szyld).\n\nLet $\\mathcal{C}$ be a c ategory and $\\Sigma$ be a class of morphisms. The localization of \n$\\ma thcal{C}$ at $\\Sigma$ is a category $\\mathcal{C}[\\Sigma^{-1}]$ together with a functor $q: \\mathcal{C} \\longrightarrow \\mathcal{C}[\\Sigma^{-1 }]$ such that $q(s)$ is an isomorphism for all $s \\in \\Sigma$\, and whic h is initial among such functors. The 2-localization is a 2-category $\\m athcal{C}[\\Sigma^{\\sim 1}]$ together with a functor \n$q: \\mathcal{C} \ \longrightarrow \\mathcal{C}[\\Sigma^{\\sim 1}]$ such that $q(s)$ is a equ ivalence for all $s \\in \\Sigma$\, and which is initial among such functo rs. In this talk I will consider the construction of such localizations by means of cylinders and its corresponding homotopies\, which will determin e the 2-cells of $\\mathcal{C}[\\Sigma^{\\sim 1}]$. I will examine the ca se where $\\Sigma = \\mathcal{W}$ is the class of weak equivalences of a Q uillen's model category\, and in particular the role of the fibrant and co fibrant replacements. I will elaborate about functorial versus non functor ial factorizations in this construction. \nI will recall informally but wi th sufficient precision the necessary definitions so that the non experts can grasp the ideas and follow the proofs.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/59/ END:VEVENT BEGIN:VEVENT SUMMARY:Noam Zeilberger DTSTART:20220630T170000Z DTEND:20220630T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/60 DESCRIPTION:Title: Parsing as a lifting problem and the Chomsky-Schützenbe rger representation theorem\nby Noam Zeilberger as part of Topos Insti tute Colloquium\n\n\nAbstract\nJoint work with Paul-André Melliès.\n\nIn “Functors are Type Refinement Systems” [1]\, we argued for the idea t hat rather than being modelled merely as categories\, type systems should be modelled as functors p : D → T from a category D whose morphisms are typing derivations to a category T whose morphisms are the terms correspon ding to the underlying subjects of those derivations. One advantage of thi s fibrational point of view is that the notion of typing judgment receives a simple mathematical status\, as a triple (R\,f\,S) consisting of two ob jects 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 judgment (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 of deduct ive systems\, beyond type systems in the traditional sense. In this work [ 2]\, we focus on derivability in context-free grammars\, a classic topic i n formal language theory with wide applications in computer science.\n\nTh e talk will begin by explaining how derivations in any context-free gramma r G may be naturally encoded by a functor of operads p : Free S → W[Σ] from a freely generated operad into a certain “operad of spliced words ”. This motivates the introduction of a more general notion of context-f ree grammar over any category C\, defined as a finite species S equipped w ith 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 sta ndard concepts and properties of context-free grammars and languages can b e formulated within this framework\, thereby admitting simpler analysis\, and that parsing may indeed be profitably considered from a fibrational pe rspective\, as a lifting problem along a functor from a freely generated o perad.\n\nThe second half of the talk will be devoted to a new proof of th e Chomsky-Schützenberger Representation Theorem. An important ingredient is the identification of a left adjoint C[−] : Operad → Cat to the ope rad of spliced arrows functor W[−] : Cat → Operad. This construction b uilds the contour category C[O] of any operad O\, whose arrows have a geom etric interpretation as “oriented contours” of operations. A direct co nsequence of the contour / splicing adjunction is that every finite specie s equipped with a color induces a universal context-free grammar\, generat ing a language of tree contour words. Finally\, we prove a generalization of the Chomsky-Schützenberger Representation Theorem\, establishing that any context-free language of arrows over a category C is the functorial im age of the intersection of a C-chromatic tree contour language and a regul ar language.\n\n[1] P.-A. Melliès and N. Zeilberger\, Functors are type r efinement systems\, POPL 2015\n\n[2] P.-A. Melliès and N. Zeilberger\, Pa rsing as a lifting problem and the Chomsky-Schützenberger representation theorem\, to appear at MFPS 2022\, preliminary version available at https: //hal.archives-ouvertes.fr/hal-03702762\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/60/ END:VEVENT BEGIN:VEVENT SUMMARY:Dan Koditschek DTSTART:20221013T170000Z DTEND:20221013T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/61 DESCRIPTION:Title: Working Compositions for Correct Execution of Robot Task Specifications\nby Dan Koditschek as part of Topos Institute Colloqui um\n\n\nAbstract\nA long tradition in robotics has deployed dynamical prim itives as empirical modules of behavior [1]. Physically grounded formaliza tion of these practices offers the prospect of an expressive programming l anguage of work for dynamically dexterous robotics whose programs lead to task and motion planners with associated controllers that are correct by d esign [2]. This talk will offer a brief progress report on a bottom-up rob otics research agenda seeking to formalize the use of Lagrangian energy la ndscapes as “letters” whose hierarchical [3]\, parallel [4] and sequen tial [5] compositions yield “words” of hybrid dynamical systems with g uaranteed behavioral properties. Attention then shifts to an emerging arch itecture for top-down task and motion planning [6] that offers the promis e of abstract\, semantic\, formal specification [7] for mobile manipulatio n tasks carried out by general purpose robots [8] in learned\, geometrical ly complicated environments [9].\n\nThe talk concludes with a more specula tive appraisal of the prospects for a unified programming environment allo wing the expressive top-down specification of robot behavior with automati c compilation into bottom-up words of work that are correct by design. A r ecent categorical treatment [10] of robot hybrid dynamical systems [11] en codes a well-grounded version of sequential composition [12] and a weak bu t still practicable version of hierarchical composition [3]\, while neglec ting the consideration of cross-talk [4] in its idealization of parallel c omposition as a monoidal product. Subsequent results imbue a slightly rest ricted version of this hybrid dynamical category [10] with a version of Co nley’s fundamental theorem [13] guaranteeing the existence of global Lya punov functions that decompose a suitably formulated relaxation of the hyb rid state space into a covering by attractor basins and their boundaries [ 14]. Thus equipped with generalized energy landscapes\, more physically g rounded refinements of this hybrid dynamical category may yield a practica ble type theory whose associated resource-aware linear logic clauses might be integrated into the more expressive linear temporal logic interface to the task and motion planning architecture of [7]. Such future developmen ts would greatly advance the longer term agenda toward an empirically prac ticable theory of “programming work” [2].\n\n[1] M. H. Raibert\, Legge d Robots That Balance. Cambridge: MIT Press\, 1986.\n\n[2] D. E. Koditsche k\, “What Is Robotics? Why Do We Need It and How Can We Get It?\,” Ann u. Rev. Control Robot. Auton. Syst.\, vol. 4\, no. 1\, pp. 1–33\, May 20 21\, doi: 10.1146/annurev-control-080320-011601.\n\n[3] R. J. Full and D. E. Koditschek\, “Templates and anchors: neuromechanical hypotheses of le gged 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 hybrid dyn amical extension of averaging and its application to the analysis of legge d 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. Burridge\ , A. A. Rizzi\, and D. E. Koditschek\, “Toward a systems theory for the composition of dexterous robot behaviours\,” Robot. Res. Seventh Int. Sy mp. ISRR’95\, pp. 149–161.\n\n[6] V. Vasilopoulos et al.\, “Reactive Semantic Planning in Unexplored Semantic Environments Using Deep Perceptu al Feedback\,” IEEE Robot. Autom. Lett.\, vol. 5\, no. 3\, pp. 4455–44 62\, Jul. 2020\, doi: 10.1109/LRA.2020.3001496.\n\n[7] V. Vasilopoulos\, Y . Kantaros\, G. Pappas\, and D. Koditschek\, “Reactive Planning for Mobi le Manipulation Tasks in Unexplored Semantic Environments\,” IEEE Int. C onf. Robot. Autom. ICRA\, May 2021\, [Online]. Available: https://reposito ry.upenn.edu/ese_papers/880\n\n[8] T. T. Topping\, V. Vasilopoulos\, A. De \, and D. Koditschek E.\, “Composition of Templates for Transitional Ped ipulation Behaviors\,” in Proc. Int. Symp. Rob. Res.\, 2019. [Online]. A vailable: https://repository.upenn.edu/ese_papers/860/\n\n[9] V. Vasilopou los\, G. Pavlakos\, K. Schmeckpeper\, K. Daniilidis\, and D. E. Koditschek \, “Reactive navigation in partially familiar planar environments using semantic perceptual feedback\,” Int. J. Robot. Res.\, vol. 41\, no. 1\, pp. 85–126\, Jan. 2022\, doi: 10.1177/02783649211048931.\n\n[10] J. Culb ertson\, P. Gustafson\, D. E. Koditschek\, and P. F. Stiller\, “Formal c omposition of hybrid systems\,” Theory Appl. Categ.\, vol. 35\, no. 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 se lf-manipulation systems\,” Int. J. Robot. Res.\, vol. 35\, no. 11\, pp. 1354--1392\, Sep. 2016\, doi: 10.1177/0278364916639380.\n\n[12] R. R. Burr idge\, A. A. Rizzi\, and D. E. Koditschek\, “Sequential Composition of D ynamically 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\, and Chaos \, Second. Boca Raton\, FL: CRC Press\, 1999. Accessed: Jan. 29\, 2017. [O nline]. Available: http://imb-biblio.u-bourgogne.fr/Record.htm?record=3252 12414349&idlist=1\n\n[14] M. D. Kvalheim\, P. Gustafson\, and D. E. Kodits chek\, “Conley’s Fundamental Theorem for a Class of Hybrid Systems\, ” SIAM J. Appl. Dyn. Syst.\, pp. 784–825\, Jan. 2021\, doi: 10.1137/20 M1336576.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/61/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrea Censi DTSTART:20220825T170000Z DTEND:20220825T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/62 DESCRIPTION:Title: Categorification of Negative Information\nby Andrea Censi as part of Topos Institute Colloquium\n\n\nAbstract\nI will present some very recent and in-progress work about dealing\nwith “negative info rmation” categorically. This need arises naturally\nin applications. For example\, in motion planning problems\, providing\nan optimal solution is the same as giving a feasible solution (the\n“positive” information) together with a proof of the fact that there\ncannot be feasible solutions better than the one given (the “negative”\ninformation). We model neg ative information by introducing the concept\nof “norphisms”\, as oppo sed to the positive information of morphisms. A\n“nategory” is a categ ory that has “Nom”-sets in addition to hom-sets\,\nand specifies the c ompatibility rules between norphisms and morphisms.\nWith this setup we ca n choose to work in “coherent” “subnategories”:\nsubcategories tha t describe a potential instantiation of the world in\nwhich all morphisms and norphisms are compatible. We derive the\ncomposition rules for norphis ms in a coherent subnategory\; we show\nthat norphisms do not compose by t hemselves\, but rather they need to\nuse morphisms as catalysts. We have t wo distinct rules of the type\nmorphism + norphism → norphism. We then s how that those complex rules\nfor norphism inference are actually as natur al as the ones for\nmorphisms\, from the perspective of enriched category theory.\n\nThis is joint work with Dr. Jonathan Lorand and Ph.D. student G ioele Zardini.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/62/ END:VEVENT BEGIN:VEVENT SUMMARY:Angeliki Koutsoukou Argyraki DTSTART:20221006T170000Z DTEND:20221006T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/63 DESCRIPTION:Title: The new era of formalised mathematics and the ALEXANDRIA Project\nby Angeliki Koutsoukou Argyraki as part of Topos Institute C olloquium\n\n\nAbstract\nThe formalisation of mathematics with proof assis tants has recently seen a \nconsiderable increase in activity\, with fast- expanding\, flourishing communities attracting computer scientists\, mathe maticians and students. I will discuss the philosophy and motivation behin d the use of modern proof assistants to formalise mathematics\, referring to the state of the art and potential of the area and to recent developmen ts involving the formalisation of advanced\, research-level mathematics. I will share my experiences from my participation in the ERC project "ALEXA NDRIA: Large-Scale Formal Proof for the Working Mathematician" (https://ww w.cl.cam.ac.uk/~lp15/Grants/Alexandria/) at the University of Cambridge le d 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://researchseminars.org/talk/ToposInstituteColloquium/63/ END:VEVENT BEGIN:VEVENT SUMMARY:Richard Zanibbi DTSTART:20221027T160000Z DTEND:20221027T170000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/65 DESCRIPTION:Title: Mathematical Information Retrieval: Searching with Formu las and Text\nby Richard Zanibbi as part of Topos Institute Colloquium \n\n\nAbstract\nMathematical information is essential for technical work\, but its creation\, interpretation\, and search are challenging. In the ho pes of helping users locate mathematical information more easily\, multimo dal retrieval models and search interfaces that support both formulas and text have been developed.\n\nIn this talk we will start by discussing some differences between the information needs and search behaviors of mathema tical experts vs. non-experts. We will then examine techniques used for re trieving math formulas\, and math-aware search engines that support querie s containing both formulas and text. Finally\, we will consider future res earch directions for math-aware search\, including tasks involving Natural Language Processing (NLP) for mathematical texts.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/65/ END:VEVENT BEGIN:VEVENT SUMMARY:David Jaz Myers DTSTART:20220908T170000Z DTEND:20220908T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/66 DESCRIPTION:Title: A synthetic approach to orbifolds\nby David Jaz Myer s as part of Topos Institute Colloquium\n\n\nAbstract\nOrbifolds are smoot h spaces where the points may have finitely many internal symmetries. Thes e spaces often arise as quotients of manifolds by the actions of discrete groups --- that is\, in situations with discrete symmetries\, such as in c rystallography. \n\nFormally\, the notion of orbifold has been presented i n a number of different guises -- from Satake's V-manifolds to Moerdijk an d Pronk's proper étale groupoids -- which do not on their face resemble t he informal definition. The reason for this divergence between formalism a nd intuition is that the points of spaces cannot have internal symmetries in traditional\, set-level foundations. In this talk\, we will see a forma l definition which closely tracks the informal idea of an orbifold.\n\nBy working with the axioms of synthetic differential geometry in cohesive hom otopy type theory\, we will give a synthetic definition of orbifold (subsu ming the traditional definitions) which closely resembles the informal def inition: an orbifold is a microlinear type where the type of identificatio ns between any two points is properly finite. In homotopy type theory\, we can construct these orbifolds simply by giving their type of points.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/66/ END:VEVENT BEGIN:VEVENT SUMMARY:Jacques Carette DTSTART:20220922T170000Z DTEND:20220922T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/67 DESCRIPTION:Title: What I learned from formalizing Category Theory in Agda< /a>\nby Jacques Carette as part of Topos Institute Colloquium\n\n\nAbstrac t\nAn interesting side-effect of formalizing mathematics in a theorem prov er is that such efforts frequently leads to learning new details (*) about a known topic. I'll discuss these "little gems" that become much more app arent via formalization. While the focus will be mostly on items learned t hrough formalizing Category Theory\, a few nuggets from other domains (Uni versal Algebra\, and the theory of programming languages) will also be thr own in.\n\n(*) These details are frequently known to select experts\, but rarely ever recorded in print.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/67/ END:VEVENT BEGIN:VEVENT SUMMARY:Chad Scherrer DTSTART:20220901T170000Z DTEND:20220901T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/68 DESCRIPTION:Title: Applied Measure Theory for Composable Statistical Modeli ng\nby Chad Scherrer as part of Topos Institute Colloquium\n\n\nAbstra ct\nStatistics is often framed in terms of probability distributions. Dist ributions are special cases of measures\; we find that working in these mo re general terms leads more naturally to a composable system. For example\ , a univariate probability density function is defined relative to Lebesgu e measure. Bayesian inference often leaves us with an unnormalized posteri or\, 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 measure that cannot be described in terms of other measures)\, and a rich set of combi nators for building new measures from existing ones. This approach gives g ood performance and makes it easy to describe measures and related structu res (kernels\, likelihoods\, etc) that are awkward or impossible to expres s in other systems.\n\nAfter introducing some fundamental concepts relevan t to the field of measure theory\, this talk will give an overview of the MeasureTheory.jl library\, finally closing with a brief introduction to Ti lde.jl\, a probabilistic programming language that specifically targets Me asureTheory.jl.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/68/ END:VEVENT BEGIN:VEVENT SUMMARY:Josef Urban DTSTART:20220707T170000Z DTEND:20220707T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/69 DESCRIPTION:Title: Combining learning and deduction over formal math corpor a\nby Josef Urban as part of Topos Institute Colloquium\n\n\nAbstract\ nThe talk will give a brief overview of recent methods that combine learni ng and deduction over large formal libraries. I will mention the "hammer" linkups between ITPs and ATPs\, systems that learn and perform direct tac tical guidance of ITPs\, discuss learning of premise selection over large libraries\, and learning-based guidance of saturation-style and tableau-st yle automated theorem provers (ATPs) trained over the large proof corpora. I will also mention feedback loops between proving and learning in this s etting\, and show some autoformalization and conjecturing experiments.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/69/ END:VEVENT BEGIN:VEVENT SUMMARY:Johan Commelin DTSTART:20220929T170000Z DTEND:20220929T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/70 DESCRIPTION:Title: Breaking the one-mind-barrier in mathematics using forma l verification\nby Johan Commelin as part of Topos Institute Colloquiu m\n\n\nAbstract\nIn this talk I will argue that formal verification helps break the\none-mind-barrier in mathematics. Indeed\, formal verification a llows a\nteam of mathematicians to collaborate on a project\, without 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 work on a\ ndifferent component of a project. It thus also expands the\none-mind-barr ier by reducing cognitive load.\n\nI will use the Liquid Tensor Experiment as an example\, to illustrate\nthe above two points. This project recentl y finished the formalization\nof the main theorem of liquid vector spaces\ , following up on a\nchallenge by Peter Scholze.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/70/ END:VEVENT BEGIN:VEVENT SUMMARY:Gilles Dowek DTSTART:20221110T170000Z DTEND:20221110T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/72 DESCRIPTION:Title: From the Universality of Mathematical Truth to the Inter operability of Proof Systems\nby Gilles Dowek as part of Topos Institu te 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 truth\, eac h proof system defining its own language for mathematical statements and i ts own truth conditions for these statements. One way to address this iss ue is to view the formalisms implemented in these systems as theories expr essed 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 theory with polymorphism\, Simple type theory with predicate subtyping\, the Calculus of constructions... can be expressed in Dedukti. Proofs developed with pr oof processing systems then can be expressed in these theories\, independe ntly of the system they have been developed with\, and used in any system that supports the axioms they use.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/72/ END:VEVENT BEGIN:VEVENT SUMMARY:Pawel Sobocinski DTSTART:20221201T170000Z DTEND:20221201T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/74 DESCRIPTION:Title: Electrical circuits with string diagrams\nby Pawel S obocinski as part of Topos Institute Colloquium\n\n\nAbstract\nOne of the goals of applied category theory is to develop new mathematics for reasoni ng about open systems of various kinds. In this talk\, I will introduce a string diagrammatic methodology for reasoning about and manipulating non-p assive electrical circuits\, which are a classical and well-known example of open system. This joint work with Guillaume Boisseau is\, on the one ha nd\, a rigorous\, compositional\, sound and complete equational calculus\, while on the other hand\, it retains elements of the intuitive\, classica l diagrammatic syntax for circuits. It is based on previous work on Affine Graphical Algebra\, joint work with Bonchi\, Piedeleu and Zanasi which I will first introduce.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/74/ END:VEVENT BEGIN:VEVENT SUMMARY:Robin Cockett DTSTART:20221020T170000Z DTEND:20221020T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/75 DESCRIPTION:Title: Turing categories\nby Robin Cockett as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk is based on the following p apers/notes:\n\n(1) "Introduction to Turing categories" with Pieter Hofstr a\n\n(2) "Timed set\, functional complexity\, and computability" with Boil s\, Gallagher\, Hrubes\n\n(3) "Total maps of Turing categories" with Piete r Hofstra and Pavel Hrubes\n\n(4) "Estonia notes" on my website\n\nTuring categories are the theory of "abstract computability". Their development followed my meeting Pieter Hofstra. He was in Ottawa at the time and he s ubsequently joined me as a postdoc. The core theory was developed in Calg ary before he returned to Ottawa as a faculty member. Tragically he died earlier this year when there was still so much to do and\, indeed\, that h e had done\, but had not published.\n\nTuring categories are important bec ause they characterize computability in a minimal traditional context. Th ese ideas are not original to Pieter and I: De Paola\, Heller\, Longo\, Mo ggi\, 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 step fur ther on a road which still stretches ahead. \n\nSo\, the purpose of the t alk is to try and explain what all this was about ... and what we were str iving to accomplish. To do this I have to introduce restriction categorie s and Turing categories in that context. Then I will describe a family of models which are fundamental to computer science. Finally\, I will take a quick look along the road at some open issues.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/75/ END:VEVENT BEGIN:VEVENT SUMMARY:Bryce Clarke DTSTART:20221103T170000Z DTEND:20221103T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/76 DESCRIPTION:Title: A double-categorical approach to lenses via algebraic we ak factorisation systems\nby Bryce Clarke as part of Topos Institute C olloquium\n\n\nAbstract\nThe goal of this talk is to draw a common thread between three concepts: double categories\, lenses\, and algebraic weak fa ctorisation systems (AWFS). A double category is a 2-dimensional categoric al structure consisting of objects\, horizontal and vertical morphisms\, a nd cells between them. In applied category theory\, lenses are a kind of m orphism which consist of a forwards component and a backwards component. A n AWFS on a category C consists of a compatible comonad L and monad R on t he arrow category of C\, such that each morphism factors into an L-coalgeb ra followed by an R-algebra. In each case\, two classes of morphisms play a central role — horizontal and vertical\, forwards and backwards\, coal gebras and algebras — and it is natural to wonder if there is a deeper r elationship between these three concepts. \n\nIn this talk\, I will develo p a double-categorical approach to lenses via AWFS. The approach builds up on the work of Bourke and Garner\, which characterises AWFS as certain kin ds of double categories\, and the work of Johnson\, Rosebrugh\, and Wood\, which implicitly characterises lenses as members of the right class of an AWFS. Combining these results leads indirectly to a double-categorical ap proach to lenses. However\, there is also a direct approach which construc ts a generalised notion of lens inside any double category\, using a proce ss called the "right-connected completion". I will compare these two appro aches\, and explore settings where they coincide.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/76/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrei Rodin DTSTART:20221215T170000Z DTEND:20221215T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/77 DESCRIPTION:Title: Univalent Foundations and Applied Mathematics\nby An drei Rodin as part of Topos Institute Colloquium\n\n\nAbstract\nIn a serie s of lectures given in 2003 Vladimir Voevodsky identified two strategic go als for his further mathematical research. The goal number one was to deve lop a "computerised library of mathematical knowledge". This line of resea rch eventually led Voevodsky to the idea of Univalent Foundations and its implementation with the UniMath library. The goal number two was to "brid ge pure and applied mathematics". Voevodsky's research towards the second goal did not bring published results but in an interview given in 2012 he expressed his intention to return to this project in the future and explai ned a possible role of Univalent Foundations in it. \n\nIn this talk based on archival sources I reconstruct Voevodsky’s original strategy of brid ging pure and applied mathematics\, illustrate it with some examples\, and argue that Applied Univalent Foundations is a viable research program. \n \n[1] Andrei Rodin\, Voevodsky’s Unfinished Project: Bridging the Gap be tween Pure and Applied Mathematics\, BioSystems\, 204 (2021)\, 104391\; pr eprint arXiv : 2012.01150\n\n[2] UniMath Library : https://github.com/UniM ath/UniMath\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/77/ END:VEVENT BEGIN:VEVENT SUMMARY:Alexandre Miquel DTSTART:20221208T170000Z DTEND:20221208T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/78 DESCRIPTION:Title: Implicative algebras: a new foundation for realizability and forcing\nby Alexandre Miquel as part of Topos Institute Colloquiu m\n\n\nAbstract\nIn this talk\, I will present implicative algebras\, a si mple algebraic\nstructure generalizing complete Heyting algebras and abstr act Krivine\nstructures\, and based on a surprising identification between the\nnotions of a realizer and of a type. I will show that this structur e\nnaturally induces a family of triposes - the implicative triposes -\nth at encompass all triposes known so far\, namely: Heyting triposes\,\nBoole an triposes\, intuitionistic realizability triposes and classical\nrealiza bility triposes\, thus providing a unified framework for\nexpressing forci ng and realizability\, both in intuitionistic and\nclassical logic. Finall y\, I will discuss about some recent\ncompleteness results about the very notion of implicative model\, both\nin higher-order logic and first-order logic.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/78/ END:VEVENT BEGIN:VEVENT SUMMARY:Paige North DTSTART:20230202T170000Z DTEND:20230202T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/79 DESCRIPTION:Title: Fuzzy type theory\nby Paige North as part of Topos I nstitute Colloquium\n\n\nAbstract\nIn this talk\, I will report on progres s developing a fuzzy type theory\, a project that started as part of the A CT 2022 Adjoint School. The motivation is to develop a logic which can mod el opinions\, and we do this by generalizing Martin-Löf type theory. Mart in-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 interpret such a term as saying that the proposition holds. Fuzzy type theory is a simila r system in which one can provide or construct evidence (aka a fuzzy 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\, which expr esses to what extent the opinion holds. Martin-Löf type theory is closely related to category theory: from such a type system one can construct a c ategory in which (very roughly) the types become objects and the terms bec ome morphisms\, and this can be made part of an equivalence. Thus\, we bas e our development of fuzzy type theory to be the thing which corresponds t o categories enriched in a category of fuzzy sets in the same way that Mar tin-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://researchseminars.org/talk/ToposInstituteColloquium/79/ END:VEVENT BEGIN:VEVENT SUMMARY:Prakash Panangaden DTSTART:20230209T170000Z DTEND:20230209T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/83 DESCRIPTION:Title: Nuclear ideals in monoidal *-categories\nby Prakash Panangaden as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk is based on 25-year old material developed in joint work with Samson Abram sky\nand Richard Blute. I hope that this talk will stimulate others (any myself) to look at\nthese topics in light on modern developments. Our goa l was to develop quantitative\nanalogues of the concept of binary relation s. In particular\, we were interested in\nfinding a suitable definition o f probabilistic relations.\n\nThe formulation that we came up with arose b y generalizing the notion of nuclear maps from\nfunctional analysis by def ining nuclear ideals in monoidal *-categories. The compact\nclosed struct ure associated with the category of relations does not generalize directly \,\ninstead one obtains nuclear ideals.\n\nMany such categories have a lar ge class of morphisms which behave as if they were part of\na compact clos ed category\, i.e. they allow one to transfer variables between the domain \nand the codomain. We introduce the notion of nuclear ideals to analyze these classes of\nmorphisms. In compact closed categories all morphisms a re nuclear\, and in the category of\nHilbert spaces\, the nuclear morphism s are the Hilbert-Schmidt maps.\n\nWe also introduce two new examples of m onoidal *-categories\, in which integration plays\nthe role of composition . In the first\, morphisms are a special class of distributions\,\nwhich w e call tame distributions. The second example is based on measure and pro bability\nand serves as a possible candidate for probabilistic relations.\ n\nSince our original paper was published\, other examples of this phenome non were discovered.\nWe also explored concepts associated with trace idea ls\, I will briefly talk about these.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/83/ END:VEVENT BEGIN:VEVENT SUMMARY:Sergey Goncharov DTSTART:20230216T170000Z DTEND:20230216T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/84 DESCRIPTION:Title: Towards a Higher-Order Mathematical Operational Semantic s\nby Sergey Goncharov as part of Topos Institute Colloquium\n\n\nAbst ract\nCompositionality proofs in higher-order languages are notoriously in volved\, and general \nsemantic frameworks guaranteeing compositionality a re hard to come by. In particular\, Turi and Plotkin’s \nbialgebraic abs tract GSOS framework\, which has been successfully applied to obtain off-t he-shelf \ncompositionality results for first-order languages\, so far did not apply to higher-order languages. I \nwill present a recently emerged development of the theory of abstract GSOS specifications for \nhigher-ord er languages\, in effect transferring the core principles of Turi and Plot kin’s framework to a \nhigher-order setting. In the present framework\, the operational semantics of higher-order languages is \nrepresented by ce rtain dinatural transformations\, we dub higher-order GSOS laws. I will present a \ngeneral compositionality result w.r.t. the strong variant of Abramsky’s applicative bisimilarity that \napplies to all systems sp ecified in this way. For presentation purposes\, I will stick to a variant of \nthe combinatory logic\, as a main vehicle.\n\nThe talk is based on a recent POPL'23 paper\, which is a joint work with: Stefan Milius\, Lutz S chröder\, \nStelios Tsampas\, and Henning Urbat.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/84/ END:VEVENT BEGIN:VEVENT SUMMARY:Justin Curry DTSTART:20230302T170000Z DTEND:20230302T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/85 DESCRIPTION:Title: Algebraic and Geometric Models for Space Networking\ nby Justin Curry as part of Topos Institute Colloquium\n\n\nAbstract\nIn t his talk I will describe recent and ongoing work dedicated to developing s calable autonomous routing protocols for a future solar system wide intern et. At the heart of the talk will be a description of a new coordinate sys tem (based on cosheaves and persistence) for time-varying graphs. In this new coordinate system\, we can describe distances between various space ne tworking scenarios\, as well as model routing (with propagation delay) usi ng matrix multiplication in a modified coefficient system valued in semi-r ings. To demonstrate these models in practice\, we use simulations of Eart h-Moon-Mars systems generated in SOAP (Satellite Orbital Analysis Program) ranging from 10s to 100s of nodes in size. These simulations are part of a growing codebase being developed by SUNY Albany and NASA Glenn Research Center under the TIMAEUS project.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/85/ END:VEVENT BEGIN:VEVENT SUMMARY:Urs Schreiber DTSTART:20230413T170000Z DTEND:20230413T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/87 DESCRIPTION:Title: Effective Quantum Certification via Linear Homotopy Type s\nby Urs Schreiber as part of Topos Institute Colloquium\n\n\nAbstrac t\nThe intricacies of realistic — namely: of classically controlled and (topologically) error-protected — quantum algorithms arguably make compu ter-assisted verification a practical necessity\; and yet a satisfactory t heory of dependent quantum data types had been missing\, certainly one tha t would be aware of topological error-protection.\n\nTo solve this problem we present Linear homotopy type theory (LHoTT) as a programming and certi fication language for quantum computers with classical control and topolog ically protected quantum gates\, focusing on (1.) its categorical semantic s\, which is a homotopy-theoretic extension of that of Proto-Quipper and a parameterized extension of Abramsky et al.'s quantum protocols\, (2.) its expression of quantum measurement as a computational effect induced from dependent linear type formation and reminiscent of Lee at al.'s dynamic li fting monad but recovering the interacting systems of Coecke et al.'s "cla ssical structures" monads.\n\nNamely\, we have recently shown that classic al dependent type theory in its novel but mature full-blown form of Homoto py Type Theory (HoTT) is naturally a certification language for realistic topological logic gates. But given that categorical semantics of HoTT is f amously provided by parameterized homotopy theory\, we had argued earlier [Sc14] for a quantum enhancement LHoTT of classical HoTT\, now with semant ics in parameterized stable homotopy theory. This linear homotopy type the ory LHoTT has meanwhile been formally described\; here we explain it as th e previously missing certified quantum language with monadic dynamic lifti ng\, as announced in.\n\nConcretely\, we observe that besides its support\ , inherited from HoTT\, for topological logic gates\, LHoTT intrinsically provides a system of monadic computational effects which realize what in a lgebraic topology is known as the ambidextrous form of Grothendieck’s "M otivic Yoga"\; and we show how this naturally serves to code quantum circu its subject to classical control implemented via computational effects. Lo gically this emerges as a linearly-typed quantum version of epistemic moda l logic inside LHoTT\, which besides providing a philosophically satisfact ory formulation of quantum measurement\, makes the language validate the q uantum programming language axioms proposed by Staton\; notably the deferr ed measurement principle is verified by LHoTT.\n\nFinally we indicate the syntax of a domain-specific programming language QS (an abbreviation both for "Quantum Systems" and for "QS^0 -modules" aka spectra) which sugars LH oTT to a practical quantum programming language with all these features\; and we showcase QS-pseudocode for simple forms of key algorithm classes\, 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/show/Quant um+Certification+via+Linear+Homotopy+Types)\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/87/ END:VEVENT BEGIN:VEVENT SUMMARY:David Corfield DTSTART:20230309T170000Z DTEND:20230309T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/88 DESCRIPTION:Title: Philosophical perspectives on category theory\nby Da vid Corfield as part of Topos Institute Colloquium\n\n\nAbstract\nFor the whole length of my academic career\, I have looked to make philosophical s ense of (higher) category theory. My earliest interests concerned category theory as a new structuralist foundational language for mathematics and f or mathematical physics. Later at the n-Category Café there were also att empts to make category-theoretic sense of probability theory\, learning th eory and diagrammatic reasoning. Today\, alongside successes in logic\, ma thematics and physics\, we find a flourishing world of applied category th eory\, involving work in probability theory\, causal reasoning\, learning theory\, natural language processing\, and so on. These are all topics of profound interest to philosophy. In this talk\, I will discuss ways in whi ch philosophy can come into a fruitful relationship with category theory.\ n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/88/ END:VEVENT BEGIN:VEVENT SUMMARY:Christina Vasilakopoulou DTSTART:20230323T170000Z DTEND:20230323T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/89 DESCRIPTION:Title: Dual algebraic structures and enrichment\nby Christi na Vasilakopoulou as part of Topos Institute Colloquium\n\n\nAbstract\nIn this talk\, we will provide a detailed overview of the sometimes called “Sweedler theory” for algebras and modules. This begins by establishin g an enrichment of the category of algebras in the category of coalgebras\ , as well as an enrichment of a global category of modules in a global cat egory of comodules\, giving rise to a structure described as an enriched f ibration. Moreover\, by investigating a many-object generalization involvi ng categories and modules\, we will discuss further directions and applica tions of this framework to operadic structures.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/89/ END:VEVENT BEGIN:VEVENT SUMMARY:Simon Willerton DTSTART:20230330T170000Z DTEND:20230330T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/90 DESCRIPTION:Title: Metric spaces\, entropic spaces and convexity\nby Si mon Willerton as part of Topos Institute Colloquium\n\n\nAbstract\nA certa in notion of convexity of sets can be captured by a monad\, known as a con vexity 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 on categ ories of metric spaces. The work of Fritz-Perrone can be recast in terms o f enriched categories if you consider metric spaces as categories enriched over the quantale of extended non-negative real numbers.\n\nOne can then do a similar thing for any 'suitably convex' quantale R and define a conve xity monad on the category of R-categories. In particular\, if R is the e xtended real line [-oo. oo] with the opposite order to that used in metric spaces\, then R-categories are what Lawvere called 'entropic spaces' and argued gave a necessary structure for state spaces in thermodynamics. 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 thermodynamics wit h the recent approach of Baez-Lynch-Moeller which involves convex spaces a nd concave maps (without the entropic structure).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/90/ END:VEVENT BEGIN:VEVENT SUMMARY:Davide Trotta DTSTART:20230420T170000Z DTEND:20230420T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/91 DESCRIPTION:Title: Generalized existential completions and applications \nby Davide Trotta as part of Topos Institute Colloquium\n\n\nAbstract\nTh is talk presents an overview of the "generalized existential completion" o f Lawvere doctrines and its applications. I present this construction that freely adds (generalized) existential quantifiers to a given doctrine and I will provide an intrinsic characterization of this notion based on an a lgebraic description of the logical concept of existential-free formulas.\ nThis characterization provides a useful tool to recognize a wide variety of examples of doctrines arising as generalized existential completions. T hese include the subobjects doctrine and the weak subobjects doctrine as w ell all realizability triposes and\, among localic triposes\, only the sup ercoherent ones.\n\nI will also present some applications of the construct ion to the dialectica interpretation\, showing how our algebraic descripti on of quantifier-free formulas allows us to prove that the logical princip les involved in the dialectica interpretation are satisfied in the categor ical setting\, establishing a tight correspondence between the logical sys tem and the categorical framework given by dialectica doctrines.\n\nThis t alk is based on the following works:\n\n- Maria Emilia Maietti\, Davide Tr otta (2023). A characterization of generalized existential completions. In Annals of Pure and Applied Logic.\n\n- Davide Trotta\, Matteo Spadetto\, Valeria de Paiva (2023). Dialectica principles via Gödel doctrines. In Th eoretical Computer Science.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/91/ END:VEVENT BEGIN:VEVENT SUMMARY:Georges Gonthier DTSTART:20230427T170000Z DTEND:20230427T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/92 DESCRIPTION:Title: Foothills and cathedrals: organising the libraries behin d big proofs\nby Georges Gonthier as part of Topos Institute Colloquiu m\n\n\nAbstract\nWhile mathematics is amongst the best organized forms of knowledge\, the level of detail of computer-assisted formal mathematics de mands an even higher degree of structuring. The cathedrals that are the co mputer proofs of famous results such as the Four Color or the Odd Order th eorems rest on the foothills of large\, architected libraries of prerequis ites\, ranging from the trivial and elementary to undergraduate and gradua te curricula. While these can often be crafted to resemble traditional cou rse material\, the extra attention to detail also motivates differences\, some examples of which we will highlight.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/92/ END:VEVENT BEGIN:VEVENT SUMMARY:Michael Barany DTSTART:20230504T170000Z DTEND:20230504T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/93 DESCRIPTION:Title: How Categories Come to Matter: On the history and sociol ogy of categories in modern mathematics\nby Michael Barany as part of Topos Institute Colloquium\n\n\nAbstract\nI will situate categories and re lated mathematical principles in the history of modern mathematics from th e late nineteenth century to the present. The worldviews and perspectives adopted by the Topos Institute derive from specific transformations in the nature and scale of mathematical research over the last century-and-a-bit . These connect the ideas of modern mathematics to its people\, institutio ns\, and infrastructures. I will consider two main senses in which categor ies "come to matter": first\, how categories of various kinds became meani ngful\, salient\, and important as ways of seeing the mathematical world a nd and the worlds of mathematicians\; and second\, how such categories wer e encoded\, translated\, reproduced\, and made to move on and across vario us kinds of material media (i.e. physical matter) such as blackboards\, in dex cards\, and printed journals. I contend that these two senses are hist orically connected\, in ways that relate to the continuing goals and chall enges of the Topos community.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/93/ END:VEVENT BEGIN:VEVENT SUMMARY:Riehl\, Bradley\, Cheng\, Dancstep\, and Lugg DTSTART:20230316T170000Z DTEND:20230316T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/94 DESCRIPTION:Title: Category theory outreach panel\nby Riehl\, Bradley\, Cheng\, Dancstep\, and Lugg as part of Topos Institute Colloquium\n\n\nAb stract\nCategory theory is a wonderful subject\, deep and broad\, spanning the breadth of mathematics and having applications throughout science\, e ngineering\, technology\, and the arts. But for people outside of academia \, it can be a difficult subject to learn. Topos Institute is hosting a pa nel discussion\, moderated by Emily Riehl\, featuring panelists who are ac tively involved in producing category theory books and videos for a non-ex pert audience. The panellists will discuss their philosophy and techniques \, and provide support and encouragement for others to join in this import ant 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 help categ ory theorists understand what they can do to facilitate this process.\n\nF or more information\, including how to submit questions\, please see https ://topos.site/ct-outreach-self-learners/\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/94/ END:VEVENT BEGIN:VEVENT SUMMARY:Chad Giusti DTSTART:20230511T170000Z DTEND:20230511T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/95 DESCRIPTION:Title: Toward a useful category for persistent homology\nby Chad Giusti as part of Topos Institute Colloquium\n\n\nAbstract\nPersiste nt homology is the central tool in modern applied topology. Briefly\, give n a (finite) sample from a distribution on a topological space embedded in a metric space\, one builds a multi-scale combinatorial representation of the sample called a filtered Vietoris-Rips complex. Applying homology\, w e summarize this multi-scale structure as an object called a persistence m odule. When the samples come from real-world data\, practitioners apply do main knowledge and ad hoc reasoning to understand how the persistence modu le reflects organizational principles of the system of interest.\n\nIf we wish to formalize this reasoning process\, or apply more sophisticated met hods from algebraic topology to data analysis\, a first step is to develop a notion of functoriality for persistent homology. This pipeline inherits the usual functoriality of homology\, taking maps of simplicial complexes to maps on persistence modules\, and substantial progress has been made i n cycle registration\, a formalism for comparing persistence modules using this structure. However\, in practice one usually compares samples from u nknown spaces\; there are relatively few settings where the required map o f the combinatorial encodings (or underlying spaces) is likely to be known . In this talk\, we describe our recent efforts to develop techniques that provide a notion of "induced map" using the kind of data reasonably avail able in applied settings\, and the challenges that remain in developing a full categorical framework for applied topology. Various parts of this wor k are joint with Iris Yoon\, Robert Ghrist\, Niko Schonsheck\, Gregory Hen selman-Petrusek\, and Lori Ziegelmeier\, amongst others.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/95/ END:VEVENT BEGIN:VEVENT SUMMARY:Elaine Landry DTSTART:20230525T170000Z DTEND:20230525T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/96 DESCRIPTION:Title: As If Category Theory were a Foundation\nby Elaine L andry 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 philosophical p roblems to solving mathematical ones\, we see that an as-if interpretation of mathematics can be used to provide an account of both the practice and the applicability of mathematics. I begin first with Plato to show that m uch philosophical milk has been spilt owing to our conflating the method o f mathematics with the method of philosophy. I then use my reading of Plat o to develop what I call as-ifism\, the view that\, in mathematics\, we tr eat our hypotheses as if they were true first principles and we do this wi th the purpose of solving mathematical problems not philosophical ones. I next extend as-ifism to modern mathematics wherein the method of mathemati cs becomes the axiomatic method\, noting that this engenders a shift from as-if hypotheses to as-if axioms. I next distinguish as-ifism from if-then ism\, and use this to develop my structural as-ifist position. I end by sh owing that taking a methodological as-ifist route\, by placing our focus o n what is needed for the practice and applicability of mathematics\, we ar e neither committed to the unconditional consistency of our mathematical a xioms nor the unconditional truth of our background meta-mathematical theo ry. Simply\, it is methodological considerations\, and not metaphysical on es\, that “condition” our as if assumptions of both the consistency of our mathematical axioms and the truth of our background meta-mathematical theory. Finally\, I use my methodological as-ifism to reconsider the “f oundations debate”\, specifically\, that between set theory and category theory.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/96/ END:VEVENT BEGIN:VEVENT SUMMARY:Tom Hirschowitz DTSTART:20230608T170000Z DTEND:20230608T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/97 DESCRIPTION:Title: Abstraction in programming language theory: Howe's metho d\nby Tom Hirschowitz as part of Topos Institute Colloquium\n\n\nAbstr act\nResearch in programming languages mostly proceeds language by\nlangua ge. This in particular means that key ideas are often introduced\nfor one typical language\, and must then be adapted to other languages.\n\nA promi nent example of this is Howe's method for proving that\napplicative bisimi larity\, a notion of program equivalence in\ncall-by-name λ-calculus\, is a congruence. This method has been adapted\nto call-by-value λ-calculus\ , PCF\, λ-calculus with delimited\ncontinuations\, higher-order π-calcul us\,…\n\nIn this work\, using category theory\, we establish an abstract congruence\ntheorem for applicative bisimilarity\, of which most existing adaptations\nof Howe's method are instances.\n\nThis is joint work with A mbroise Lafont.\n\nSee also Ugo Dal Lago\, Francesco Gavazzo\, and Paul Le vy. Effectful applicative bisimilarity: Monads\, relators\, and Howe’s m ethod. LICS 2017. Extended version: https://arxiv.org/abs/1704.04647 .\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/97/ END:VEVENT BEGIN:VEVENT SUMMARY:Taco Cohen DTSTART:20230615T170000Z DTEND:20230615T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/98 DESCRIPTION:Title: Categorical Causality & Systems Theory\nby Taco Cohe n as part of Topos Institute Colloquium\n\n\nAbstract\nCategorical Systems theory is a general framework for modelling systems whose state evolves d epending on some inputs or actions\, and which produce some observable out puts. This framework is general enough to describe arbitrary classical phy sical systems\, and generalizes the Partially Observed Markov Decision Pro cess commonly used in AI. Causal models\, formalized as string diagrams in CD-categories\, provide a convenient high-level framework for reasoning a bout how intervening on some outcome variables would affect others. In thi s talk I will provide a high-level introduction to both frameworks\, and d iscuss their relations. In particular we ask when a system can be accurate ly described by a causal model\, and show that this is not generally possi ble\, thus highlighting the limitations of existing causal modelling frame works.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/98/ END:VEVENT BEGIN:VEVENT SUMMARY:Clark Barrett DTSTART:20230518T170000Z DTEND:20230518T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/99 DESCRIPTION:Title: Proof Certificates in Satisfiability Modulo Theories \nby Clark Barrett as part of Topos Institute Colloquium\n\n\nAbstract\nSa tisfiability modulo theories (SMT) is an automated reasoning paradigm that can automatically prove a wide variety of first-order logic theorems rela ting to theories that commonly occur when reasoning about computer systems (e.g.\, arithmetic\, arrays\, strings\, etc.). Together with my colleagu es at U Iowa\, Bar-Ilan\, and UF Minas Gerais\, we have for the past few y ears been developing a way to produce proof certificates from the cvc5 SMT solver. These proof certificates provide enough detail to allow an indep endent proof checker to confirm the correctness of the theorem proved. Th e obvious benefit is that this drastically reduces the code that must be t rusted to ensure correct results. A less obvious benefit is that proof ce rtificates open up the possibility of integrating SMT solvers into skeptic al proof assistants such as Coq\, Isabelle/HOL\, or Lean. In this talk\, I will give an overview of the proof production and proof checking mechani sms we are developing for cvc5 and explain how we are leveraging these to provide trusted SMT automation in proof assistants.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/99/ END:VEVENT BEGIN:VEVENT SUMMARY:Alex Martsinkovsky DTSTART:20230601T170000Z DTEND:20230601T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/100 DESCRIPTION:Title: How to interpret cotorsion\nby Alex Martsinkovsky a s part of Topos Institute Colloquium\n\n\nAbstract\nTwo important features of a linear control system are its controllability and observability. \nF rom the algebraic prospective\, a system is a module over a ring of differ ential operators (with constant\, polynomial\, or analytic coefficients). The part of the system that cannot be controlled \nis called the autonomy of the system. In the algebraic language\, this is just the torsion submo dule \nof the module. Thus the controllable part is described by the torsi on-free quotient of the module. \n\nThere is a duality between the control lability of the system and the observability of the dual \nsystem. The goa l of this talk is to propose a conjectural algebraic analog of the observa bility\, \ncalled cotorsion. As a justification for the conjecture\, we wi ll see a duality between cotorsion \nand torsion\, effected by the Ausland er-Gruson-Jensen functor. The latter seems to be a \nrecurring theme\, fou nd in a variety of functor categories. It is to be hoped that\, despite th e \nalgebraic nature of this talk\, the non-algebraic members of the audie nce would recognize \nfamiliar (enriched) categorical patterns.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/100/ END:VEVENT BEGIN:VEVENT SUMMARY:Jared Culbertson DTSTART:20230622T170000Z DTEND:20230622T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/101 DESCRIPTION:Title: Applying Categorical Thinking to Practical Domains\ nby Jared Culbertson as part of Topos Institute Colloquium\n\n\nAbstract\n Embracing a categorical perspective has proven to be a useful way to forma lize many intuitive and ad hoc compositional approaches across a diverse s et of practical fields. In this talk\, we will discuss work in three prima ry domains including probabilistic modeling\, hierarchical clustering\, an d robotics. After briefly surveying prior work in the first two\, we will focus on formalizing what it means to "apply a behavior" in a very concret e context of legged robots whose controllers are modeled as hybrid dynamic al systems. Central to this approach is developing a common framework for describing (i) sequential composition of hybrid systems (enabled by a cosp an description of interfaces and a generalization of Conley's (epsilon\,T) -chains to the hybrid setting)\; (ii) transformations of hybrid systems (m odeled as hybrid semiconjugacies and integrated with sequential compositio n via a double category)\; and (iii) hierarchical composition of hybrid sy stems (where hybrid subdivisions satisfying a certain fiber product condit ion enable composing spans of template/anchor pairs). Throughout\, we will highlight some specific practical lessons that were learned in applying c ategorical formalisms to these real-world problem domains.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/101/ END:VEVENT BEGIN:VEVENT SUMMARY:Nathaniel Osgood DTSTART:20230629T170000Z DTEND:20230629T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/103 DESCRIPTION:Title: Towards Compositional System Dynamics for Public Health \nby Nathaniel Osgood as part of Topos Institute Colloquium\n\n\nAbstr act\nFor decades\, System Dynamics (SD) modeling has served as a prominent \, diagram-centric methodology used for public health modeling. Much of it s strength arises from its versatile use of 3 types of diagrams\, with eac h serving both to elevate transparency across the interdisciplinary teams responsible for most impactful models\, and to reason about patterns of sy stem behavior. Causal loop diagrams (CLDs) are used in semi-qualitative pr ocesses early in the modeling process and seek to support insight into fee dback structure\, behavioral modes\, and leverage points. As modeling pro ceeds\, system structure diagrams further distinguish stocks (accumulation s) from flows and material from informational dependencies. Stock & flow d iagrams build on that representation to characterize mathematical dependen cies\, quantify parameters and initial values for stocks\, and have been p articularly widely used in scenario simulation in public health and mathem atical epidemiology. While ubiquitous use of diagrams renders SD modeling markedly effective in supporting team science and shaping stakeholders’ mental models\, existing tools suffer from a number of shortcomings. The se include poor support for modularity\, cumbersome and obscurant model st ratification\, and an inability to capture the relationships between the 3 diagram types. Within this talk\, we describe initial progress towards cr eating a framework for compositional System Dynamics\, including theory\, API support via StockFlow.jl within AlgebraicJulia\, and ModelCollab -- a real-time collaborative tool to support interdisciplinary teams in modular ly building\, composing and flexibly analyzing Stock & Flow diagrams. Our approach separates syntax from semantics\, and characterizes diagrams usin g copresheaves with a schema category. Diagram composition draws on the th eory of structured cospans and undirected wiring diagrams\, and employs pu llbacks for model stratification. Model interpretation is achieved via fun ctorial semantics\, with ordinary differential equations being just one of several semantic domains supported. After describing the current state of implementation\, we describe plans for future work\, including enriching support for CLDs\, and adding support for several computational statistics algorithms and additional types of structurally-informed model analyses. This is joint work with John Baez\, Evan Patterson\, Nicholas Meadows\, S ophie Libkind\, Alex Alegre and Eric Redekopp.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/103/ END:VEVENT BEGIN:VEVENT SUMMARY:Urs Schreiber DTSTART:20230824T170000Z DTEND:20230824T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/104 DESCRIPTION:Title: Quantum Programming via Linear Homotopy Types\nby U rs Schreiber as part of Topos Institute Colloquium\n\n\nAbstract\nThe intr icacies of realistic — namely: of classically controlled and\n(topologic ally) error-protected — quantum algorithms arguably make\ncomputer-assis ted verification a practical necessity\; and yet a\nsatisfactory theory of dependent quantum data types had been missing\,\ncertainly one that would be aware of topological error-protection.\n\nTo solve this problem we pre sent Linear homotopy type theory (LHoTT)\nas a programming and certificati on language for quantum computers with\nclassical control and topologicall y protected quantum gates\, focusing\non (1.) its categorical semantics\, which is a homotopy-theoretic\nextension of that of Proto-Quipper and a pa rameterized extension of\nAbramsky et al.'s quantum protocols\, (2.) its e xpression of quantum\nmeasurement as a computational effect induced from d ependent linear\ntype formation and reminiscent of Lee at al.‘s dynamic lifting monad\nbut recovering the interacting systems of Coecke et al.‘s "classical\nstructures" monads.\n\nNamely\, we have recently shown that c lassical dependent type theory in\nits novel but mature full-blown form of Homotopy Type Theory (HoTT) is\nnaturally a certification language for re alistic topological logic\ngates. But given that categorical semantics of HoTT is famously\nprovided by parameterized homotopy theory\, we had argue d earlier\n[Sc14] for a quantum enhancement LHoTT of classical HoTT\, now with\nsemantics in parameterized stable homotopy theory. This linear\nhomo topy type theory LHoTT has meanwhile been formally described\; here\nwe ex plain it as the previously missing certified quantum language\nwith monadi c dynamic lifting\, as announced in.\n\nConcretely\, we observe that besid es its support\, inherited from HoTT\,\nfor topological logic gates\, LHoT T intrinsically provides a system of\nmonadic computational effects which realize what in algebraic topology\nis known as the ambidextrous form of G rothendieck’s “Motivic Yoga”\;\nand we show how this naturally serve s to code quantum circuits subject\nto classical control implemented via c omputational effects. Logically\nthis emerges as a linearly-typed quantum version of epistemic modal\nlogic inside LHoTT\, which besides providing a philosophically\nsatisfactory formulation of quantum measurement\, makes the language\nvalidate the quantum programming language axioms proposed by Staton\;\nnotably the deferred measurement principle is verified by LHoTT .\n\nFinally we indicate the syntax of a domain-specific programming\nlang uage QS (an abbreviation both for “Quantum Systems” and for “QS^0\n- modules” aka spectra) which sugars LHoTT to a practical quantum\nprogram ming language with all these features\; and we showcase\nQS-pseudocode for simple forms of key algorithm classes\, such as\nquantum teleportation\, 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 will be av ailable at:\nncatlab.org/schreiber/show/Quantum+Certification+via+Linear+H omotopy+Types)\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/104/ END:VEVENT BEGIN:VEVENT SUMMARY:Jonathan Sterling DTSTART:20230928T170000Z DTEND:20230928T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/105 DESCRIPTION:Title: Synthetic Domains in the 21st Century\nby Jonathan Sterling as part of Topos Institute Colloquium\n\n\nAbstract\nIt is easy t o teach a student how to give a naïve denotational semantics to a typed l ambda calculus without recursion\, and then use it to reason about the equ ational theory: a type might as well be a set\, and a program might as wel l be a function\, and equational adequacy at base type is established usin g a logical relation between the initial model and the category of sets. A dding any non-trivial feature to this language (e.g. general recursion\, p olymorphism\, state\, etc.) immediately increases the difficulty beyond th e facility of a beginner: to add recursion\, one must replace sets and fun ctions with domains and continuous maps\, and to accommodate polymorphism and state\, one must pass to increasingly inaccessible variations on this basic picture.\n\nThe dream of the 1990s was to find a category that behav es like SET in which even general recursive and effectful programming lang uages could be given naïve denotational semantics\, where types are inter preted as “sets” and programs are interpreted as a “functions”\, w ithout needing to check any arduous technical conditions like continuity. The benefit of this synthetic domain theory is not only that it looks “e asy” for beginners\, as more expert-level constructions like powerdomain s or even domain equations for recursively defined semantic worlds become simple and direct. Although there have been starts and stops\, the dream o f synthetic domain theory is alive and well in the 21st Century. Today’s synthetic domain theory is\, however\, both more modular and more powerfu l than ever before\, and has yielded significant results in programming la nguage semantics including simple denotational semantics for an state of t he art programming language with higher-order polymorphism\, dependent typ es\, recursive types\, general reference types\, and first-class module pa ckages that can be stored in the heap.\n\nIn this talk\, I will explain so me important classical results in synthetic domain theory as well as more recent results that illustrate the potential impact of “naïve denotatio nal semantics” on the life of a workaday computer scientist.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/105/ END:VEVENT BEGIN:VEVENT SUMMARY:Nat Shankar DTSTART:20230831T170000Z DTEND:20230831T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/106 DESCRIPTION:Title: Abstraction Engineering with the Prototype Verification System (PVS)\nby Nat Shankar as part of Topos Institute Colloquium\n\ n\nAbstract\nLogic has always played a central role in computing. One suc cessful\napplication of logic is its use in specifying and modeling\ncompu tational behavior\, and in proving properties of computation\nsystems. SR I's PVS was released thirty years ago with the goal of\ndemocratizing inte ractive theorem proving by combining an expressive\nformalism with powerfu l automated reasoning tools for building and\nmaintaining complex formaliz ations and proofs. We describe some of\nthe features of PVS for defining and reasoning with mathematical\nabstractions and bridging the gap between informal and formalized\nmathematical discourse. PVS features an express ive-order logic with\nalgebraic/coalgebraic datatypes\, dependent predicat e subtypes\, and\nparametric theories. The interactive theorem prover emp loys a range\nof automated proof strategies for simplification\, rewriting \, and case\nanalysis\, along with built-in decision procedures for SAT an d SMT\nsolving. The applicative fragment of PVS can be viewed as a\nfunct ional programming language\, and efficient executable code can be\ngenerat ed in Common Lisp and C\, among other languages. PVS includes\nextensive libraries spanning a range of topics in mathematics and\ncomputing. The t alk is an informal overview of the underlying\ntheoretical foundations\, a nd the proof and code generation\ncapabilities of PVS.\n\nBio: Dr. Nataraj an Shankar is a Distinguished Senior Scientist and SRI\nFellow at the SRI Computer Science Laboratory. He received a\nB.Tech. degree in Electrical Engineering from the Indian Institute of\nTechnology\, Madras\, and Ph.D. in Computer Science from the University\nof Texas at Austin. He is the au thor of the book\, "Metamathematics\,\nMachines\, and Godel's Proof"\, pub lished by Cambridge University Press.\nDr. Shankar is the co-developer of a number of technologies including\nthe PVS interactive proof assistant\, the SAL model checker\, the Yices\nSMT solver\, and the Arsenal semantic p arser. He is a co-recipient of\nthe 2012 CAV Award and the recipient of t he 2022 Herbrand Award.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/106/ END:VEVENT BEGIN:VEVENT SUMMARY:Brandon Shapiro DTSTART:20231102T170000Z DTEND:20231102T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/107 DESCRIPTION:Title: (Higher) category theory in Cat^#\nby Brandon Shapi ro as part of Topos Institute Colloquium\n\n\nAbstract\nThe double categor y Cat^#\, which can be built out of polynomial comonads\, provides a compu tation-friendly mathematical language for categorical database theory\, ef fects handlers in programming\, and discrete open dynamical systems. It ha s categories as objects\, cofunctors as arrows\, and prafunctors as pro-ar rows. Monads among prafunctors\, such as the free category monad on graphs \, have algebras including categories\, n-categories (strict or weak)\, do uble categories\, multicategories (symmetric or plain)\, monoids\, monoida l categories (of nearly any variety)\, and in fact any algebraic notion of higher category whose definition is of a particular form. I will introduc e the Cat^# approach to defining (higher) categories and survey some const ructions from (higher) category theory that can be expressed in the langua ge of Cat^#\, including higher categorical nerves and "algebraic prafuncto rs" such as the free monoidal category monad on Cat.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/107/ END:VEVENT BEGIN:VEVENT SUMMARY:Simona Paoli DTSTART:20231019T170000Z DTEND:20231019T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/108 DESCRIPTION:Title: Simplicial delta versus fat delta in higher category th eory\nby Simona Paoli as part of Topos Institute Colloquium\n\n\nAbstr act\nMany structures in higher category theory have been described using t he combinatorics of simplicial objects\, based on the category simplicial delta. A prototype example is that a category can be described as a simpli cial set satisfying appropriate conditions (the so called Segal conditions ) via the nerve functor.\nIn dimension two\, simplicial objects in Cat can be used to describe strict 2-categories and double categories. Among the latter\, one can identity the category of weakly globular double categorie s which gives a model of weak 2-categories via a new paradigm to weaken hi gher categorical structures: the notion of weak globularity.\nThe fat delt a\, introduced by Joachim Kock\, carries some intuition similar to the sim plicial delta\, yet it has a different and rich structure. Kock used it to define fair 2-categories\, encoding weak 2-categories with strict composi tion laws.\nIn this talk I illustrate a direct comparison between fair 2-c ategories and weakly globular double categories which enables to interpret the weak globularity condition in terms of weak units. This comparison 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 explain t he significance of this result in terms of potential higher dimensional ge neralizations.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/108/ END:VEVENT BEGIN:VEVENT SUMMARY:Julie Bergner DTSTART:20231207T170000Z DTEND:20231207T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/109 DESCRIPTION:Title: Models for (∞\,n)-categories with discreteness condit ions\nby Julie Bergner as part of Topos Institute Colloquium\n\n\nAbst ract\nThere are two ways of turning Segal spaces into models for up-to-hom otopy categories\, or (∞\,1)-categories: either asking that the space of objects be discrete\, or requiring Rezk's completeness condition. When g eneralizing to higher (∞\,n)-categories\, both of these approaches have been taken to multisimplicial models\, in the form of Segal n-categories a nd n-fold complete Segal spaces\, but models given by Θ_n-diagrams have f ocused on the completeness conditions. In this talk\, we'll discuss how t o get a Θ_n-model with discreteness conditions\, but also address the que stion of when these conditions can be mixed and matched with one another.\ n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/109/ END:VEVENT BEGIN:VEVENT SUMMARY:Leonardo de Moura DTSTART:20230907T170000Z DTEND:20230907T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/110 DESCRIPTION:Title: Lean 4: Empowering the Formal Mathematics Revolution an d Beyond\nby Leonardo de Moura as part of Topos Institute Colloquium\n \n\nAbstract\nThis talk presents Lean 4\, the latest version of the Lean p roof assistant\, and its impact on the mathematical community. We first in troduce the project's design and objectives\, followed by the mission of t he newly established Lean Focused Research Organization (FRO).\nThe advent of Lean and similar proof assistants has sparked a transformation in math ematical practice\, an era we refer to as the "Formal Mathematics Revoluti on". We'll explore how Lean 4 contributes to this revolution\, with its to ols and structures enabling mathematicians to formalize complex theories a nd proofs with unprecedented ease. A key aspect of our philosophy is facil itating decentralized innovation. We discuss the strategies employed to em power a diverse community of researchers\, developers\, and enthusiasts 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 on ly created an environment for formalizing mathematics but also an effectiv e tool for writing software\, enabling a smooth interaction between mathem atical and computational aspects. Finally\, we will look ahead\, sharing o ur vision and planned steps for the future of Lean 4 and the Lean FRO. We' ll discuss how we aim to further grow the user base\, continue improving u sability\, and deepen the reach of formal methods into mathematics and com puter science.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/110/ END:VEVENT BEGIN:VEVENT SUMMARY:Dominic Orchard DTSTART:20231012T170000Z DTEND:20231012T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/111 DESCRIPTION:Title: Programming for the Planet\nby Dominic Orchard as p art of Topos Institute Colloquium\n\n\nAbstract\nClimate change is one of the greatest challenges of our time. Assessing its risks and our progress towards mitigating its worst effects requires a wealth of data about our n atural environment that we rapidly process into accurate indicators\, asse ssments\, and predictions\, with sufficient trust in the resulting insight s to make decisions that affect the lives of billions worldwide\, both now and in the future. However\, in the last decade\, climate modelling has f aced diminishing returns from current hardware trends and software techniq ues. Furthermore\, developing the required models and analysis tools to ef fectively process\, explore\, archive\, and derive policy decisions\, with a high degree of transparency and trust\, remains difficult. I argue that more cross-disciplinary effort between mathematics\, computer science\, s oftware engineering\, and data science is needed to help close the gap bet ween 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 progra mming in addressing the needs of climate science. I will also make connect ions to relevant areas of category theory which could be leveraged to deve lop more flexible climate models in the future.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/111/ END:VEVENT BEGIN:VEVENT SUMMARY:Michael Levin DTSTART:20230921T170000Z DTEND:20230921T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/112 DESCRIPTION:Title: Emergent Selves and Unconventional Intelligences: where philosophy and engineering meet\nby Michael Levin as part of Topos In stitute Colloquium\n\n\nAbstract\nWe are composites\, made out an agential material. In this talk\, I \nwill describe how molecular pathways\, cells \, tissues\, and organs display \nintelligence - problem-solving and creat ive behavior in a variety of \ndiverse problem spaces. I will describe evo lutionary aspects of this \namazing multiscale competency architecture\, a nd how the cognition of \ncells scales up to the grandiose goals of morpho genetic\, behavioral\, and \nlinguistic collectives. I will show data from my lab that uses \ndevelopmental biophysics\, computer science\, and beha vioral science to \nunderstand diverse intelligence and work towards pract ical\, biomedical \napplications of these ideas (in areas of regeneration birth defects\, and \ncancer). I will also describe our synthetic life for ms\, which we use to \nunderstand the latent space of goals for collective systems without an \nevolutionary history.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/112/ END:VEVENT BEGIN:VEVENT SUMMARY:Tom Leinster DTSTART:20231026T170000Z DTEND:20231026T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/113 DESCRIPTION:Title: Entropy and diversity: the axiomatic approach\nby T om Leinster as part of Topos Institute Colloquium\n\n\nAbstract\nEcologist s have been debating the best way to measure diversity for more\nthan 70 y ears. The concept of diversity is relevant not only in ecology\,\nbut also in other fields such as genetics and economics\, as well as being\nclosel y related to information entropy. \n\nThe question of how best to quantify diversity has surprising mathematical\ndepth. Indeed\, a general study of invariants resembling cardinality and\nEuler characteristic led to the un ifying notion of the magnitude of an\nenriched category - a quantity which is also closely related to the maximum\ndiversity of a community of presc ribed species. I will give a high-level\noverview of the concepts of entro py\, diversity and magnitude\, and how they\nfit together.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/113/ END:VEVENT BEGIN:VEVENT SUMMARY:Maurice Chiodo DTSTART:20231116T170000Z DTEND:20231116T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/114 DESCRIPTION:Title: Normalising ethical reasoning for mathematicians\nb y Maurice Chiodo as part of Topos Institute Colloquium\n\n\nAbstract\nIn t he past 10 years there has been a significant increase in the level of att ention on issues of ethical and responsible development in mathematics. "E thics in Mathematics" is now a recognised area of study\, and there are no w substantially more resources to consult on this. However\, such understa nding has not yet permeated into the minds of the bulk of mathematicians. Most either have minimal realisation of the need to consider ethical and s ocietal issues when carrying out mathematical work\, or lack the skill set needed to carry out such thinking in a thorough and systematic way. In sh ort: most mathematicians either don't know how to spot ethical issues\, 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 "Teachin g Resources for Embedding Ethics in Mathematics" (arXiv:2310.08467)\, whic h is a tool to embed ethics in mathematics teaching by way of mathematical exercises that normalise ethical considerations. I will also present my " Manifesto for the Responsible Development of Mathematical Works" (arXiv:23 06.09131)\, which is a tool to help mathematicians dissect their workflow and identify the points at which their actions and choices may lead to har mful consequences. In short: train mathematicians to think about ethics al l the time\, then educate them on what to do when they identify such issue s.\nThese are joint works with Dennis Müller\, and form part of the Cambr idge University Ethics in Mathematics Project (ethics.maths.cam.ac.uk).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/114/ END:VEVENT BEGIN:VEVENT SUMMARY:John Cartmell DTSTART:20240118T170000Z DTEND:20240118T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/115 DESCRIPTION:Title: Aspects of a Mathematical Theory of Data\nby John C artmell as part of Topos Institute Colloquium\n\n\nAbstract\nI will discus s significant aspects of a theory of data and what may be achieved by repr esenting data specifications as sketches of Range Categories with additio nal structure. I will discuss the distinction between relational and non-r elational physical data specifications and contrast physical and logical d ata specifications. I will discuss goodness criteria for such specificatio ns and define some specific criteria which generalise the classic relation al goodness criteria i.e. the so called normal forms of Codd\, Fagin\, Lin g and Goh and others.\n\nMy goal for a fully elaborated Mathematical Theor y of Data is to effect a change in what is considered best practice for th e way in which data is specified and programmed as as to enable best pract ice to be shifted from being at the level that data is physically represen ted and communicated to being at the more abstract level of its logical st ructure.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/115/ END:VEVENT BEGIN:VEVENT SUMMARY:Minhyong Kim DTSTART:20231130T170000Z DTEND:20231130T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/116 DESCRIPTION:Title: Who Owns Mathematics: A Question of Identity\nby Mi nhyong Kim as part of Topos Institute Colloquium\n\n\nAbstract\nAt a recen t conference on the global history of mathematics\, a question was raised about the recurrence of Euclid in a number of the talks and the 'Western' bias that seemed to appear in a meeting that was concerned with global his tory. In this talk\, I will discuss the misconceptions around the identiti es of historical figures like Euclid\, the deep-rooted confusion surroundi ng ancient identities in general\, and why it might be important for mathe maticians of our times to be aware of them.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/116/ END:VEVENT BEGIN:VEVENT SUMMARY:Susan Niefield DTSTART:20240208T170000Z DTEND:20240208T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/117 DESCRIPTION:Title: Cauchy Completeness and Adjoints in Double Categories\nby Susan Niefield as part of Topos Institute Colloquium\n\n\nAbstract\ nIn his 1973 paper (TAC Reprints\, 2002)\, Lawvere observed that a metric space Y is a category enriched in the extended reals\, and showed that Y i s Cauchy complete if and only if every bimodule (i.e.\, profunctor) with c odomain Y has a right adjoint. More recently\, Paré (2021) considered adj oints and Cauchy completeness in double categories\, and showed that an (S \,R)-bimodule M has a right adjoint in the double category of commutative rings if and only if it is finitely generated and projective as an S-modul e. It is well known that the latter property characterizes the existence o f a left adjoint to tensoring with M on the category of S-modules\, and th is was generalized to rigs and quantales in a 2017 paper by Wood and the s peaker.\n\nThis talk consists of two parts. First\, after recalling the re levant definitions\, we present examples of Cauchy complete objects in som e "familiar" double categories. Second\, we incorporate the two above ment ioned projectivity results into a version of the 2017 theorem with Wood wh ich we then apply to (not-necessarily commutative) rings\, rigs\, and quan tales.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/117/ END:VEVENT BEGIN:VEVENT SUMMARY:Juan Pablo Vigneaux DTSTART:20240125T170000Z DTEND:20240125T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/118 DESCRIPTION:Title: Cohomological aspects of information\nby Juan Pablo Vigneaux as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk w ill discuss the cohomological aspects of information functions within the framework of information cohomology (first introduced by Baudot and Benneq uin in 2015). Several known functionals can be identified as cohomology cl asses in this framework\, including the Shannon entropy of discrete probab ility measures and the differential entropy and underlying dimension of co ntinuous measures. I’ll try to provide an accessible overview of the fou ndations of the theory\, which should require only a basic familiarity wit h category theory and homological algebra\, and survey the main known resu lts. Finally\, I'll discuss some perspectives and open problems: firstly i n connection with Renyi's information dimension and other (possibly geomet ric) invariants of laws taking values on manifolds\, and secondly with not ions of entropy for categories (akin to Leinster's diversity of metric spa ces).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/118/ END:VEVENT BEGIN:VEVENT SUMMARY:André Joyal DTSTART:20231214T170000Z DTEND:20231214T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/119 DESCRIPTION:Title: Higher topos theory and Goodwillie Calculus\nby And ré Joyal as part of Topos Institute Colloquium\n\n\nAbstract\nLurie's hig her topos theory is a vast extension of Grothendieck's topos theory. I wil l compare the two theories\, stressing similarities and differences. The f act that the ∞-category of parametrised spectra is a higher topos has no analog in Grothendieck topos theory. It is the first stage of the Goodwil lie tower associated to any left exact localization of a higher topos. The tower can be understood in analogy with the completion tower of an ideal in a commutative ring. For many purposes\, a topos has the dual aspects o f a space (the topos) and of a ring (the logos). The category of logoi (=t he opposite of the category of topoi) has many properties in common with t he category of commutative rings.\n\nIn collaboration with Mathieu Anel\, Georg Biedermann and Eric Finster.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/119/ END:VEVENT BEGIN:VEVENT SUMMARY:Robert Paré DTSTART:20240111T170000Z DTEND:20240111T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/120 DESCRIPTION:Title: The functorial difference operator\nby Robert Paré as part of Topos Institute Colloquium\n\n\nAbstract\nAs a tool for studyi ng the structure of endofunctors F of Set\, \nwe introduce the difference operator△\n\n△[F](X) = F(X + 1) \\ F(X).\n\nThis is analogous to the c lassical difference operator for real\nvalued functions\, a discrete form of the derivative.\n\nThe \\ above is set difference and can't be expect ed to be functorial\,\nbut it is for a large class of functors\, the taut functors of Manes\, \nwhich include polynomial functors and many more.\n\n We obtain combinatorial versions of classical identities\, often\n''improv ed'. Many examples will be given.\n\nThe talk should be accessible to ever yone. The only prerequisite \nis some very basic category theory.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/120/ END:VEVENT BEGIN:VEVENT SUMMARY:André Joyal DTSTART:20240215T170000Z DTEND:20240215T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/121 DESCRIPTION:Title: Free bicompletion of categories revisited (part 1)\ nby André Joyal as part of Topos Institute Colloquium\n\n\nAbstract\nWhit man's theory of free lattices can be extended to free lattices enriched ov er a quantales\, to free bicomplete enriched categories and even to free b icomplete enriched oo-categories. It has applications to the semantic of L inear Logic (Hongde Hu and J.)\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/121/ END:VEVENT BEGIN:VEVENT SUMMARY:Joachim Kock DTSTART:20240222T170000Z DTEND:20240222T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/122 DESCRIPTION:Title: Polynomial functors — from elementary arithmetic to i nfinity-operads\nby Joachim Kock as part of Topos Institute Colloquium \n\n\nAbstract\nIn their simplest form\, polynomial functors are endofunct ors of the category of sets built from sums and products. At first they ca n be considered a categorification of the notion of polynomial function\, but it has turned out the theory of polynomial functors is more generally an efficient toolbox for dealing with induction\, nesting\, and substituti on. The talk will highlight some of these aspects in combinatorics\, logic \, and homotopy theory.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/122/ END:VEVENT BEGIN:VEVENT SUMMARY:Steven Clontz DTSTART:20240328T170000Z DTEND:20240328T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/123 DESCRIPTION:Title: Sociotechnical infrastructure for mathematics research< /a>\nby Steven Clontz as part of Topos Institute Colloquium\n\n\nAbstract\ nThe National Science Foundation defines "cyberinfrastructure" as "the har dware\, software\, networks\, data and people that underpin today's advanc ed computing technology"\, particularly technologies that advance scientif ic discovery. In particular\, this infrastructure is incomplete without it s "people"\, leading some to prefer the terminology "sociotechnical infras tructure" to emphasize the importance of how these technologies connect hu man researchers\, and how human researchers in turn use and develop these technologies in order to create new knowledge. In mathematics research\, e ven theoretical mathematics\, we use many technologies\, and engage with m any 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 as part of my spring 2024 sabbatical dedicated to the research and development of improved sociotechnical infrastructure for mathematics research.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/123/ END:VEVENT BEGIN:VEVENT SUMMARY:Po-Shen Loh DTSTART:20240404T170000Z DTEND:20240404T180000Z DTSTAMP:20260423T094652Z 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 Topos Inst itute Colloquium\n\n\nAbstract\nOne of the central challenges of beyond-st andard-curriculum instruction (such as "gifted" education) is how to achie ve equitably-distributed scale. Making matters worse\, generative AI such as ChatGPT is increasingly adept at solving standard curricular tasks\, s o it is urgent to scalably deliver teaching that goes beyond current stand ards. Fortunately\, there is an area close to math which devises solutions in which problems solve themselves even through self-serving human behavi or: Game Theory.\n\nThe speaker will describe his recent work\, which uses Game Theory to create a novel alignment of incentives\, which concurrentl y solves pain points in disparate sectors. At the heart of the innovation is a new\, mutually-beneficial cooperation between high school math stars and professionally trained actors and comedians. This creates a highly sca lable community of extraordinary coaches with sufficient capacity to teach large numbers of middle schoolers seeking to learn critical thinking and creative analytical problem solving (https://live.poshenloh.com). At the s ame time\, it creates a new pathway for high school math stars to signific antly strengthen their emotional intelligence. The whole program is conduc ted virtually\, so it reaches through geographical barriers. The speaker w ill also share his experience extending this work to build talent developm ent pipelines in underprivileged communities\, identifying and supporting highly motivated middle school students who otherwise did not have access to coaching.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/124/ END:VEVENT BEGIN:VEVENT SUMMARY:Rodrigo Ochigame DTSTART:20240815T170000Z DTEND:20240815T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/125 DESCRIPTION:Title: The Automation of Mathematics from an Anthropological P erspective\nby Rodrigo Ochigame as part of Topos Institute Colloquium\ n\n\nAbstract\nThis talk will examine some aspects of the ongoing automati on of mathematical research from an anthropological perspective. It will f irst address the diversity of practical standards of proof (across fields\ , places\, and times)\, the longstanding tension between “understanding ” and mechanical “checking\,” and the persistent need for social adj udication even for computer-encoded (“formal”) proofs. It will then di scuss how automation might affect divisions of labor\, economies of credit \, institutional hierarchies\, and structures of incentive and reward in p rofessional research. The talk will also draw comparisons to current debat es about automation and machine learning in other fields of science\, such as experimental physics.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/125/ END:VEVENT BEGIN:VEVENT SUMMARY:Gioele Zardini DTSTART:20240425T170000Z DTEND:20240425T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/126 DESCRIPTION:Title: Co-Design of Complex Systems: From Autonomy to Future M obility\nby Gioele Zardini as part of Topos Institute Colloquium\n\n\n Abstract\nWhen designing complex systems\, we need to consider multiple tr ade-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) and the d esign of the mobility systems they enable are closely coupled. Indeed\, kn owledge about the intended service of novel mobility solutions would impac t their design and deployment process\, while insights about their technol ogical development could significantly affect transportation management po licies. Optimally co-designing sociotechnical systems is a complex task fo r at least two reasons. On one hand\, the co-design of interconnected syst ems (e.g.\, large networks of cyber-physical systems) involves the simulta neous choice of components arising from heterogeneous natures (e.g.\, hard ware vs. software parts) and fields\, while satisfying systemic constraint s and accounting for multiple objectives. On the other hand\, components a re connected via collaborative and conflicting interactions between differ ent stakeholders (e.g.\, within an intermodal mobility system). In this ta lk\, I will present a framework to co-design complex systems\, leveraging a monotone theory of co-design and tools from applied category theory. The framework will be instantiated in the task of designing future mobility s ystems\, all the way from the policies that a city can design\, to the aut onomy of vehicles as part of an autonomous mobility-on-demand service. Thr ough various case studies\, I will show how the proposed approaches allow one to efficiently answer heterogeneous questions\, unifying different mod eling techniques and promoting interdisciplinarity\, modularity\, and comp ositionality. I will then discuss open challenges for compositional system s design optimization\, and present my agenda to tackle them.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/126/ END:VEVENT BEGIN:VEVENT SUMMARY:Mason Porter DTSTART:20240627T170000Z DTEND:20240627T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/127 DESCRIPTION:Title: Topological Data Analysis of Spatial Systems\nby Ma son Porter as part of Topos Institute Colloquium\n\n\nAbstract\nI will dis cuss topological data analysis (TDA)\, which uses ideas from topology to q uantify the "shape" of data. I will focus in particular on persistent homo logy (PH)\, which one can use to find "holes" of different dimensions in d ata sets. I will briefly introduce these ideas and then discuss a series o f examples of TDA of spatial systems. The examples that I'll discuss inclu de voting data\, the locations of polling sites\, and the webs of spiders under the influence of various drugs.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/127/ END:VEVENT BEGIN:VEVENT SUMMARY:Nicola Gambino DTSTART:20240523T170000Z DTEND:20240523T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/128 DESCRIPTION:Title: Monoidal bicategories\, differential linear logic\, and analytic functors\nby Nicola Gambino as part of Topos Institute Collo quium\n\n\nAbstract\nThe aim of this talk is to present bicategorical coun terparts of the notions of a linear explonential comonad\, as considered i n the study of linear logic\, and of a codereliction transformation\, intr oduced in the study of differential linear logic via differential categori es. As an application\, the differential calculus of Joyal's analytic func tors will be extended to analytic functors between presheaf categories\, i n a way that is analogous to how ordinary calculus extends from a single v ariable to many variables. This is based on joint work with Marcelo Fiore and Martin Hyland (https://arxiv.org/abs/2405.05774).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/128/ END:VEVENT BEGIN:VEVENT SUMMARY:Spencer Breiner DTSTART:20240905T170000Z DTEND:20240905T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/129 DESCRIPTION:Title: Polynomial Interfaces\nby Spencer Breiner as part o f Topos Institute Colloquium\n\n\nAbstract\nI will argue that applied cate gory theory would benefit\, both practically and strategically\, from grea ter attention to user interface. Starting from some very basic examples\, I will discuss some of the conceptual challenges in this area and explain how they map onto categorical structures like monads\, comonads and polyno mial functors. I will close with a discussion of the Semagrams user inter face library\, its goals and future prospects.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/129/ END:VEVENT BEGIN:VEVENT SUMMARY:Eugenio Moggi DTSTART:20240509T170000Z DTEND:20240509T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/130 DESCRIPTION:Title: Categories of Classes for Collection Monads\nby Eug enio Moggi as part of Topos Institute Colloquium\n\n\nAbstract\nIn 1998 Ma nes introduced the notion of collection monad on the category of sets as a suitable semantics for collection types. The canonical example of collec tion monad is the finite powerset monad.\n\nIn order to account for the al gorithmic aspects the category of sets should be replaced with other categ ories\, whose arrows are maps computable by "low complexity" algorithms.\n \nWe extends Manes' definition of collection monad to models for weak vers ions of Algebraic Set Theory (AST). AST was proposed by Joyal and Moerdij k in the '90 as a category-theoretic counterpart of Bernays' set theory ba sed on classes.\n\nWe give a systematic way to construct such models\, whi ch include\ncategories whose arrows are "low complexity" functions between countable sets.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/130/ END:VEVENT BEGIN:VEVENT SUMMARY:Will Crichton DTSTART:20240822T170000Z DTEND:20240822T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/131 DESCRIPTION:Title: How to Make Mathematicians Into Programmers (And Vice V ersa)\nby Will Crichton as part of Topos Institute Colloquium\n\n\nAbs tract\nTools for formalized mathematics (FM)\, such as proof assistants an d model checkers\, are increasingly capable of handling the real-world pro blems of both mathematicians and software developers. Yet\, these tools ar e only as effective as the people who use them. The FM community clearly n eeds to invest in better education and better tooling. But... which curric ula are actually effective for learners? What tooling will actually make u sers more productive? In this talk\, I will lay out some preliminary ideas for how to systematically investigate these questions\, i.e.\, develop a science of human factors for FM. My core proposal is to combine experiment al psychological methods (e.g.\, lab studies\, IDE telemetry) and cognitiv e theories (e.g.\, working memory\, mental models) to study how people use FM tools. Then that understanding can be applied to make principled predi ctions about the efficacy of curricula\, tooling\, and language design.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/131/ END:VEVENT BEGIN:VEVENT SUMMARY:Elena Di Lavore DTSTART:20240516T170000Z DTEND:20240516T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/132 DESCRIPTION:Title: Effectful trace semantics via effectful streams\nby Elena Di Lavore as part of Topos Institute Colloquium\n\n\nAbstract\nEffe ctful streams are a coinductive semantic universe for effectful dataflow p rogramming and traces. As an example\, we formalise the stream cipher cryp tographic protocol. In monoidal categories with conditionals and ranges\, effectful streams particularize to families of morphisms satisfying a caus ality condition. Effectful streams allow us to develop notions of trace an d bisimulation for effectful Mealy machines\; bisimulation implies effectf ul trace equivalence.\n\nThis is recent joint work with Filippo Bonchi and Mario Román.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/132/ END:VEVENT BEGIN:VEVENT SUMMARY:Edward Lee DTSTART:20240418T170000Z DTEND:20240418T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/133 DESCRIPTION:Title: Certainty or Intelligence: Pick One!\nby Edward Lee as part of Topos Institute Colloquium\n\n\nAbstract\nMathematical models can yield certainty\, as can probabilistic models where the probabilities degenerate. The field of formal methods emphasizes developing such certain ty about engineering designs. In safety critical systems\, such certainty is highly valued and\, in some cases\, even required by regulatory bodies. But achieving reasonable performance for sufficiently complex environment s appears to require the use of AI technologies\, which resist such certai nty. This talk suggests that certainty and intelligence may be fundamental ly incompatible.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/133/ END:VEVENT BEGIN:VEVENT SUMMARY:Steve Vickers DTSTART:20240530T170000Z DTEND:20240530T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/134 DESCRIPTION:Title: The Fundamental Theorem of Calculus: point-free\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 space 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 opens of th e space correspond to propositional formulae derived from the theory: thus the theory defines both the points and the topology. Then continuity of m aps just means that they are constructed in accordance with the constraint s of the logic.\n\nWhy bother to do topology that way? After all\, the log ic is even more constrained than constructive reasoning\, and we still don ’t know how far it reaches.\n\nThe first reason is that it quite painles sly extends to toposes\, viewed as generalized spaces. This uses the machi nery of classifying toposes\, but only in an unobtrusive way [1]. Many pro per classes can then be viewed as point-free spaces - just write down a ge ometric theory whose models are the elements of the class.\n\nThe second r eason follows from the first but can then be applied back to ungeneralized spaces in a very natural treatment of bundles. Theory presentations can t hemselves be described as the models of a geometric theory\, and this allo ws us to view bundles as continuously mapping base points to spaces (the f ibres). For physics in particular\, this invites exploration of how much c an be done using geometric methods. See eg [2].\n\nMeanwhile\, there is th e question of how much ordinary mathematics\, and in particular real analy sis\, can be done in this style. I present as a case study the Fundamental Theorem of Calculus [3]. This illustrates some typically geometric featur es of the reasoning\, such as attention paid to one-sided reals and the us e of hyperspaces and their analogues\, and some exploitation of the geomet ric fact that everything is continuous\, as well as a cute new trick using uniform probability measures.\n\n[1] Steven Vickers “Topical categories of domains”\, Mathematical Structures in Computer Science 9 (1999)\n[2] Bas Spitters\, Steven Vickers and Sander Wolters “Gelfand spectra in Gr othendieck toposes using geometric mathematics"\, Electronic Proceedings i n Theoretical Computer Science 158 (2014)\n[3] Steven Vickers “The Funda mental Theorem of Calculus point-free\, with applications to exponentials and logarithms"\, arXiv:2312.05228\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/134/ END:VEVENT BEGIN:VEVENT SUMMARY:Alex Simpson DTSTART:20240606T170000Z DTEND:20240606T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/135 DESCRIPTION:Title: Three toposes for probability and randomness\nby Al ex Simpson as part of Topos Institute Colloquium\n\n\nAbstract\nI shall gi ve a brief guided tour of three toposes that have arisen in a research pro gramme to model aspects of probability and randomness from a topos perspe ctive. The first topos of "probability sheaves" supports a synthetic style of probabilistic reasoning about random variables. The second "random top os" makes sense of the notion of "random element" and models a world in w hich all sets are measurable. The third topos of "random probability sheav es" combines the previous two and provides a home for a more radical style of "synthetic probability theory" expunged of all concerns about sigma-al gebras\, measurability and the like.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/135/ END:VEVENT BEGIN:VEVENT SUMMARY:Kathrin Stark DTSTART:20240801T170000Z DTEND:20240801T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/136 DESCRIPTION:Title: On Taming Differentiable Logics\nby Kathrin Stark a s part of Topos Institute Colloquium\n\n\nAbstract\nFor performance and ve rification in machine learning\, new methods have recently been proposed t hat optimise learning systems to satisfy formally expressed logical proper ties. Among these methods\, differentiable logics (DLs) are used to transl ate propositional or first-order formulae into loss functions deployed for optimisation in machine learning. At the same time\, recent attempts to g ive programming language support for verification of neural networks showe d that DLs can be used to compile verification properties to machine-learn ing backends. This situation is calling for stronger guarantees about the soundness of such compilers\, the soundness and compositionality of DLs\, and the differentiability and performance of the resulting loss functions. In this talk\, I report on recent work to 1.) give uniform semantics to a nd 2.) to formalise existing DLs using the Mathematical Components library in the Coq proof assistant. This work is meant as a stepping stone for th e development of programming language support for verification of machine learning.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/136/ END:VEVENT BEGIN:VEVENT SUMMARY:Filippo Bonchi DTSTART:20240502T170000Z DTEND:20240502T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/137 DESCRIPTION:Title: Diagrammatic Algebra of First Order Logic\nby Filip po Bonchi as part of Topos Institute Colloquium\n\n\nAbstract\nWe introduc e the calculus of neo-Peircean relations\, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as fir st order logic and comes with a complete axiomatisation. The axioms are ob tained by combining two well known categorical structures: cartesian and l inear bicategories.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/137/ END:VEVENT BEGIN:VEVENT SUMMARY:Bartosz Milewski DTSTART:20240613T170000Z DTEND:20240613T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/139 DESCRIPTION:Title: Parametric Profunctor Preoptics\nby Bartosz Milewsk i as part of Topos Institute Colloquium\n\n\nAbstract\nLocally graded cate gories and parametric optics provide a compositional model of neural netwo rks. I will show how to generalize this approach to pre-optics. I'll intro duce a parametric profunctor representation of preoptics and use it to imp lement a perceptron in Haskell.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/139/ END:VEVENT BEGIN:VEVENT SUMMARY:Cyrus Omar DTSTART:20240829T170000Z DTEND:20240829T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/140 DESCRIPTION:Title: Totally Live Programming and Proving in Hazel\nby C yrus Omar as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk w ill review progress on the Hazel programming environment and its underlyin g theoretical developments. Hazel is the first totally live typed general- purpose programming environment\, meaning that it deploys error localizati on and recovery mechanisms\, rooted in language-theoretic developments\, t hat ensure that every editor state is syntactically well-structured and st atically and dynamically meaningful. The talk will review the underlying t heory and include a live demonstration of various Hazel features\, includi ng its editor\, training mode\, and its stepper\, which is forming the bas is for ongoing work on a Hazel-based theorem prover. The talk will also di scuss various other ongoing and future directions of interest to the commu nity\, including our vision for a "computational commons" that operates li ke a planetary-scale live program.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/140/ END:VEVENT BEGIN:VEVENT SUMMARY:Seth Frey DTSTART:20240926T170000Z DTEND:20240926T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/141 DESCRIPTION:Title: Online communities as model systems for commons governa nce\nby Seth Frey as part of Topos Institute Colloquium\n\n\nAbstract\ nThe best citizens of a large-scale democracy are those who have built and broken several small ones to see how they work. By empowering people to b uild any kind of community together\, the Internet has become a laboratory for self-governance experimentation. Groups who start online communities must overcome the challenges of recruiting finite resources around difficu lt common goals. Fortunately\, they can draw on a growing range of support technologies\, peer networks\, and scholarship. With their transparency\ , the Internet's millions of online communities can be surveyed for insigh ts into their design and functioning. Looking at three large platforms for small self-governing online communities\, we will pose several questions of institutional processes at the population level\, as drawn from the lit eratures on common-pool resource management and institutional analysis and design.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/141/ END:VEVENT BEGIN:VEVENT SUMMARY:Arthur J Parzygnat DTSTART:20240808T170000Z DTEND:20240808T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/142 DESCRIPTION:Title: A generalization of inversion using Bayes' rule with ap plications to quantum\nby Arthur J Parzygnat as part of Topos Institut e Colloquium\n\n\nAbstract\nBayes' rule has recently been given a categori cal definition in terms of string diagrams due to Cho and Jacobs. This def inition of Bayesian inversion\, however\, is not robust enough for categor ies that include reasoning about quantum systems due to the no-cloning the orem. In this talk\, I will explain how semi-cartesian categories (which h ave less structure than Markov categories) provide a suitable framework to define Bayesian inversion categorically. In particular\, I will provide a xioms for such an abstract form of Bayesian inversion. It remains an open question whether these axioms characterize Bayesian inversion for quantum systems.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/142/ END:VEVENT BEGIN:VEVENT SUMMARY:Fabio Gadducci DTSTART:20240711T170000Z DTEND:20240711T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/143 DESCRIPTION:Title: From gs-monoidal to cartesian categories: a structural analysis\nby Fabio Gadducci as part of Topos Institute Colloquium\n\n\ nAbstract\nIt is now folklore that cartesian categories can be viewed as s ymmetric monoidal ones equipped with two natural transformations\, modelli ng diagonals and projections. In this talk we explore the taxonomy obtaine d by relaxing the naturality requirement\, from gs-monoidal/cd-categories to restriction and Markov ones. We show how these possibly order-enriched 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://researchseminars.org/talk/ToposInstituteColloquium/143/ END:VEVENT BEGIN:VEVENT SUMMARY:Amélia Liao DTSTART:20241003T170000Z DTEND:20241003T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/145 DESCRIPTION:Title: Cubical types for the working formalizer\nby Améli a Liao as part of Topos Institute Colloquium\n\n\nAbstract\nCubical type t heory is an extension of dependent type theory designed\n to make the univ alence principle *provable*\, rather than an axiom.\n Then\, by what is es sentially a happy coincidence\, it also provides a\n design for working wi th 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 use r of cubical type theory is directly exposed to the\n complicated primitiv e operations that let us implement these higher\n features\, even if they' re working on set-level mathematics. Worse\, any\n implementation of HoTT imposes additional proof obligations to stay in\n the realm of sets rather than escaping off into coherence purgatory.\n\n This talk discusses the e xperience of using cubical type theory to\n build the 1Lab— in particula r\, the automation we've been building so\n the end-user of the library do es not have to memorise the cubical type\n theory papers if all they want is to formalise traditional\,\n low-homotopy level mathematics.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/145/ END:VEVENT BEGIN:VEVENT SUMMARY:Thomas Powell DTSTART:20241016T170000Z DTEND:20241016T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/146 DESCRIPTION:Title: Quantitative results for stochastic processes\nby T homas Powell as part of Topos Institute Colloquium\n\n\nAbstract\nIt is an elementary fact from real analysis that any monotone bounded sequence of real numbers converges. It turns out that the monotone convergence theorem can be given an equivalent finitary formulation: roughly that any suffici ently long monotone bounded sequence experiences long regions where the se quence is metastable. This so-called "finite convergence principle" is car efully motivated and discussed by Terence Tao in a 2007 blog post ('Soft a nalysis\, hard analysis\, and the finite convergence principle')\, but was already known to proof theorists\, where the use of logical methods to bo th finitize infinitary statements and provide uniform quantitative informa tion for the finitary versions plays a central role in the so-called proof mining program.\n\nThe goal of my talk is to discuss how methods from pro of mining can be applied to the theory of stochastic processes\, an area o f mathematics hitherto unexplored from this perspective. I will begin by d iscussing the simple monotone convergence principle\, and will then focus on how everything I mentioned above can be generalised to the analogous re sult in the stochastic setting: Doob's martingale convergence theorems. Th is then sets the groundwork for new applications of proof theory in stocha stic optimization\, and I will give a high level overview of some work in progress in this direction\, including a quantitative analysis of the famo us Robbins-Siegmund lemma. This is all joint work with my PhD student More nikeji Neri.\n\nIn giving the talk I will not assume any knowledge of proo f theory\, just some elementary analysis and probability theory.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/146/ END:VEVENT BEGIN:VEVENT SUMMARY:Christine Tasson DTSTART:20240912T170000Z DTEND:20240912T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/149 DESCRIPTION:Title: Semantics for Reactive Probabilistic Programming\nb y Christine Tasson as part of Topos Institute Colloquium\n\n\nAbstract\nSy nchronous languages are now a standard industry tool for critical embedded systems. Designers write high-level specifications by composing streams o f values. These languages have been extended with Bayesian reasoning to pr ogram state-space models which compute a stream of distributions given a s tream of observations [1].\n\nThis talk aims at describing semantics for p robabilistic synchronous languages\, based on a joint work with Guillaume Baudart and Louis Mandel [2]. The key idea is to interpret probabilistic e xpressions as a stream of un-normalized density functions which maps rando m variable values to a result and positive score. Two equivalent semantics are presented: the co-iterative semantics is executable while the relatio nal semantics is easy to use for proving program equivalence. The semantic al framework is then applied to prove the correctness of a program transfo rmation required to run an optimized inference algorithm.\n\n[1] Reactive Probabilistic Programming\, Guillaume Baudart et al\, PLDI 2020\n[2] Densi ty-Based Semantics for Reactive Probabilistic Programming\, Guillaume Baud art\, Louis Mandel\, Christine Tasson\, arxiv:2308.01676\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/149/ END:VEVENT BEGIN:VEVENT SUMMARY:Chris Fields DTSTART:20240919T170000Z DTEND:20240919T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/150 DESCRIPTION:Title: What is the Identity operator?\nby Chris Fields as part of Topos Institute Colloquium\n\n\nAbstract\nThe idea that objects ha ve associated Identity morphisms\, or operators\, is fundamental to mathem atics\, physics\, and the theory of Active Inference. All of these\, moreo ver\, support the idea that identity can be maintained via multiple paths. We will explore the relationship between the idea of identity and the not ions of space\, time\, and memory\, with an emphasis on how these latter t hree relate to the idea of an object in both physical theory and active in ference.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/150/ END:VEVENT BEGIN:VEVENT SUMMARY:Mario Román DTSTART:20241031T170000Z DTEND:20241031T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/151 DESCRIPTION:Title: Partial Markov Categories\nby Mario Román as part of Topos Institute Colloquium\n\n\nAbstract\nPartial Markov categories are an algebra and syntax for Bayesian inference. They use a string diagramma tic syntax—with a formal correspondence to programs—to reason about co ntinuous and discrete probability\, decision problems (Monty Hall\, Newcom b's)\, the compositional properties of normalization\, and an abstract Bay es' theorem.\n\nPartial Markov categories are a careful blend of Markov ca tegories (from categorical probability theory) and cartesian restriction c ategories (from the algebraic theory of partial computations). We will dis cuss the construction\, theory\, and applications of partial Markov catego ries.\n\nThis is joint work with Elena Di Lavore. It is based on "Evidenti al Decision Theory via Partial Markov Categories"\, presented at LiCS'23 ( https://arxiv.org/abs/2301.12989).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/151/ END:VEVENT BEGIN:VEVENT SUMMARY:Carl Miller DTSTART:20241107T170000Z DTEND:20241107T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/152 DESCRIPTION:Title: Graphical Methods in Quantum Cryptography\nby Carl Miller as part of Topos Institute Colloquium\n\n\nAbstract\nMathematical s ecurity 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 re search) is managing the complexity of these proofs. Fully rigorous securi ty proofs can occupy a lot of space even when the underlying ideas are rel atively simple. In the subfield of quantum cryptography\, which incorpora tes quantum states and processes\, this challenge has additional complicat ions.\n\nVisual reasoning helps illuminate proofs in cryptography\, and in some cases\, visual reasoning can actually serve as a replacement for sym bolic reasoning. In this talk I will discuss how picture-proofs\, based o n categorical quantum mechanics\, can be incorporated into quantum cryptog raphy.\n\nReferences:\n\n- Breiner\, Spencer\, Carl A. Miller\, and Neil J . Ross. "Graphical methods in device-independent quantum cryptography." Qu antum 3 (2019): 146. arXiv:1705.09213\n\n- Breiner\, Spencer\, Amir Kalev \, and Carl Miller. "Parallel Self-Testing of the GHZ State with a Proof b y Diagrams." 15th International Conference on Quantum Physics and Logic. E lectronic Proceedings in Theoretical Computer Science (EPTCS)\, 2018. arXi v:1806.04744\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/152/ END:VEVENT BEGIN:VEVENT SUMMARY:Arezoo Islami DTSTART:20241114T170000Z DTEND:20241114T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/153 DESCRIPTION:Title: Unravelling the "Unreasonable Effectiveness" of Mathema tics\nby Arezoo Islami as part of Topos Institute Colloquium\n\n\nAbst ract\nThe Applicability Problem is the problem of explaining why mathemati cs is applicable to the empirical sciences. This problem is revived and re formulated by the physicist Eugene Wigner under the striking title "The Un reasonable Effectiveness of Mathematics in the Natural Sciences". In this influential work\, Wigner argues that the applicability of mathematics is a miracle\, "a wonderful gift which we neither understand nor deserve". Re sponses to this problem range from metaphysical claims about the mathemati cal structure of the universe to epistemic claims about the nature of huma n cognition\, as well as formalist views that characterize mathematics as a type of game.\n\nIn my view\, to find an explanation for this relationsh ip\, we must first understand the explanandum itself. More fundamental tha n the why-question (why is mathematics applicable in the natural sciences) is the how-question (how is mathematics applicable in the natural science s). By examining how mathematics has been used across different eras and f ields within the natural sciences\, we can begin to understand the relatio nship between mathematics and the sciences. More importantly\, this explor ation allows us to address questions regarding the nature of mathematics a s it is used and practiced. By distinguishing pseudo-problems from the gen uine problems of applicability\, we open new paths for philosophical refle ctions on the nature of mathematics and the sciences.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/153/ END:VEVENT BEGIN:VEVENT SUMMARY:Matthew Akamatsu DTSTART:20241205T170000Z DTEND:20241205T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/156 DESCRIPTION:Title: Collective grassroots knowledge generation with lab dis course graphs\nby Matthew Akamatsu as part of Topos Institute Colloqui um\n\n\nAbstract\nScientific research teams face persistent challenges in coordinating their work and synthesizing collective knowledge into models across projects and labs. Discourse graphs offer a solution by breaking s cientific research into its atomic components - questions\, claims\, and e vidence - and connecting them in a semantic graph. In our cell biology la b\, we have implemented discourse graphs as a coordination layer for colle ctive research and model building. Lab members use the graphs to identify open research questions\, maintain focus on their chosen hypotheses while documenting new results\, and share discrete findings with clear provenan ce and context. Researchers report streamlined thinking\, better orientat ion toward their target question\, and a sense of accomplishment from cont ributing tangible\, reusable results. This collaborative approach has allo wed the lab to organically evolve its scientific models through bottom-up knowledge synthesis. Our new user pilot aims to extend these benefits thr ough accessible tooling and interoperable graphs\, thereby enabling collec tive grassroots knowledge generation and sensemaking across research commu nities.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/156/ END:VEVENT BEGIN:VEVENT SUMMARY:Eswaran Subrahmanian and Yves Keraron DTSTART:20241212T170000Z DTEND:20241212T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/157 DESCRIPTION:Title: Engineering practice and the potential role of CT in sy stems engineering\nby Eswaran Subrahmanian and Yves Keraron as part of Topos Institute Colloquium\n\n\nAbstract\nIn this talk\, we will illustra te the role of information structures in engineering practices. In a parti cular case\, we will instantiate an example of the required structures and their interaction in the systems engineering process. We will then identi fy Categorical representations that could formalize the models embedded in systems engineering standards and support their composition. The talk is not mathematical but an attempt to map the needs of systems engineering mo deling to potential categorical representations that serve the purpose of engineering practices.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/157/ END:VEVENT BEGIN:VEVENT SUMMARY:Nina Otter DTSTART:20250313T170000Z DTEND:20250313T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/158 DESCRIPTION:Title: (Co)algebraic analysis of social systems: from graphs t o hypergraphs\nby Nina Otter as part of Topos Institute Colloquium\n\n \nAbstract\nThe algebraic analysis of social systems\, or algebraic social network analysis\, refers to a collection of methods designed to extract information about the structure of social systems modelled as directed gra phs. Central among these are methods to determine the roles that exist wit hin a given system\, namely compound relations\, and the social positions\ , which one can think of as groups of similarly connected actors. In these methods the focus is on pairwise relationships between social actors\, wh ich are modelled through directed graphs. \nThe importance of higher-order relationships in the modelling of social systems has received considerabl e interest in recent years. In this talk I will explain how we can use the theory of universal coalgebra to formalise these notions for graphs\, gen eralise them to models of social systems that also take into account highe r-order interactions between social actors\, such as hypergraphs\, and fin ally tie together the analyses of social roles and positions through a fun ctoriality result. \n\nThe talk is based on joint work with Nima Motamed a nd Emily Roff.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/158/ END:VEVENT BEGIN:VEVENT SUMMARY:Paul-Andre Mellies DTSTART:20250206T170000Z DTEND:20250206T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/159 DESCRIPTION:Title: The rabbit calculus: convolution products on double cat egories and categorification of rule algebra\nby Paul-Andre Mellies as part of Topos Institute Colloquium\n\n\nAbstract\nReporting on recent joi nt work with Nicolas Behr and Noam Zeilberger\, I will describe the rabbit calculus\, a convolution product over presheaves of double categories mot ivated by term and graph rewriting. As I will explain\, the convolution pr oduct generalizes to any double category the usual Day tensor product of p resheaves of monoidal categories. An interesting aspect of the constructio n is that the resulting convolution product is in general only oplaxl asso ciative. Therefore\, I will identify several classes of double categories for which the convolution product is not only oplax associative\, but full y associative. These include framed bicategories on the one hand\, and dou ble categories of term and graph rewriting on the other. For the latter\, we establish a formula that justifies the view that the convolution produc t categorizes the rule algebra product\, and captures the basic intuitions of causality in rewriting theory.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/159/ END:VEVENT BEGIN:VEVENT SUMMARY:Jason Gross DTSTART:20241024T170000Z DTEND:20241024T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/160 DESCRIPTION:Title: Compact Proofs: Measuring Quality of Understanding with a Compression-Based Metric\nby Jason Gross as part of Topos Institute Colloquium\n\n\nAbstract\nThe field of mechanistic interpretability – t echniques for reverse engineering model weights into human-interpretable a lgorithms – seeks to compress explanations model behavior. By studying t iny transformers trained to perform algorithmic tasks\, we can make rigoro us the extent to which various understandings of a model permit compressin g an explanation of its behavior.\n\nIn this talk\, I’ll discuss how we prototyped this approach in our paper where formally proved lower bounds o n the accuracy of 151 small transformers trained on a Max-of-K task\, crea ting 102 different computer-assisted proof strategies to assess their leng th and tightness of bound on each of our models. Using quantitative metric s\, we found that shorter proofs seem to require and provide more mechanis tic understanding. Moreover\, we found that more faithful mechanistic unde rstanding leads to tighter performance bounds.\n\nWe identified compoundin g structureless noise as the leading obstacle to generating more compact p roofs of tighter performance bounds. I plan to discuss ongoing work to add ress this challenge by either relaxing the worst-case constraint enforced by using proofs\; or by fine-tuning partially-interpreted models to align more closely with our explanations.\n\nI’ll conclude by discussing the r oadmap I see to scaling the compact proofs approach to rigorous mech inter p up to frontier models.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/160/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrew Dudzik DTSTART:20250213T170000Z DTEND:20250213T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/161 DESCRIPTION:Title: Tensor Species: The Theory and Practice of Neural Netwo rks\nby Andrew Dudzik as part of Topos Institute Colloquium\n\n\nAbstr act\nAs category theory grows in popularity within the machine learning co mmunity\, those of us interested in both theory and practice are faced wit h the question: which abstractions are directly useful when innovating in the design of neural networks? We explain why this is a hard problem\, whi le making use of Joyal’s theory of species to give a down-to-earth descr iption of the data types we see in contemporary neural networks\, paying c lose attention to performance.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/161/ END:VEVENT BEGIN:VEVENT SUMMARY:Adrian Miranda DTSTART:20250130T170000Z DTEND:20250130T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/162 DESCRIPTION:Title: Kleisli constructions for pseudomonads\nby Adrian M iranda as part of Topos Institute Colloquium\n\n\nAbstract\nThe passage fr om a monad (A\,S) to its category of algebras (resp. category of free alge bras) can be seen as a V = Cat weighted limit (resp. colimit) construction [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 the two- dimensional setting\, the 2-category of pseudoalgebras can be seen as a V= Gray enriched weighted limit [2]\, but neither of the familiar descriptio ns of the Kleisli category categorify to give a weighted colimit [3]. We g ive a third\, less well-known description of the Kleisli category which do es categorify to the pseudomonad setting to give a weighted colimit. We sh ow that comparisons induced by pseudoadjunctions splitting the pseudomonad are biequivalences if and only if their left pseudoadjoints are biessenti ally surjective on objects. This allows the more familiar Kleisli construc tions for pseudomonads to be seen as tricategorical colimits\, and for the development of the formal theory of pseudomonads pt. 2.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/162/ END:VEVENT BEGIN:VEVENT SUMMARY:B. Scot Rousse DTSTART:20250320T170000Z DTEND:20250320T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/163 DESCRIPTION:Title: Language\, Technology\, & Care\nby B. Scot Rousse a s part of Topos Institute Colloquium\n\n\nAbstract\nThis talk explores "ca re" as a missing dimension in contemporary discussions on technology\, usi ng debates around LLMs and AI alignment as a case study. Our civilization ’s technological prowess is largely identified with abstraction and opti mization—powers that have yielded immense benefits but which have also r eshaped our relationship with reality. Increasingly\, our drive to abstrac t and optimize takes on a life of its own\, leading both technologists and non-technologists alike to engage with the world primarily through questi ons of modeling\, measurement\, and control. But what we care about cannot be appropriately tended to in such an instrumental framework\, for it lac ks a defined ultimate goal\, a why for which we model\, measure\, and cont rol. Our challenge is designing how to pursue technological progress withi n a broader context of care\, not mere "values" that are relative to imper atives of efficiency and optimization.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/163/ END:VEVENT BEGIN:VEVENT SUMMARY:Nathanael Arkor DTSTART:20250403T170000Z DTEND:20250403T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/164 DESCRIPTION:Title: A (virtual) double category theorist's perspective on p olynomials\nby Nathanael Arkor as part of Topos Institute Colloquium\n \n\nAbstract\nI shall tell the tale of how I came to understand polynomial s. In doing so\, I will exhibit a novel universal property of the double c ategory of polynomials in a locally cartesian closed category. In fact\, w e shall see how polynomials may be liberated from the assumption of expone ntiability entirely. This talk is based on joint work with Bryce Clarke.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/164/ END:VEVENT BEGIN:VEVENT SUMMARY:Joe Moeller DTSTART:20250227T170000Z DTEND:20250227T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/165 DESCRIPTION:Title: A categorical approach to Lyapunov stability\nby Jo e Moeller as part of Topos Institute Colloquium\n\n\nAbstract\nIn his 1892 thesis\, Lyapunov developed a method for certifying the stability of an e quilibrium point $x^*$ of a dynamical system without actually having to so lve the differential equations. He showed that if you can construct a func tion $V$ (now called a *Lyapunov function*) on the state space which is bo th positive definite relative to $x^*$ and always decreasing in the direct ion the system is pointing\, then $x^*$ is necessarily (asymptotically) st able. The theory and methodology built on Lyapunov's theorem form the foun dations for modern nonlinear control.\n\nIn this talk\, we present a categ orical framework in which we can develop a generalization of Lyapunov theo ry. This comes in two parts: coalgebras of an endofunctor play the role of dynamical systems in a category\, and internal monoid actions play the ro le of solutions of these systems. We prove a generalization of Lyapunov's theorem in this framework\, namely\, that an equilibrium point of a coalge bra is stable if there is a *Lyapunov morphism*. This generalization allow s us to recover both the classical continuous and discrete time versions o f Lyapunov's theorem\, as well as for dynamics in Lawvere metric spaces an d more generally quantale-enriched categories.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/165/ END:VEVENT BEGIN:VEVENT SUMMARY:Matteo Capucci DTSTART:20250306T170000Z DTEND:20250306T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/166 DESCRIPTION:Title: Representable Behaviour in Double Categorical Systems T heory\nby Matteo Capucci as part of Topos Institute Colloquium\n\n\nAb stract\nCategory theory has a long history of being applied to the study o f general systems. Double Categorical Systems Theory (DCST) condenses many lessons learned along the way regarding compositional structures for the representation of systems\, their behaviour and the interaction of these t wo aspects. In this talk I'll revisit old and new wisdom regarding functor ial behaviour of systems represented by a category of timepieces\, and pro ve old and new compositionality theorems for them.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/166/ END:VEVENT BEGIN:VEVENT SUMMARY:Kate Fleming DTSTART:20250410T170000Z DTEND:20250410T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/167 DESCRIPTION:Title: Beyond Tech Solutionism: Challenges of unlocking under- served community knowledge\nby Kate Fleming as part of Topos Institute Colloquium\n\nAbstract: TBA\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/167/ END:VEVENT BEGIN:VEVENT SUMMARY:Kristine Bauer DTSTART:20250501T170000Z DTEND:20250501T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/168 DESCRIPTION:Title: Distillation systems as models of homotopy colimits \nby Kristine Bauer as part of Topos Institute Colloquium\n\n\nAbstract\nT his is joint work with Kathryn Hess\, Brenda Johnson and Julie Rasmusen.\n \nColimits (and limits) are among the most fundamental notions in category theory\, and also among the most useful of the basic structures. In topol ogy\, colimits are used to “glue” spaces together. However\, problems arise when we try to work with spaces as they continuously deform\, becaus e colimits are not invariant under such deformations. In this case\, one u ses a related notion called a homotopy colimit. But what are these\, reall y? Homotopy colimits do not satisfy a universal property\, even in the hom otopy category\, and are usually defined by the way they are computed in p articular types of categories\, such as model categories. In joint work\, Hess and Johnson identified a list of properties that one would expect hom otopy limits to satisfy in any homotopical category. These properties were chosen carefully because they are needed to perform certain constructions in functor calculus. Building on their work\, we have identified the cate gorical structures that govern these properties. A distillation system rel ates two actions of the category of small categories on the category of ca tegories through a lax linear functor. In this talk\, I will define distil lation systems and explain when they do and don’t recover homotopy colim its.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/168/ END:VEVENT BEGIN:VEVENT SUMMARY:Juergen Jöst DTSTART:20250327T170000Z DTEND:20250327T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/169 DESCRIPTION:Title: Geometric principles of data visualization\nby Juer gen Jöst as part of Topos Institute Colloquium\n\n\nAbstract\nMany machin e 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 soph isticated mathematical tools from Riemannian geometry and category theory. We develop and improve the mathematical theory in a rigorous way\, leadin g to an improved algorithm\, IsUMap. The category theoretical foundations include Spivak's fuzzy simplicial sets\, and they also offer a link to Top ological Data Analysis. They provide a conceptual tool for merging differe nt generalized metric structures\, and we will also put them in a wider co ntext.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/169/ END:VEVENT BEGIN:VEVENT SUMMARY:Robert Brandom DTSTART:20250619T170000Z DTEND:20250619T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/170 DESCRIPTION:Title: Articulating the Structure of Reasons: Logical Expressi vism and Implication-Space Semantics\nby Robert Brandom as part of Top os Institute Colloquium\n\n\nAbstract\nSemantic inferentialism understands the propositional contents expressed by declarative sentences in terms of the role those sentences play in the material relations of implication an d incompatibility that are implicit in practices of offering some sentence s as expressing reasons for or against others. Reason relations in this se nse can be expressed mathematically both proof-theoretically and model-the oretically. Standard versions of these metainferential vocabularies depend on strong structural assumptions about the reason relations they codify\, though. In particular\, specifically logical consequence is monotonic and transitive. However\, those structural conditions incorporated in logical and semantic metavocabularies are not in general satisfied by the implica tion relations appealed to in reasoning outside of broadly mathematical co ntexts. \n\nI present both a sequent-calculus specifications of a version of classical logic and an implication-space model-theoretic specifications of conceptual roles (based on Girard's phase-space semantics for linear l ogic) that is sound and complete for that logic\, which have the expressiv e power to make explicit even radically substructural constellations of re ason relations. A top-down relational approach\, which starts with the goo dness of implications and advances to their ranges of subjunctive robustne ss\, turns out to be much more expressively powerful in substructural cont exts than a bottom-up atomistic approach that begins with truth values of sentences and advances to their truth conditions.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/170/ END:VEVENT BEGIN:VEVENT SUMMARY:Bart Jacobs DTSTART:20250417T170000Z DTEND:20250417T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/172 DESCRIPTION:Title: Update rules of Pearl and Jeffrey\nby Bart Jacobs a s part of Topos Institute Colloquium\n\n\nAbstract\nThis presentation desc ribes the two different rules for probabilistic updating\, associated with Pearl and with Jeffrey. The difference emerges in the presence of updatin g with multiple data items that one wishes to learn from (update with). It will be sketched how Jeffrey's rule is used in a classical algorithm in m achine learning\, namely Expectation Maximisaton.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/172/ END:VEVENT BEGIN:VEVENT SUMMARY:Amar Hadzihasanovic DTSTART:20250508T170000Z DTEND:20250508T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/174 DESCRIPTION:Title: Combinatorial foundation for planar string diagrams \nby Amar Hadzihasanovic as part of Topos Institute Colloquium\n\n\nAbstra ct\nI will explain how diagrammatic sets can serve as a combinatorial and computational foundation for 2-dimensional string diagrams\, alternative t o and as expressive as the topological foundation given by Joyal and Stree t. Since diagrammatic proofs formalised as diagrams in diagrammatic sets c an be interpreted not just in a 2-category or bicategory\, but more genera lly in an (infty\, n)-category\, this is a painless way to extend their ap plicability.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/174/ END:VEVENT BEGIN:VEVENT SUMMARY:Samson Abramsky DTSTART:20250515T170000Z DTEND:20250515T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/175 DESCRIPTION:Title: Duality for complete atomic partial Boolean algebras\nby Samson Abramsky as part of Topos Institute Colloquium\n\n\nAbstract\ nPartial Boolean algebras are an abstraction of projectors on Hilbert spac e ("quantum propositions") introduced by Kochen and Specker in their funda mental work on contextuality and the non-classicality of quantum mechanics .\nRather than the orthomodular lattice structure emphasized in most work on quantum logic\, partial Boolean algebras reflect non-commutativity by p artiality: conjunction is only defined for compatible elements (correspond ing to commuting projectors).\n\nThe classic Stone-type duality results fo r Boolean algebras\, which build dual spaces of points\, do not apply to partial Boolean algebras\, since the import of the Kochen-Specker theorem is precisely that in the cases of greatest interest\, they have no points. \nWe develop a novel duality theory for the case of (complete) atomic Bool ean algebras.\nWhereas the classical Lindenbaum-Tarski duality is between CABA and Set\, we build a duality between pCABA (complete atomic partial B oolean algebras) and a certain category of exclusivity graphs. The total c ase corresponds to the complete graphs\, where the relation is classical a partness (the negation of equality). The morphisms are certain relations b etween these graphs\, again specializing to the usual total case of functi ons.\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 compositio nal quantum logic.\n\n(Joint work with Rui Soares Barbosa)\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/175/ END:VEVENT BEGIN:VEVENT SUMMARY:Daniel Polani DTSTART:20250529T170000Z DTEND:20250529T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/176 DESCRIPTION:Title: Organisation of the Information Flow in the Perception- Action Loop\nby Daniel Polani as part of Topos Institute Colloquium\n\ n\nAbstract\nAgents interact with their environment primarily through thei r perception-action loop. One way to look at this interaction is to consid er it as the exchange of information\, specifically\, Shannon information. In my talk\, I will discuss how that is done\, how this relates to the st ructure of how the agent interacts with their environment (a high-level vi ew of so-called "embodiment") and a number of phenomena that can be unders tood through this perspective. It turns out that the embodiment or agent/e nvironment interaction imposes substantial structure onto the information flow\, in addition to the fundamental structural constraints that determin e the relation between the agent and its environment.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/176/ END:VEVENT BEGIN:VEVENT SUMMARY:Pierre-Louis Curien DTSTART:20250626T170000Z DTEND:20250626T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/177 DESCRIPTION:Title: Opetopic shapes\, combinatorially\nby Pierre-Louis Curien as part of Topos Institute Colloquium\n\n\nAbstract\n(dedicated to the memory of Marek Zawadowski\, both a friend and a very smart scientist) \n\nOpetopes and opetopic sets were introduced by Baez and Dolan at the en d of the previous millenium as a framework for dealing with higher structu res and higher coherences. \nThey are many-to-one shapes in all dimensions and can be represented in different ways:\nabstractly through the iterate d so-called plus or slice construction on polynomial monads\, and more con cretely as zoom complexes (Kock-Joyal-Batanin-Mascari)\, or as some suitab le oriented posets of faces as in the works of Zawadowski. In a series of works\, Louise Leclerc\, and Louise Leclerc and myself have laid down prec ise isomorphisms between these combinatorial presentations\, adding one in the picture: opetopes as epiphytes\, which are recursively defined as tre es whose nodes and edges are decorated with codimension 1 and 2 epiphytes\ , respectively\, and are arguably most faithful to the original abstract s etting. The talk will offer a (gentle) journey through these (quite involv ed) combinatorial descriptions (epiphytes\, zoom complexes\, oriented face structures).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/177/ END:VEVENT BEGIN:VEVENT SUMMARY:Brendan Fong DTSTART:20250710T170000Z DTEND:20250710T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/178 DESCRIPTION:Title: Abstractions for Real People\nby Brendan Fong as pa rt of Topos Institute Colloquium\n\n\nAbstract\nComputing is built on abst ractions. Abstractions forget details\, so that we can focus on what is im portant. What happens\, however\, when we forget something of value? I arg ue that certain risks and fears around AI today result from action informe d by abstractions that diverge from what matters in their context of use. Moreover\, I suggest that building better societal practices of abstractio n is a task to which mathematicians – especially category theorists – are well placed to contribute. To begin a conversation\, I envision a prac tice of abstraction that prizes accessibility\, responsiveness\, and plura lism. I’ll illustrate this practice via ongoing work at Topos\, especial ly our collaborative modelling platform CatColab.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/178/ END:VEVENT BEGIN:VEVENT SUMMARY:Rory Lucyshyn-Wright DTSTART:20250424T170000Z DTEND:20250424T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/179 DESCRIPTION:Title: V-graded categories as a setting for enrichment and act ions of monoidal categories V\nby Rory Lucyshyn-Wright as part of Topo s Institute Colloquium\n\n\nAbstract\nEnriched categories have hom-objects in a monoidal category V\, but their theory is usually formulated under t he assumption that V is biclosed and so is enriched in itself. Categories equipped with an action of V (or V-actegories) provide a related setting w ith the advantage that an arbitrary monoidal category V can always be rega rded as a V-actegory. Richard Wood delineated a setting subsuming both V-e nriched categories and V-actegories by considering V-graded categories\, w hich are categories enriched in a monoidal category of presheaves on V but admit also a direct and elementary definition in terms of a notion of mor phism with an additional parameter in V. Graded categories have also been called procategories (by Kelly-Labella-Schmitt-Street) and locally V-grade d categories (by Levy).\n\nIn this talk\, we introduce V-graded categories and their basic theory\, with an emphasis on how V-graded categories prov ide a foundational setting generalizing V-enrichment for arbitrary monoida l categories V. We also discuss the speaker's recent work that provides a way of defining V-graded functor categories and bifunctors for arbitrary m onoidal categories V\, by involving a notion of bigraded category\, of whi ch V is always an example. This contrasts with the familiar settings of en riched category theory where the use of functor categories and bifunctors demands a symmetry on V\, or more generally a normal duoidal structure on V as studied by Garner and López Franco. We discuss how V-graded modules or profunctors for an arbitrary monoidal category V are examples of graded bifunctors.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/179/ END:VEVENT BEGIN:VEVENT SUMMARY:Dario Stein DTSTART:20250522T170000Z DTEND:20250522T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/180 DESCRIPTION:Title: Random Variables\, Independence Structures and Dagger C ategories of Relations\nby Dario Stein as part of Topos Institute Coll oquium\n\n\nAbstract\nRandom variables are a central notion of probability theory\, but they are defined with reference to an elusive sample space e xisting 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 o ut that sample spaces can be generalized to a wide variety of probability- like phenomena\, such as nondeterminism or fresh name generation. The prob ability sheaf construction hinges on a notion of independence structure wh ere certain squares of sample spaces are distinguished as independent.\n\n I will give a tour of these abstract samples and then discuss the rich int erplay between sample spaces and couplings. These categories determine eac h other in a precise sense\, where couplings behave like relations over sa mple spaces and compose via independent pullback.\n\nJoint work with Chris Heunen\, Matthew Di Meglio and Paolo Perrone\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/180/ END:VEVENT BEGIN:VEVENT SUMMARY:Fosco Loregian DTSTART:20250925T170000Z DTEND:20250925T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/181 DESCRIPTION:Title: A double category of transducers\nby Fosco Loregian as part of Topos Institute Colloquium\n\n\nAbstract\nWe define a bicatego ry 𝟚TDX whose 1-cells provide a categorification of transducers\, compu tational devices extending finite-state automata with output capabilities. This bicategory is a mathematically interesting object: among many equiva lent characterizations\, given an input category 𝒜 and an output catego ry ℬ\, its 1-cells (𝒬\, t) : 𝒜 ⇝ ℬ can be seen as “families of profunctors over 𝒬\, indexed over 𝒜\, and enriched over (a univer sal monoidal category obtained from) ℬ”\; more precisely\, 2-transduce rs are functors of type\n\n  t : 𝒜 × 𝒬ᵒᵖ × 𝒬 × (ℬ* ) ᵒᵖ ⟶ Set\n\nwhere ℬ* denotes the free monoidal category over ℬ. Extending t to 𝒜*\, in the obvious way\, for each “word” 𝑎̲ in 𝒜* we obtain an endoprofunctor over a category 𝒬 of “states” and enriched in presheaves over the free monoidal category ℬ*.\n\nWe discus s a number of other characterizations of 𝟚TDX(𝒜\, ℬ) in detail\; w e establish a Kleisli-like universal property for 𝟚TDX(𝒜\, ℬ) and explore the connection of 𝟚TDX to other bicategories of computational m odels\, such as Walters’ “bicategory of circuits”. It is convenient to regard 𝟚TDX as the loose bicategory of a double category 𝔻TDX\; t he bicategory (resp. double category) of profunctors is naturally containe d in the bicategory (resp. double category) 𝟚TDX (resp. 𝔻TDX)\; we s tudy the completeness and cocompleteness properties of 𝔻TDX\, as well a s monads\, adjunctions\, and other structures/properties that naturally ar ise from the definition.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/181/ END:VEVENT BEGIN:VEVENT SUMMARY:Aleks Kissinger DTSTART:20250703T170000Z DTEND:20250703T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/182 DESCRIPTION:Title: ZX Calculus and Fault-tolerant quantum computing\nb y Aleks Kissinger as part of Topos Institute Colloquium\n\n\nAbstract\nQua ntum computers are highly susceptible to noise due to interactions with en vironment and tiny imperfections in the physical implementations of basic operations like gates and measurements. Fault tolerant quantum computing e ncodes quantum data with some redundancy\, which can be exploited to detec t and correct errors throughout a computation. This is a huge area with ma ny hard problems and fascinating techniques. In this talk\, I will survey some of the ways we have been chipping away at those problems using compos itional ideas\, and in particular the ZX calculus\, a graphical language f or representing and reasoning about quantum computations. I will assume no prior knowledge of quantum computing\, only complex linear algebra and th e tensor product.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/182/ END:VEVENT BEGIN:VEVENT SUMMARY:Kevin Carlson DTSTART:20251002T170000Z DTEND:20251002T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/183 DESCRIPTION:Title: Instances of models of double theories\nby Kevin Ca rlson as part of Topos Institute Colloquium\n\n\nAbstract\nI'll introduce 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 of an ar bitrary double theory $\\mathbb{D}$ (that is\, a lax double functor $\\mat hbb{D}\\to\\mathbb{S}\\mathbf{pan}$) is to its instances. The motivating c ase of the analogy arises precisely when we set $\\mathbb{D}$ to be the te rminal double theory.\n\nThus the theory of instances can be seen as a cha pter of categorical database theory. Beyond the most fundamental case\, in troduced by Spivak and Kent\, of a database schema as a small category $C$ of "types" and "attributes"\, or "tables" and "foreign keys"\, and a data base as a $C$-set\, the concept of instance encompasses such known extensi ons as to Baas\, Fairbanks\, Lynch\, and Patterson's attributed $C$-sets\, as well as to Schultz\, Spivak\, Vasilakopoulou\, and Wisknesky's algebra ic profunctors. From broader motivations\, such structures as multifunctor s from a multicategory to $\\mathbf{Set}$ and models of a Lawvere theory a re also instances of "instances." \n\nI'll describe the category of instan ces of models of simple double theories\, as well\, hopefully\, as introdu cing the story for models of the modal double theories recently introduced into our CatColab tool as our main approach for handling categorical stru ctures including multi-ary operations. I'll aim to explain how quite a lot of the standard theory of $C$-sets generalizes beyond the terminal double theory. For instance\, I'll give a comprehensive factorization system on the category of models of a double theory\, together with a Grothendieck c onstruction giving an equivalence between the category of discrete opfibra tions over a model $X$ and the category of $X$-instances.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/183/ END:VEVENT BEGIN:VEVENT SUMMARY:Mohamed Barakat DTSTART:20250717T170000Z DTEND:20250717T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/184 DESCRIPTION:Title: CAP — a categorical (re)organization of computer alge bra\nby Mohamed Barakat as part of Topos Institute Colloquium\n\n\nAbs tract\nIn this talk I will introduce CAP (Categories\, Algorithms and Prog ramming)\, a multi-package open-development software project for algorihmi c category theory. CAP is currently loosely organized by the 3-category of “doctrines". By a doctrine we mean a 2-category of structured categorie s\, structure-preserving 2-functors\, and natural transformations between them. Compositions of such 2-functors applied to a specific category give rise to what we call "categorical towers"\, a highly economic and modular way to create various computational contexts in computer algebra. Such mod ular code cannot be optimized by hand for comptutational performance as it would require breaking the modularity: Each layer in the tower treats the layer below merely as a blackbox. This forced us to develop CompilerForCA P\, a category-theory-aware compiler that is able to get rid of the entire categorical abstraction and produce efficient low-level code which is alm ost impossible to write by hand\, let alone error-free.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/184/ END:VEVENT BEGIN:VEVENT SUMMARY:Nathaniel Virgo DTSTART:20250904T170000Z DTEND:20250904T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/185 DESCRIPTION:Title: Towards a mathematical theory of intentional systems\nby Nathaniel Virgo as part of Topos Institute Colloquium\n\n\nAbstract\ nWhat does it mean for a system to have "beliefs" and take "actions" in se rvice of "goals"? Philosophy and cognitive science have offered a variety of answers to this question\, including Dennett's intentional stance\, the Bayesian brain hypothesis\, and various forms of 'enactivism'\, among man y others. I will talk about several closely related approaches to telling these stories\, or simplified versions of them\, in a mathematical way. Su rprisingly (to me at least)\, doing so makes them seem much more compatibl e and closely related than they might at first appear.\n\nDennett's core i dea is that the key question to ask about a system is not whether it is an agent or not\, but whether its behaviour can be well described by treatin g it as one. This entails ascribing beliefs and goals to it\, and predicti ng its behaviour by assuming it will take actions that would bring the goa ls about if the beliefs were true. For some systems this yields excellent predictions of their behaviour\, and the behavioural patterns that enable this can be said to be a real property of the system.\n\nMathematically th is 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 problems it can solve. In doing this we are forced to grapple with questions such a s what exactly constitutes a belief\; how should beliefs change over time in response to new information\; what happens if two different belief attr ibutions give rise to the same behaviour\; and where should we draw the bo undary of a system\, if we want to treat it as an agent? Ideas from catego rical systems theory and category-theoretic probability are used throughou t the work.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/185/ END:VEVENT BEGIN:VEVENT SUMMARY:Eric Finster DTSTART:20250911T170000Z DTEND:20250911T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/186 DESCRIPTION:Title: Dependetopes and Higher Generalized Algebraic Theories< /a>\nby Eric Finster as part of Topos Institute Colloquium\n\n\nAbstract\n Many of the classical tools of categorical algebra can be generalized\nto the world of higher algebra\, that is\, the study of algebraic\nstructures on homotopy types. Indeed we can talk about ∞-Lawvere\ntheories\, ∞-f inite limit theories\, classifying ∞-topoi\, ∞-operads and\nso on. Th at we can define and reason about such higher algebraic\ntheories is a res ult of the well-developed theory of (∞\,1)-categories\nof Joyal and Luri e\, and ultimately relies on the tractability of\nworking combinatorially with simplices.\n\nType theorists and computer scientists often work with presentations\nof algebraic theories using dependent types\, so-called "Ge neralized\nAlgebraic Theories"\, exactly because they have convenient synt actic\ndescriptions which lend themselves to computer implementation. We can\ngeneralize the categorical semantics of these theories to the higher\ nsetting using the tools above\, but doing so renders the connection to\nc oncrete syntax somewhat tenuous.\n\nIn this talk I'll introduce a method f or recovering a more syntactic\ndescription of the notion of higher genera lized algebraic theory by\nintroducing the category of dependetopes. The n ame derives from the\nfact that the dependetopes can be understood as a de pendently typed\nextension of Baez-Dolan's notion of opetope which capture s the higher\ngeometry of type-dependency. In addition to their definition \, I will\nexplain how the dependetopes come with a concrete syntax arisin g from\ntype theory\, which can be used to define and manipulate them.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/186/ END:VEVENT BEGIN:VEVENT SUMMARY:Barbara König DTSTART:20251009T170000Z DTEND:20251009T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/187 DESCRIPTION:Title: Behavioural Metrics via Functor Lifting – A Coalgebra ic Approach\nby Barbara König as part of Topos Institute Colloquium\n \n\nAbstract\nBehavioural distances of transition systems modelled via coa lgebras for\nendofunctors generalize traditional notions of behavioural eq uivalence\nto a quantitative setting\, in which states are equipped with a measure\nof how (dis)similar they are. Endowing transition systems with s uch\ndistances essentially relies on the ability to lift functors describi ng\nthe one-step behavior of the transition systems to the category of\nps eudometric spaces. We consider the category theoretic generalization\nof t he Kantorovich/Wasserstein lifting from transportation theory to the\ncase of lifting functors to pseudo-metric spaces. We also consider\ncompositio nality results which are essential ingredients for adapting\nup-to-techniq ues to the case of behavioural distances. Up-to techniques\nare a well-kno wn coinductive technique for efficiently showing lower\nbounds for behavio ural metrics. We illustrate the method with a case\nstudy on probabilistic automata.\n\nThis is joint work with Paolo Baldan\, Filippo Bonchi\, Henn ing Kerstan\,\nDaniela Petrisan\, Keri D'Angelo\, Sebastian Gurke\, Johann a Maria Kirss\,\nMatina Najafi\, Wojciech Rozowski and Paul Wild.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/187/ END:VEVENT BEGIN:VEVENT SUMMARY:Maru Sarazola DTSTART:20250918T170000Z DTEND:20250918T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/188 DESCRIPTION:Title: Double categorical equivalences\nby Maru Sarazola a s part of Topos Institute Colloquium\n\n\nAbstract\nDouble categories are a flexible 2-dimensional setting that allows us to encode two types of mor phisms between objects\, as well as a notion of higher cells. Surprisingly \, unlike most categorical structures\, there is no canonical notion of “equivalence of double categories”\, as it seems that every possible d efinition requires us to make a choice. In this talk we will illustrate th e issue that arises when defining double-categorical equivalences. Then\, we will show how we can use homotopy theory to give a decisive answer as t o who the “canonical double categorical equivalences” should be: the g regarious equivalences introduced by Campbell. In the process\, we will sh ow how to construct a plethora of model structures on double categories wh ose homotopy theories encode different 2-dimensional structures.\n\nBased on work in preparation joint with Lyne Moser and Paula Verdugo.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/188/ END:VEVENT BEGIN:VEVENT SUMMARY:Rune Haugseng DTSTART:20251106T170000Z DTEND:20251106T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/190 DESCRIPTION:Title: Commutative rings\, bispans\, and their equivariant ana logues\nby Rune Haugseng as part of Topos Institute Colloquium\n\n\nAb stract\nCommutative monoids in a category with finite products can be\nide ntified with product-preserving functors from spans of finite\nsets. Simil arly\, we can describe commutative semirings as\nproduct-preserving functo rs from "bispans" (or "polynomial diagrams")\nin finite sets. I will outli ne a proof of this comparison that also\nworks in the ∞-categorical sett ing\, and then discuss its G-equivariant\nanalogue for a finite group G. I n sets\, this amounts to an\nidentification of Tambara functors as G-commu tative algebras in Mackey\nfunctors (first proved by R. Hoyer)\, while in ∞-groupoids it gives a\nconcrete description of "genuine" commutative ri ngs in connective\nG-spectra as homotopy-coherent Tambara functors. This i s joint work\nwith B. Cnossen\, T. Lenz\, and S. Linskens.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/190/ END:VEVENT BEGIN:VEVENT SUMMARY:Alex Kavvos DTSTART:20251113T170000Z DTEND:20251113T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/191 DESCRIPTION:Title: Two-dimensional Kripke Semantics\nby Alex Kavvos as part of Topos Institute Colloquium\n\n\nAbstract\nThe study of modal logi c has witnessed tremendous development following the introduction of Kripk e semantics. However\, recent developments in programming languages and ty pe theory have led to a second way of studying modalities\, namely through their categorical semantics. We show how the two correspond.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/191/ END:VEVENT BEGIN:VEVENT SUMMARY:John Baez DTSTART:20251211T170000Z DTEND:20251211T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/192 DESCRIPTION:Title: Cospans of finite sets\nby John Baez as part of Top os Institute Colloquium\n\n\nAbstract\nCospans of finite sets are the morp hisms in a bicategory\, not really a category\, because composition of cos pans is associative only up to natural isomorphism. How can we characteriz e this bicategory abstractly? There's a category of finite sets and *isomo rphism classes* of cospans. Steve Lack gave a beautiful characterization o f this\, which I will explain\, and Fong and Spivak used this category to clarify the concept of "hypergraph category". But what about the *bicatego ry* of finite sets\, cospans\, and maps between cospans? I will state a gu ess that I haven't proved.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/192/ END:VEVENT BEGIN:VEVENT SUMMARY:Cole Comfort DTSTART:20251016T170000Z DTEND:20251016T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/193 DESCRIPTION:Title: Syntax and semantics for mechanical processes\nby C ole Comfort as part of Topos Institute Colloquium\n\n\nAbstract\nIn this t alk I will review how certain classes of quantum and classical mechanical processes can be represented in terms of affine Lagrangian relations betwe en finite-dimensional vector spaces (the semantics)\; which comes equipped with a ZX-calculus-style graphical language (the syntax). \n\nI will dis cuss how both the syntax and semantics can be extended to more expressive settings: on the one hand with Gaussian probabilistic behaviour\, and on t he other hand with discrete-time-evolution.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/193/ END:VEVENT BEGIN:VEVENT SUMMARY:Xiao-Gang Wen DTSTART:20251023T170000Z DTEND:20251023T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/194 DESCRIPTION:Title: Symmetry beyond group and its description by braided fu sion category\nby Xiao-Gang Wen as part of Topos Institute Colloquium\ n\n\nAbstract\nThe conventional understanding\, which describes symmetry u sing group theory\, is insufficient\, because symmetry can be anomalous\, higher-group\, and/or non-invertible (those symmetries are called algebrai c higher symmetries in the paper). We find that all such finite symmetries - when considered up to holo-equivalence - are precisely classified by to pological orders in one higher dimension (that can host a gappable boundar y). This fundamentally shifts our perspective: symmetry is not inherently about groups\, but is more naturally described by the mathematics of braid ed fusion higher categories.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/194/ END:VEVENT BEGIN:VEVENT SUMMARY:Slim Lim DTSTART:20251204T170000Z DTEND:20251204T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/195 DESCRIPTION:Title: Concrete syntax matters\, actually\nby Slim Lim as part of Topos Institute Colloquium\n\n\nAbstract\nToo many programming lan guages researchers dismiss concrete syntax as an afterthought: arbitrary\, superficial\, or distracting from matters of “actual” (semantic) impo rtance. This received view ignores a critical factor: the human at the com puter. Concrete syntax defines the principal interface through which progr ammers interact with the vast majority of programming languages. Moreover\ , this interface is hardly decoupled from semantics\; even trivial-seeming differences in keywords\, sigils\, and indentation can affect how program mers utilize and reason about language behavior. Using examples from async hronous control flow\, gradual subtyping\, first-class functions\, and mor e\, I will make a case for the importance of concrete syntax\, why languag e designers often overlook it\, and what this implies for those of us who care about the usability of abstractions. Finally\, I will describe some p reliminary work evaluating the role of lexical ambiguity in programmer com prehension of type system features.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/195/ END:VEVENT BEGIN:VEVENT SUMMARY:Terry Winograd DTSTART:20251030T170000Z DTEND:20251030T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/197 DESCRIPTION:Title: What's up with AI?\nby Terry Winograd as part of To pos Institute Colloquium\n\n\nAbstract\nThe current boom in AI has been ac companied by tremendous hype\, both\nnegative and positive. My goal is to go beneath this surface and\nprovide a better understanding of what AI sy stems are actually doing\,\nand what concerns we should have about where t hey are going.\nI am neither a doomer nor a booster. The very real problem s created by AI today\nand in the foreseeable future need to be approached by considering the\nways we (as a society) choose to apply it and the way s 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 language mode ls and\nsimilar systems have no real understanding or intention\, even tho ugh\nthey often promote the illusion that they do. They can still be usef ul\nin many contexts\, as long as we recognize the need for humans to\nalw ays provide the foundation of care.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/197/ END:VEVENT BEGIN:VEVENT SUMMARY:Benjamin Pierce DTSTART:20260226T170000Z DTEND:20260226T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/199 DESCRIPTION:Title: Properties for the People\nby Benjamin Pierce as pa rt of Topos Institute Colloquium\n\n\nAbstract\nProperty-Based Testing (PB T) is a lightweight formal method offering an attractive blend of the abst ract (formal specification) and the concrete (executability). Its populari ty in the functional programming community has grown steadily over the pas t 25 years\, and it is poised to play a key role in the larger software in dustry\, mediating between human programmers and their AI collaborators. I 'll describe a collection of recent advances and remaining challenges in t his space.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/199/ END:VEVENT BEGIN:VEVENT SUMMARY:Marcelo Aguiar DTSTART:20260305T170000Z DTEND:20260305T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/200 DESCRIPTION:Title: The Eckmann-Hilton argument in duoidal categories\n by Marcelo Aguiar as part of Topos Institute Colloquium\n\n\nAbstract\nWe will go over the basics of duoidal categories\, illustrating with a number of examples. As monoidal categories provide a context for monoids\, duoid al categories provide one for duoids and bimonoids. Our main goal is to di scuss a number of versions of the classical Eckmann-Hilton argument which may be formulated in this setting. As an application we will obtain the co mmutativity of the cup product on the cohomology of a bimonoid with coeffi cients in a duoid\, an extension of a familiar result for group and bialge bra cohomology with trivial coefficients.\n\nThe talk borrows on earlier w ork in collaboration with Swapneel Mahajan on the foundations of duoidal c ategories (2010). The main results are from ongoing work with Javier Coppo la. We also rely on work of Richard Garner and Ignacio López-Franco (2016 ).\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/200/ END:VEVENT BEGIN:VEVENT SUMMARY:Jean-Simon Lemay DTSTART:20250612T170000Z DTEND:20250612T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/201 DESCRIPTION:Title: Cartesian Fermat Categories\, a new class of Cartesian Differential Categories\nby Jean-Simon Lemay as part of Topos Institut e Colloquium\n\n\nAbstract\nCartesian differential categories (introduced by Blute\, Cockett\, and Seely) provide a categorical framework for diffe rential calculus\, and also provide the categorical foundations for the di fferential lambda calculus\, differentiable programming\, and certain auto matic differentiation techniques used for machine learning. Another approa ch to the categorical foundations of differentiation are Fermat theories ( introduced by Dubuc and Kock)\, which are Lawvere theories that have Hadam ard’s Lemma as an axiom. It is already known that every Fermat theory is a Cartesian differential category. However\, the definition of a Fermat t heory is heavily dependent on 1) being a Lawvere theory and 2) being able to multiply maps\, which are two things that are not assumed for Cartesian differential categories. In this talk\, we will introduce Cartesian Ferma t categories\, the proper Fermat theory analogue of a Cartesian differenti al category\, with the main result being that Cartesian Fermat category is a Cartesian differential category. This talk will also include a friendly introduction to Cartesian differential categories\, and thus will be acce ssible to anyone\, including newcomers\, interested in differential catego ries.\n\nThis talk is based on joint work with Carlos Pascual Miralles.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/201/ END:VEVENT BEGIN:VEVENT SUMMARY:Dan Ghica DTSTART:20260205T170000Z DTEND:20260205T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/202 DESCRIPTION:Title: Designing and developing an industrial-strength program ming language: Stories from the trenches\nby Dan Ghica as part of Topo s Institute Colloquium\n\n\nAbstract\nFor the last five years I have been working as one of the architects of a new programming language called Cang jie (CJ). CJ is part of a new open-source ecosystem for Huawei devices whi ch has the HarmonyOS operating system at its core. I will discuss some of the innovations adopted by CJ such as effect handlers (released) and modal types (work in progress) and comment on my personal experience as a 'theo ry person' now involved in developing a language for a wide audience\, whi ch includes some of the top Chinese tech companies.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/202/ END:VEVENT BEGIN:VEVENT SUMMARY:Patrick Shafto DTSTART:20260219T170000Z DTEND:20260219T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/203 DESCRIPTION:Title: Autoformalization and the future of math and science\nby Patrick Shafto as part of Topos Institute Colloquium\n\n\nAbstract\n Advances in autoformalization suggest the possibility of automatic transla tion between natural language mathematics and formal verification programm ing languages. We'll chart this recent progress in mathematics. We will co nsider implications for mathematics\, and science more broadly.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/203/ END:VEVENT BEGIN:VEVENT SUMMARY:Paul Levy DTSTART:20260312T170000Z DTEND:20260312T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/204 DESCRIPTION:Title: What is a monoid?\nby Paul Levy as part of Topos In stitute Colloquium\n\n\nAbstract\nIn many situations one encounters an ent ity that resembles a monoid. It consists of a carrier and two operations t hat resemble a unit and a multiplication\, subject to three equations that resemble associativity and left and right unital laws. The question then arises whether this entity is\, in fact\, a monoid in a suitable sense.\n\ nCategory theorists have answered this question by providing a notion of m onoid in a monoidal category\, or more generally in a multicategory. Whil e these encompass many examples\, there remain cases which do not fit into these frameworks\, such as the notion of relative monad\, and the modelli ng of call-by-push-value sequencing. In each of these examples\, the left most and/or the rightmost factor of a multiplication or associativity law seems to be distinguished. \n\nTo include such examples\, we generalize t he multicategorical framework in two stages. \n\nFirstly\, we move to the framework of a left-skew multicategory (due to Bourke and Lack)\, which g eneralizes both multicategory and left-skew monoidal category. The notion of monoid in this framework encompasses examples where only the leftmost factor is distinguished\, such as the notion of relative monad.\n\nSecondl y\, we consider monoids in the novel framework of a bi-skew multicategory. This encompasses examples where both the leftmost and the rightmost fact or are distinguished\, such as the notion of a category on a span\, and th e modelling of call-by-push-value sequencing.\n\nIn the bi-skew framework (which is the most general)\, we give a coherence result saying that a mon oid corresponds to an unbiased monoid\, i.e. a map from the terminal bi-sk ew multicategory.\n\nThis is joint work with Morgan Rogers\, and was prese nted at the POPL 2026 conference. See the paper at https://dl.acm.org/doi /10.1145/3776727\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/204/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrej Bauer DTSTART:20260402T170000Z DTEND:20260402T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/205 DESCRIPTION:Title: Classically laughable theorems\nby Andrej Bauer as part of Topos Institute Colloquium\n\n\nAbstract\nIn intuitionistic mathem atics one encounters theorems that may seem strange\, even laughable\, to a classically trained mathematician. Yet\, interpreted internally in topos es and other non-classical models\, they carry genuine mathematical conten t. For example\, Lawvere’s fixed-point theorem says that if there is a s urjection $A \\to B^A$\, then every endomap on $B$ has a fixed point\; cla ssically the precondition forces $B$ to be a singleton. Likewise\, a state ment that is false in classical set theory can be meaningful internally: i n the effective topos there exists a set that is neither finite nor infini te. In the talk we will try not to laugh\, and instead explain how such cl aims acquire substance once the viewpoint expands beyond classical mathema tics.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/205/ END:VEVENT BEGIN:VEVENT SUMMARY:Robin Piedeleu DTSTART:20260416T170000Z DTEND:20260416T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/206 DESCRIPTION:Title: The Algebra of Probabilistic Boolean Circuits\nby R obin Piedeleu as part of Topos Institute Colloquium\n\n\nAbstract\nBoolean algebra gives us a complete and elegant way to reason algebraically about propositional logic and simple circuits. But what happens when we introdu ce randomness?\nIn this talk\, we will see how to extend Boolean circuits with probabilistic primitives\, obtaining probabilistic Boolean circuits t hat combine logical operations with random choice and conditioning. We wil l formalise these as string diagrams and give them two functorial semantic s: one in terms of (sub)stochastic maps\, and another in which subdistribu tions are identified up to normalisation. We will then present a sound and complete equational theory for each possible interpretation. Time allowin g\, we will also cover the relationship with probabilistic programming and extensions of the diagrammatic calculus to mixtures of Gaussians. \n\nNot e these developments are of interest for the development of probability th eory in Markov categories: our results give a presentation by generators a nd equations of the symmetric monoidal category of stochastic maps (with t he cartesian product as monoidal product) restricted to objects that are p owers of the two-element set.\n\nBased on joint work with Mateo Torres-Rui z\, 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://researchseminars.org/talk/ToposInstituteColloquium/206/ END:VEVENT BEGIN:VEVENT SUMMARY:Chris Heunen DTSTART:20260423T170000Z DTEND:20260423T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/207 DESCRIPTION:Title: Control\, Complete\, Compute: Rig Categories in Quantum Computing\nby Chris Heunen as part of Topos Institute Colloquium\n\nI nteractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=b jdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: 65537\nView-only livestrea m: https://www.youtube.com/live/jiCiuCQQ2Jo\n\nAbstract\nWe present a cate gorical axiomatisation of quantum computation based on free constructions. Starting from a PROP of base circuits\, we introduce a theory of computat ional control given by eight natural equations\, and show that adjoining c ontrol syntactically corresponds semantically to completing the PROP to it s free rig category. Next\, we show that two further generators and three further equations suffice to fully characterise quantum computing. The res ulting free model replaces the usual linear-algebraic semantics with a pur ely symbolic\, combinatorial one. We argue that this gives a conceptually simpler foundation for quantum computing that isolates quantum advantage i n a precise categorical sense. (Based on joint work https://doi.org/10.107 3/pnas.2510881123 and https://arxiv.org/abs/2510.05032 with Robin Kaarsgaa rd\, Louis Lemonnier\, Neil Julien Ross\, Amr Sabry\, and Jacques Carette. )\n LOCATION:https://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:20260423T094652Z UID:ToposInstituteColloquium/208 DESCRIPTION:Title: Combinatory Completeness in Structured Multicategories< /a>\nby Chad Nester as part of Topos Institute Colloquium\n\n\nAbstract\nC ombinatory logic was introduced more than a century ago in pursuit of logi cal syntax without bound variables. Its power and simplicity have made it a subject of enduring interest\, and it has played a foundational role in logic and computer science. A combinatory algebra is an algebraic model of combinatory logic. Concretely\, such an algebra consists of a set equippe d with a binary operation satisfying a condition called combinatory comple teness. This condition is rather complex\, but is equivalent to the existe nce of elements of the carrier set satisfying certain simple equations.\n\ nThis talk concerns a more general notion of combinatory completeness rela tive to a certain well-behaved collections of functions between finite set s\, called faithful Cartesian clubs. The classical notion of combinatory c ompleteness corresponds to the club consisting of all such functions. More over\, the equivalence of combinatory completeness with the existence of e lements satisfying simple equations holds in some form for a number instan ces of the more general notion. These results hold in settings beyond the usual category of sets and functions\, and their technical development tak es place in a multicategory equipped with an action of the faithful Cartes ian club in question. These structured multicategories are a natural setti ng in which to study (variations of) combinatory algebras.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/208/ END:VEVENT BEGIN:VEVENT SUMMARY:Danel Ahman DTSTART:20260409T170000Z DTEND:20260409T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/209 DESCRIPTION:Title: Containers and Comodule Representations of Second-Order Functionals\nby Danel Ahman as part of Topos Institute Colloquium\n\n \nAbstract\nIn information-theoretic terms\, a map is continuous when a fi nite\namount of information about its input suffices for computing a finit e\namount of information about its output. Already Brouwer observed that\n this allows one to represent a continuous functional from sequences to\nnu mbers 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 “re sults” Q b. In this work\, we\nobserve that such tree representations ca n be expressed in purely\ncategory-theoretic terms\, using the notion of r ight T-comodules for\nthe monad T of well-founded trees on the category of containers. A\ntree representation for F is then just a Kleisli map for t he monad T.\n\nDoing so exposes a rich underlying structure\, and immediat ely suggests\ngeneralisations: any right T-comodule for any monad T on con tainers\ngives rise to a corresponding representation theorem for second-o rder\nfunctionals. We give several examples of these\, ranging from finite ly\nsupported functionals\, to functionals that can query their input just \nonce (or sometimes not at all)\, to functionals that can additionally\ni nteract with their environment\, to partial functionals\, to observing\nth at any functional can be trivially represented by itself.\n\nThis is joint work with Andrej Bauer from the University of Ljubljana.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/209/ END:VEVENT BEGIN:VEVENT SUMMARY:Christoph Benzmueller DTSTART:20260507T170000Z DTEND:20260507T180000Z DTSTAMP:20260423T094652Z UID:ToposInstituteColloquium/210 DESCRIPTION:Title: Many Logics\, One Methodology — On the Virtues of Log iKEy in Computational Metaphysics and Ontology\nby Christoph Benzmuell er as part of Topos Institute Colloquium\n\nInteractive livestream: https: //topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz 09\nPassword hint: 65537\n\nAbstract\nThis talk advances the case for logi cal pluralism at the object logic level within a unifying meta-logical fra mework. While modern proof assistant systems often enforce a single founda tional logic — a tendency we may call logical imperialism — such rigid ity impedes the kind of interdisciplinary reuse that robust knowledge repr esentation demands. Our proposed alternative is LogiKEy: a logic-pluralist ic methodology for knowledge representation and reasoning in which object logics are treated as first-class\, analyzable entities\, with applicabili ty across many fields\, including but not limited to computational metaphy sics and ontology.\n\nThe virtues of LogiKEy are illustrated through a con crete case study: Gödel's modal ontological argument and Dana Scott's var iant of it. Supported by experimental studies in a proof assistant system for classical higher-order logic\, we demonstrate how the framework promot es interdisciplinary research and education on logical foundations and phi losophical arguments\, while also yielding new formal insights into these landmark arguments\, and we address some questions accumulated over the pa st decade.\n\nThis is partly joint work with Dana Scott.\n\nReference: Not es on Gödel's and Scott's Variants of the Ontological Argument\, Christop h Benzmüller\, Dana S. Scott · Monatshefte für Mathematik 208\, 569–6 11. Doi: https://doi.org/10.1007/s00605-025-02078-x\n LOCATION:https://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:20260423T094652Z UID:ToposInstituteColloquium/211 DESCRIPTION:Title: Total Functional Programming\, Reloaded\nby Jeremy Gibbons as part of Topos Institute Colloquium\n\nInteractive livestream: h ttps://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ 3pUdz09\nPassword hint: 65537\nView-only livestream: https://www.youtube.c om/live/0WBLvstjZ4I\n\nAbstract\nMathematically structured functional prog ramming presents its practitioners with a dilemma. On the one hand\, it is very appealing to model programs taking typed inputs to typed outputs as total functions between sets. Then standard constructions satisfy simple b ut powerful universal properties\, giving rise to a useful body of laws fo r program calculation\; everything fits neatly together. On the other hand \, this appealing model is too simplistic: it cannot address the possibili ty of non-productive non-termination\, so in particular rules out arbitrar y recursive definitions. Accommodating such extra expressivity entails swi tching the setting from total functions between sets to continuous functio ns between CPOs\; many of the laws are weakened\, or complicated through s trictness side-conditions. Ideally we would work in an intermediate settin g\, encompassing well-founded generative recursion (such as divide-and-con quer algorithms and the hylomorphism pattern) while still excluding ill-fo unded general recursion. What is the right path towards this ideal world? I have been exploring this question while writing my forthcoming book Patt erns in Functional Programming. I don't have any answers\, but I do have s ome options\, suggestions\, and challenges.\n LOCATION:https://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:20260423T094652Z 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://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:20260423T094652Z UID:ToposInstituteColloquium/213 DESCRIPTION:Title: BV-Categories and Higher-Order Quantum Theory\nby J ames Hefford as part of Topos Institute Colloquium\n\n\nAbstract\nBV-logic is an extension of multiplicative linear logic which adds an additional n on-commutative connective representing sequential composition. BV-categori es have been suggested as potential models of this logic and I will show h ow they arise as pseudomonoids in a bicategory of *-autonomous categories while discussing their relation to self-dual duoidal categories. This allo ws us to lift the Chu construction to this setting and use it to cofreely construct many examples of BV-categories. One notable application is to mo dels of higher-order quantum theory\, quantum supermaps and indefinite cau sal orders and I will discuss how these structures can be modelled by pass ing to the strong Hyland envelope of a category.\n\nThis is joint work wit h Matt Wilson\, based on https://dl.acm.org/doi/abs/10.1145/3661814.366212 3 and https://arxiv.org/abs/2502.19022.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/213/ END:VEVENT BEGIN:VEVENT SUMMARY:Simon Willerton DTSTART:20260514T170000Z DTEND:20260514T180000Z DTSTAMP:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z UID:ToposInstituteColloquium/217 DESCRIPTION:Title: The category of schemes is abelian (and other obviously -false true things)\nby Inna Zakharevich as part of Topos Institute Co lloquium\n\nAbstract: TBA\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/217/ END:VEVENT BEGIN:VEVENT SUMMARY:Richard Blute DTSTART:20260618T170000Z DTEND:20260618T180000Z DTSTAMP:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://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:20260423T094652Z 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://researchseminars.org/talk/ToposInstituteColloquium/231/ URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT dGhvZ3pUdz09 END:VEVENT END:VCALENDAR