BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:David Spivak
DTSTART;VALUE=DATE-TIME:20210204T170000Z
DTEND;VALUE=DATE-TIME:20210204T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210211T210000Z
DTEND;VALUE=DATE-TIME:20210211T220000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210218T170000Z
DTEND;VALUE=DATE-TIME:20210218T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210311T170000Z
DTEND;VALUE=DATE-TIME:20210311T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210325T180000Z
DTEND;VALUE=DATE-TIME:20210325T190000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210401T170000Z
DTEND;VALUE=DATE-TIME:20210401T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210408T170000Z
DTEND;VALUE=DATE-TIME:20210408T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210506T170000Z
DTEND;VALUE=DATE-TIME:20210506T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210513T170000Z
DTEND;VALUE=DATE-TIME:20210513T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210520T170000Z
DTEND;VALUE=DATE-TIME:20210520T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210527T170000Z
DTEND;VALUE=DATE-TIME:20210527T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210603T170000Z
DTEND;VALUE=DATE-TIME:20210603T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210624T180000Z
DTEND;VALUE=DATE-TIME:20210624T190000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210415T170000Z
DTEND;VALUE=DATE-TIME:20210415T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210617T170000Z
DTEND;VALUE=DATE-TIME:20210617T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210422T170000Z
DTEND;VALUE=DATE-TIME:20210422T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210708T170000Z
DTEND;VALUE=DATE-TIME:20210708T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210722T170000Z
DTEND;VALUE=DATE-TIME:20210722T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210729T220000Z
DTEND;VALUE=DATE-TIME:20210729T230000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210610T170000Z
DTEND;VALUE=DATE-TIME:20210610T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210429T170000Z
DTEND;VALUE=DATE-TIME:20210429T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210805T170000Z
DTEND;VALUE=DATE-TIME:20210805T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210930T150000Z
DTEND;VALUE=DATE-TIME:20210930T160000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210909T170000Z
DTEND;VALUE=DATE-TIME:20210909T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210923T170000Z
DTEND;VALUE=DATE-TIME:20210923T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210701T170000Z
DTEND;VALUE=DATE-TIME:20210701T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210916T170000Z
DTEND;VALUE=DATE-TIME:20210916T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210819T170000Z
DTEND;VALUE=DATE-TIME:20210819T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20211007T150000Z
DTEND;VALUE=DATE-TIME:20211007T160000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20211014T170000Z
DTEND;VALUE=DATE-TIME:20211014T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20211021T170000Z
DTEND;VALUE=DATE-TIME:20211021T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20211028T170000Z
DTEND;VALUE=DATE-TIME:20211028T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210812T170000Z
DTEND;VALUE=DATE-TIME:20210812T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210826T170000Z
DTEND;VALUE=DATE-TIME:20210826T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20211202T170000Z
DTEND;VALUE=DATE-TIME:20211202T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20211209T170000Z
DTEND;VALUE=DATE-TIME:20211209T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20211118T170000Z
DTEND;VALUE=DATE-TIME:20211118T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20210902T170000Z
DTEND;VALUE=DATE-TIME:20210902T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20211104T180000Z
DTEND;VALUE=DATE-TIME:20211104T190000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220217T170000Z
DTEND;VALUE=DATE-TIME:20220217T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220224T170000Z
DTEND;VALUE=DATE-TIME:20220224T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220331T170000Z
DTEND;VALUE=DATE-TIME:20220331T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220602T170000Z
DTEND;VALUE=DATE-TIME:20220602T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220317T170000Z
DTEND;VALUE=DATE-TIME:20220317T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220407T170000Z
DTEND;VALUE=DATE-TIME:20220407T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220526T170000Z
DTEND;VALUE=DATE-TIME:20220526T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220324T200000Z
DTEND;VALUE=DATE-TIME:20220324T210000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220303T170000Z
DTEND;VALUE=DATE-TIME:20220303T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220414T170000Z
DTEND;VALUE=DATE-TIME:20220414T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220519T170000Z
DTEND;VALUE=DATE-TIME:20220519T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220623T170000Z
DTEND;VALUE=DATE-TIME:20220623T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220609T170000Z
DTEND;VALUE=DATE-TIME:20220609T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220428T170000Z
DTEND;VALUE=DATE-TIME:20220428T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220616T170000Z
DTEND;VALUE=DATE-TIME:20220616T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220512T170000Z
DTEND;VALUE=DATE-TIME:20220512T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220505T170000Z
DTEND;VALUE=DATE-TIME:20220505T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220915T170000Z
DTEND;VALUE=DATE-TIME:20220915T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220630T170000Z
DTEND;VALUE=DATE-TIME:20220630T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221013T170000Z
DTEND;VALUE=DATE-TIME:20221013T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220825T170000Z
DTEND;VALUE=DATE-TIME:20220825T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221006T170000Z
DTEND;VALUE=DATE-TIME:20221006T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221027T160000Z
DTEND;VALUE=DATE-TIME:20221027T170000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220908T170000Z
DTEND;VALUE=DATE-TIME:20220908T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220922T170000Z
DTEND;VALUE=DATE-TIME:20220922T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220901T170000Z
DTEND;VALUE=DATE-TIME:20220901T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220707T170000Z
DTEND;VALUE=DATE-TIME:20220707T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20220929T170000Z
DTEND;VALUE=DATE-TIME:20220929T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221110T170000Z
DTEND;VALUE=DATE-TIME:20221110T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221201T170000Z
DTEND;VALUE=DATE-TIME:20221201T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221020T170000Z
DTEND;VALUE=DATE-TIME:20221020T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221103T170000Z
DTEND;VALUE=DATE-TIME:20221103T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221215T170000Z
DTEND;VALUE=DATE-TIME:20221215T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20221208T170000Z
DTEND;VALUE=DATE-TIME:20221208T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230202T170000Z
DTEND;VALUE=DATE-TIME:20230202T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230209T170000Z
DTEND;VALUE=DATE-TIME:20230209T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230216T170000Z
DTEND;VALUE=DATE-TIME:20230216T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230302T170000Z
DTEND;VALUE=DATE-TIME:20230302T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230413T170000Z
DTEND;VALUE=DATE-TIME:20230413T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230309T170000Z
DTEND;VALUE=DATE-TIME:20230309T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230323T170000Z
DTEND;VALUE=DATE-TIME:20230323T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230330T170000Z
DTEND;VALUE=DATE-TIME:20230330T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230420T170000Z
DTEND;VALUE=DATE-TIME:20230420T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230427T170000Z
DTEND;VALUE=DATE-TIME:20230427T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230504T170000Z
DTEND;VALUE=DATE-TIME:20230504T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230316T170000Z
DTEND;VALUE=DATE-TIME:20230316T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230511T170000Z
DTEND;VALUE=DATE-TIME:20230511T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230525T170000Z
DTEND;VALUE=DATE-TIME:20230525T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230608T170000Z
DTEND;VALUE=DATE-TIME:20230608T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230615T170000Z
DTEND;VALUE=DATE-TIME:20230615T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230518T170000Z
DTEND;VALUE=DATE-TIME:20230518T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230601T170000Z
DTEND;VALUE=DATE-TIME:20230601T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230622T170000Z
DTEND;VALUE=DATE-TIME:20230622T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230629T170000Z
DTEND;VALUE=DATE-TIME:20230629T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230824T170000Z
DTEND;VALUE=DATE-TIME:20230824T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230928T170000Z
DTEND;VALUE=DATE-TIME:20230928T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230831T170000Z
DTEND;VALUE=DATE-TIME:20230831T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20231102T170000Z
DTEND;VALUE=DATE-TIME:20231102T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20231019T170000Z
DTEND;VALUE=DATE-TIME:20231019T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20231207T170000Z
DTEND;VALUE=DATE-TIME:20231207T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230907T170000Z
DTEND;VALUE=DATE-TIME:20230907T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20231012T170000Z
DTEND;VALUE=DATE-TIME:20231012T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20230921T170000Z
DTEND;VALUE=DATE-TIME:20230921T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20231026T170000Z
DTEND;VALUE=DATE-TIME:20231026T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20231116T170000Z
DTEND;VALUE=DATE-TIME:20231116T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240118T170000Z
DTEND;VALUE=DATE-TIME:20240118T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20231130T170000Z
DTEND;VALUE=DATE-TIME:20231130T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240208T170000Z
DTEND;VALUE=DATE-TIME:20240208T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240125T170000Z
DTEND;VALUE=DATE-TIME:20240125T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20231214T170000Z
DTEND;VALUE=DATE-TIME:20231214T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240111T170000Z
DTEND;VALUE=DATE-TIME:20240111T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240215T170000Z
DTEND;VALUE=DATE-TIME:20240215T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240222T170000Z
DTEND;VALUE=DATE-TIME:20240222T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240328T170000Z
DTEND;VALUE=DATE-TIME:20240328T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240404T170000Z
DTEND;VALUE=DATE-TIME:20240404T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240815T170000Z
DTEND;VALUE=DATE-TIME:20240815T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240425T170000Z
DTEND;VALUE=DATE-TIME:20240425T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240627T170000Z
DTEND;VALUE=DATE-TIME:20240627T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240523T170000Z
DTEND;VALUE=DATE-TIME:20240523T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240905T170000Z
DTEND;VALUE=DATE-TIME:20240905T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240509T170000Z
DTEND;VALUE=DATE-TIME:20240509T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240822T170000Z
DTEND;VALUE=DATE-TIME:20240822T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240516T170000Z
DTEND;VALUE=DATE-TIME:20240516T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240418T170000Z
DTEND;VALUE=DATE-TIME:20240418T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240530T170000Z
DTEND;VALUE=DATE-TIME:20240530T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240606T170000Z
DTEND;VALUE=DATE-TIME:20240606T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240801T170000Z
DTEND;VALUE=DATE-TIME:20240801T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240502T170000Z
DTEND;VALUE=DATE-TIME:20240502T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240613T170000Z
DTEND;VALUE=DATE-TIME:20240613T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240829T170000Z
DTEND;VALUE=DATE-TIME:20240829T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240926T170000Z
DTEND;VALUE=DATE-TIME:20240926T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240808T170000Z
DTEND;VALUE=DATE-TIME:20240808T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240711T170000Z
DTEND;VALUE=DATE-TIME:20240711T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20241003T170000Z
DTEND;VALUE=DATE-TIME:20241003T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20241016T170000Z
DTEND;VALUE=DATE-TIME:20241016T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
UID:ToposInstituteColloquium/146
DESCRIPTION:Title: Quantitative results for stochastic processes\nby T
homas Powell as part of Topos Institute Colloquium\n\nInteractive livestre
am: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\n\nAbstract\nIt is an el
ementary fact from real analysis that any monotone bounded sequence of rea
l numbers converges. It turns out that the monotone convergence theorem ca
n be given an equivalent finitary formulation: roughly that any sufficient
ly long monotone bounded sequence experiences long regions where the seque
nce is metastable. This so-called "finite convergence principle" is carefu
lly motivated and discussed by Terence Tao in a 2007 blog post ('Soft anal
ysis\, hard analysis\, and the finite convergence principle')\, but was al
ready known to proof theorists\, where the use of logical methods to both
finitize infinitary statements and provide uniform quantitative informatio
n for the finitary versions plays a central role in the so-called proof mi
ning program.\n\nThe goal of my talk is to discuss how methods from proof
mining can be applied to the theory of stochastic processes\, an area of m
athematics hitherto unexplored from this perspective. I will begin by disc
ussing the simple monotone convergence principle\, and will then focus on
how everything I mentioned above can be generalised to the analogous resul
t in the stochastic setting: Doob's martingale convergence theorems. This
then sets the groundwork for new applications of proof theory in stochasti
c optimization\, and I will give a high level overview of some work in pro
gress in this direction\, including a quantitative analysis of the famous
Robbins-Siegmund lemma. This is all joint work with my PhD student Morenik
eji Neri.\n\nIn giving the talk I will not assume any knowledge of proof t
heory\, just some elementary analysis and probability theory.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/146/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christine Tasson
DTSTART;VALUE=DATE-TIME:20240912T170000Z
DTEND;VALUE=DATE-TIME:20240912T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20240919T170000Z
DTEND;VALUE=DATE-TIME:20240919T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
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;VALUE=DATE-TIME:20241031T170000Z
DTEND;VALUE=DATE-TIME:20241031T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
UID:ToposInstituteColloquium/151
DESCRIPTION:Title: Partial Markov Categories\nby Mario Román as part
of Topos Institute Colloquium\n\nInteractive livestream: https://topos-ins
titute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPasswor
d hint: the 5th Fermat prime\n\nAbstract\nPartial Markov categories are an
algebra and syntax for Bayesian inference. They use a string diagrammatic
syntax—with a formal correspondence to programs—to reason about conti
nuous and discrete probability\, decision problems (Monty Hall\, Newcomb's
)\, the compositional properties of normalization\, and an abstract Bayes'
theorem.\n\nPartial Markov categories are a careful blend of Markov categ
ories (from categorical probability theory) and cartesian restriction cate
gories (from the algebraic theory of partial computations). We will discus
s the construction\, theory\, and applications of partial Markov categorie
s.\n\nThis is joint work with Elena Di Lavore. It is based on "Evidential
Decision Theory via Partial Markov Categories"\, presented at LiCS'23 (htt
ps://arxiv.org/abs/2301.12989).\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/151/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Carl Miller
DTSTART;VALUE=DATE-TIME:20241107T170000Z
DTEND;VALUE=DATE-TIME:20241107T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
UID:ToposInstituteColloquium/152
DESCRIPTION:by Carl Miller as part of Topos Institute Colloquium\n\nIntera
ctive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS0
9wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstract:
TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/152/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Arezoo Islami
DTSTART;VALUE=DATE-TIME:20241114T170000Z
DTEND;VALUE=DATE-TIME:20241114T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
UID:ToposInstituteColloquium/153
DESCRIPTION:by Arezoo Islami as part of Topos Institute Colloquium\n\nInte
ractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdV
S09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstrac
t: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/153/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew Dudzik
DTSTART;VALUE=DATE-TIME:20241121T170000Z
DTEND;VALUE=DATE-TIME:20241121T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
UID:ToposInstituteColloquium/155
DESCRIPTION:by Andrew Dudzik as part of Topos Institute Colloquium\n\nInte
ractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdV
S09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstrac
t: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/155/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Matthew Akamatsu
DTSTART;VALUE=DATE-TIME:20241205T170000Z
DTEND;VALUE=DATE-TIME:20241205T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
UID:ToposInstituteColloquium/156
DESCRIPTION:by Matthew Akamatsu as part of Topos Institute Colloquium\n\nI
nteractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=b
jdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbst
ract: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/156/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Eswaran Subrahmanian
DTSTART;VALUE=DATE-TIME:20241212T170000Z
DTEND;VALUE=DATE-TIME:20241212T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
UID:ToposInstituteColloquium/157
DESCRIPTION:by Eswaran Subrahmanian as part of Topos Institute Colloquium\
n\nInteractive livestream: https://topos-institute.zoom.us/j/84392523736?p
wd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\n
Abstract: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/157/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nina Otter
DTSTART;VALUE=DATE-TIME:20250313T170000Z
DTEND;VALUE=DATE-TIME:20250313T180000Z
DTSTAMP;VALUE=DATE-TIME:20241013T140106Z
UID:ToposInstituteColloquium/158
DESCRIPTION:by Nina Otter as part of Topos Institute Colloquium\n\nInterac
tive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09
wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstract:
TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/158/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
END:VCALENDAR