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:20240803T044943Z
UID:ToposInstituteColloquium/1
DESCRIPTION:Title: Poly: a category of remarkable abundance\nby D
avid Spivak as part of Topos Institute Colloquium\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Richard Garner
DTSTART;VALUE=DATE-TIME:20210211T210000Z
DTEND;VALUE=DATE-TIME:20210211T220000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/2
DESCRIPTION:Title: Comodels of an algebraic theory\nby Richard Ga
rner as part of Topos Institute Colloquium\n\n\nAbstract\nIn 1991 Eugenio
Moggi introduced the monadic approach to computational effects\; this is t
he mechanism by which purely functional programming languages such as Hask
ell can express computations with side-effects such as output\, input\, or
interaction with an external store.\n\nAround 2000\, Plotkin and Power re
fined the Moggi perspective by looking not at monads\, but the equational
algebraic theories which generate them: this amounts to specifying not jus
t a kind of side-effect\, but a set of primitive operations by which one c
an program with these side-effects.\n\nAlgebraic theories have models\, no
t only in the category of sets\, but also in any category with finite prod
ucts. In particular\, one can look at comodels of a theory: a model in the
opposite of the category of sets. A crucial insight of Power and Shkaravs
ka is that\, if T is a theory encoding interaction with an environment\, t
hen a T-comodel is a state machine providing an instance of the environmen
t with which T interacts.\n\nThe objective of this talk is to explain this
history\, and to prove a new result: the category of comodels of any alge
braic theory T is a presheaf category [B\,Set]\, where B is a small catego
ry\, which can be computed explicitly\, that encodes the static and dynami
c properties of the side-effects encoded by T.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gunnar E. Carlsson
DTSTART;VALUE=DATE-TIME:20210218T170000Z
DTEND;VALUE=DATE-TIME:20210218T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/3
DESCRIPTION:Title: Relative topology\, motion planning\, and coverage
problems\nby Gunnar E. Carlsson as part of Topos Institute Colloquium
\n\n\nAbstract\nAlgebraic topology produces invariants that capture aspect
s of the shape of a space\, or in the case of topological data analysis. A
lthough these invariants are in general quite rich\, they are somewhat spa
rse in low dimensions. On the other hand\, it is possible to consider comm
a categories of spaces\, for example the category of spaces with reference
to a fixed base space and morphisms respecting the reference map. When on
e does this\, one obtains a much richer set of invariants. I will discuss
how to apply this kind of construction in the setting of evasion problems
for sensor nets and more general motion planning problems.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Samson Abramsky
DTSTART;VALUE=DATE-TIME:20210311T170000Z
DTEND;VALUE=DATE-TIME:20210311T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/4
DESCRIPTION:Title: The logic of contextuality\nby Samson Abramsky
as part of Topos Institute Colloquium\n\n\nAbstract\n(joint work with Rui
Soares Barbosa)\n\nContextuality is a key signature of quantum non-classi
cality\, which has been shown to play a central role in enabling quantum a
dvantage for a wide range of information-processing and computational task
s.\nWe study the logic of contextuality from a structural point of view\,
in the setting of partial Boolean algebras introduced by Kochen and Specke
r in their seminal work.\nThese contrast with traditional quantum logic a
la Birkhoff--von Neumann\nin that operations such as conjunction and disju
nction are partial\, only being defined in the domain where they are physi
cally meaningful.\n\nWe study how this setting relates to current work on
contextuality such as the sheaf-theoretic and graph-theoretic approaches.\
nWe introduce a general free construction extending the commeasurability r
elation on a partial Boolean algebra\, i.e. the domain of definition of th
e binary logical operations.\nThis construction has a surprisingly broad r
ange of uses.\nWe apply it in the study of a number of issues\, including:
\n\n- establishing the connection between the abstract measurement scenari
os studied in the contextuality literature and the setting of partial Bool
ean algebras\;\n\n- formulating various contextuality properties in this s
etting\, including probabilistic contextuality as well as the strong\, sta
te-independent notion of contextuality given by Kochen--Specker paradoxes\
, which are logically contradictory statements validated by partial Boolea
n algebras\, specifically those arising from quantum mechanics\;\n\n- inve
stigating a Logical Exclusivity Principle\, and its relation to the Probab
ilistic Exclusivity Principle widely studied in recent work on contextuali
ty\nas a step towards closing in on the set of quantum-realisable correlat
ions\;\n\n- developing some work towards a logical characterisation of the
Hilbert space tensor product\, using logical exclusivity to capture some
of its salient quantum features.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Baez
DTSTART;VALUE=DATE-TIME:20210325T180000Z
DTEND;VALUE=DATE-TIME:20210325T190000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/5
DESCRIPTION:Title: Mathematics in the 21st century\nby John Baez
as part of Topos Institute Colloquium\n\n\nAbstract\nThe climate crisis is
part of a bigger transformation in which humanity realizes that the Earth
is a finite system and that no physical quantity can grow exponentially f
orever. This transformation may affect mathematics — and be affected by
it — just as dramatically as the agricultural and industrial revolutions
did. After a review of the problems\, we discuss how mathematicians can h
elp make this transformation a bit easier\, and some ways in which mathema
tics may change.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dan Christensen
DTSTART;VALUE=DATE-TIME:20210401T170000Z
DTEND;VALUE=DATE-TIME:20210401T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/6
DESCRIPTION:Title: Reasoning in an ∞-topos with homotopy type theor
y\nby Dan Christensen as part of Topos Institute Colloquium\n\n\nAbstr
act\nThis talk will be an introduction to homotopy type theory that will
explain how it can be used to prove theorems that hold in any ∞-topos.
I will introduce the basic ideas of type theory and give some intuition f
or what these mean homotopically. I will end by giving examples of resu
lts proved in homotopy type theory that tell us new results in any ∞-to
pos. No prior knowledge of type theory or ∞-category theory will be a
ssumed.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joachim Kock
DTSTART;VALUE=DATE-TIME:20210408T170000Z
DTEND;VALUE=DATE-TIME:20210408T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/7
DESCRIPTION:Title: Noncrossing hyperchords and free probability\n
by Joachim Kock as part of Topos Institute Colloquium\n\n\nAbstract\nFree
probability is a noncommutative probability theory introduced by Voiculesc
u in the 1980s\, motivated by operator algebras and free groups\, and usef
ul in random matrix theory. Where classical independence relates to the te
nsor product of algebras\, free independence relates to the free product o
f algebras. Speicher discovered the combinatorial substrate of the theory:
noncrossing partitions. He derived the free cumulant-moment relations fro
m Möbius inversion in the incidence algebra of the lattice of noncrossing
partitions\, and used it\, via two reduction procedures\, to model free m
ultiplicative convolution. A crucial ingredient\, which has no analogue in
the classical setting\, is the notion of Kreweras complement of a noncros
sing partition. In this talk\, after a long introduction to these topics\,
I will explain some more categorical viewpoints. A first step is an opera
d of noncrossing partitions. A second step is a decomposition space (2-Seg
al space) Y of noncrossing hyperchords\, whose simplicial structure encode
s higher versions of Kreweras complementation. The incidence bialgebra of
Y is a direct combinatorial model for free multiplicative convolution. It
is related to the previous models by the standard simplicial notion of dec
alage: the first decalage of Y gives the (two-sided bar construction of th
e) operad\, and the second decalage gives the lattice. These two decalages
encode precisely Speicher's two reductions.\n\nThis is joint work with Ku
rusch Ebrahimi-Fard\, Loïc Foissy\, and Frédéric Patras.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Emily Riehl
DTSTART;VALUE=DATE-TIME:20210506T170000Z
DTEND;VALUE=DATE-TIME:20210506T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/8
DESCRIPTION:Title: Contractibility as uniqueness\nby Emily Riehl
as part of Topos Institute Colloquium\n\n\nAbstract\nWhat does it mean for
something to exist uniquely? Classically\, to say that a set A has a uniq
ue element means that there is an element x of A and any other element y o
f A equals x. When this assertion is applied to a space A\, instead of a m
ere set\, and interpreted in a continuous fashion\, it encodes the stateme
nt that the space A is contractible\, i.e.\, that A is continuously deform
able to a point. This talk will explore this notion of contractibility as
uniqueness and its role in generalizing from ordinary categories to infini
te-dimensional categories.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maria Emilia Maietti
DTSTART;VALUE=DATE-TIME:20210513T170000Z
DTEND;VALUE=DATE-TIME:20210513T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/9
DESCRIPTION:Title: Quotient completions for topos-like structures
\nby Maria Emilia Maietti as part of Topos Institute Colloquium\n\n\nAbstr
act\nIn this talk we report fundamental results concerning free completion
s with quotients of specific Lawvere doctrines for building toposes\, quas
i-toposes and predicative versions of them. Our final goal is to use such
completions for modelling foundations of constructive and classical mathem
atics which are predicative in the sense of Poincaré\, Weyl and Feferman\
, including that in [M09]. We first recall how the tool of completing an e
lementary existential Lawvere doctrine with exact quotients is the fundame
ntal construction behind the tripos-to-topos construction in [HJP80] besid
e including as instances both the exact completion of a regular category a
nd that of a weakly lex finite product category\, as reported in [MR15]. W
e then describe recent work with Fabio Pasquali and Pino Rosolini where we
show how the elementary quotient completion of an elementary Lawvere doct
rine in [MR13] is the fundamental construction behind a tripos-to-quasi-to
pos construction including toposes as exact completions of a left exact ca
tegory in [Me03] as instances. We also mention a joint work with Davide Tr
otta where we extend results in [MPR17] about tripos-to-topos construction
s coinciding with exact completions of a left exact category. We end by a
pplying the elementary quotient completion to build examples of predicati
ve toposes including the Effective Predicative Topos in [MM21].\n\nReferen
ces\n\n[HJP80] J.M. Hyland\, P. T. Johnstone and A.M.Pitts. Tripos theory.
Math. Proc. Cambridge Philos. Soc. 88\, 205-232\, 1980\n\n[M09] M.E. Maie
tti. A minimalist two-level foundation for constructive mathematics. Annal
s of Pure and Applied Logic\, 160(3): 319-354\, 2009\n\n[MR13] M.E. Maiett
i and G. Rosolini. Elementary quotient completion. Theory and Applications
of Categories\, 27(17): 445–463\, 2013\n\n[MR15 ] M.E. Maietti and G. R
osolini. Unifying Exact Completions. Applied Categorical Structures 23(1):
43-52\, 2015\n\n[MPR17] M.E. Maietti\, F. Pasquali and G. Rosolini. Tripo
ses\, exact completions\, and Hilbert's ε-operator. Tbilisi Mathematical
Journal. 10(3): 141-66\, 2017\n\n[Me03] M. Menni. A characterization of th
e left exact categories whose exact completions are toposes. Journal of Pu
re and Applied Algebra\, 3(177): 287-301\, 2003\n\n[MM21] M.E. Maietti\, S
. Maschio. A predicative variant of Hyland's Effective Topos. To appear in
The Journal of Symbolic Logic\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tobias Fritz
DTSTART;VALUE=DATE-TIME:20210520T170000Z
DTEND;VALUE=DATE-TIME:20210520T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/10
DESCRIPTION:Title: The law of large numbers in categorical probabili
ty\nby Tobias Fritz as part of Topos Institute Colloquium\n\n\nAbstrac
t\nThe law of large numbers (in its various guises) can be regarded as the
most central result of probability theory\, and any serious axiomatic sys
tem for probability must reproduce it in some form. After a general introd
uction to categorical probability in terms of Markov categories\, I will e
xplain how to formulate a form of the strong law of large numbers within t
his framework\, namely the Glivenko-Cantelli theorem on the convergence of
the empirical distribution. I will also sketch how to use this statement
in order to derive other laws of large numbers from it.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michael Shulman
DTSTART;VALUE=DATE-TIME:20210527T170000Z
DTEND;VALUE=DATE-TIME:20210527T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/11
DESCRIPTION:Title: Two-dimensional semantics of homotopy type theory
\nby Michael Shulman as part of Topos Institute Colloquium\n\n\nAbstra
ct\nThe general higher-categorical semantics of homotopy type theory invol
ves (∞\,1)-toposes and Quillen model categories. However\, for many appl
ications it suffices to consider (2\,1)-toposes\, which are reasonably con
crete categorical objects built out of ordinary groupoids. In this talk I
'll describe how to interpret homotopy type theory in (2\,1)-toposes\, and
some of the applications we can get from\nsuch an interpretation. I will
assume a little exposure to type theory\, as in Dan Christensen's talk fro
m April\, but no experience with higher toposes or homotopy theory. This t
alk will also serve as an introduction to some basic notions of Quillen mo
del categories\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Steve Awodey
DTSTART;VALUE=DATE-TIME:20210603T170000Z
DTEND;VALUE=DATE-TIME:20210603T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/12
DESCRIPTION:Title: Model Structures from Models of HoTT\nby Stev
e Awodey as part of Topos Institute Colloquium\n\n\nAbstract\nHomotopical
models of Martin-Löf type theory often make use of the notion of a Quille
n model category\, even if only implicitly. From the interpretation of id
entities between terms as paths in an abstract space\, to the univalence p
rinciple identifying identities of types with homotopy equivalences of spa
ces\, the standard tools of abstract homotopy theory provide the means to
make rigorous the basic intuition behind the homotopical interpretation of
the formal logical system. \nSo good is this kind of model that it turns
out to be possible to invert the process\, in a certain sense\; given a c
ategorical model of HoTT of an appropriate kind\, one can construct from i
t a full Quillen model structure on the underlying category. This can be
seen as a further strengthening of the idea of HoTT as the internal langua
ge of an $\\infty$-topos.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kathryn Hess
DTSTART;VALUE=DATE-TIME:20210624T180000Z
DTEND;VALUE=DATE-TIME:20210624T190000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/13
DESCRIPTION:Title: From comonads to calculus\nby Kathryn Hess as
part of Topos Institute Colloquium\n\n\nAbstract\nAbstracting the framewo
rk common to most flavors of functor calculus\, one can define a calculus
on a category M equipped with a distinguished class of weak equivalences t
o be a functor that associates to each object x of M a tower of objects in
M that are increasingly good approximations to x\, in some well defined\,
Taylor-type sense. Such calculi could be applied\, for example\, to test
ing whether morphisms in M are weak equivalences.\n\nIn this talk\, after
making the definition above precise\, I will describe a machine for creati
ng calculi on functor categories Fun (C\,M) that is natural in both the so
urce C and the target M. Our calculi arise by comparison of the source cat
egory C with a tower of test categories\, equipped with cubical structure
of progressively higher dimension\, giving rise to sequences of resolution
s of functors from C to M\, built from comonads derived from the cubical s
tructure on the test categories. The stages of the towers of functors tha
t we obtain measure how far the functor we are analyzing deviates from bei
ng a coalgebra over each of these comonads. The naturality of this constr
uction makes it possible to compare both different types calculi on the sa
me functor category\, arising from different towers of test categories\,
and the same type of calculus on different functor categories\, given by a
fixed tower of test categories.\n\n(Joint work with Brenda Johnson)\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Asgar Jamneshan
DTSTART;VALUE=DATE-TIME:20210415T170000Z
DTEND;VALUE=DATE-TIME:20210415T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/14
DESCRIPTION:Title: Topos theory and measurability\nby Asgar Jamn
eshan as part of Topos Institute Colloquium\n\n\nAbstract\nIn point-free (
or abstract) measure theory measurable spaces are replaced by $\\sigma$-co
mplete Boolean algebras\, measurable functions by Boolean homomorphisms\,
and measure spaces by measure algebras. This more general perspective has
some advantages over the traditional pointwise approach to measure theory.
For example\, it facilitates the use of topos-theoretic techniques to stu
dy measurability. To this effect\, a translation process between the inter
nal language/ logic of certain Boolean topoi and the "usual" external lang
uage/ logic is required which we can accomplish by using the formalism of
conditional analysis. We illustrate this with some recent applications in
ergodic theory.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chris Heunen
DTSTART;VALUE=DATE-TIME:20210617T170000Z
DTEND;VALUE=DATE-TIME:20210617T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/15
DESCRIPTION:Title: Sheaf representation of monoidal categories\n
by Chris Heunen as part of Topos Institute Colloquium\n\n\nAbstract\nWould
n't it be great if monoidal categories were nice and easy? They are! We wi
ll discuss how a monoidal category embeds into a "nice" one\, and how a "n
ice" monoidal category consists of global sections of a sheaf of "easy" mo
noidal categories. This theorem cleanly separates "spatial" and "temporal"
directions of monoidal categories.\n\nMore precisely\, "nice" means that
certain morphisms into the tensor unit have joins that are respected by te
nsor products\, namely those morphisms that are central and idempotent wit
h respect to the tensor product. By "easy" we mean that the topological sp
ace of which these central idempotents form the opens is a lot like a sing
leton space\, namely local.\n\nCategorifying flabby sheaves in the appropr
iate way makes the representation functorial from monoidal categories to s
chemes of local monoidal categories. The representation respects many prop
erties of monoidal categories: if a monoidal category is closed/traced/com
plete/Boolean\, then so are its local stalks. As instances we recover the
Lambek-Moerdijk-Awodey sheaf representation for toposes\, the Stone repres
entation of Boolean algebras\, the representation by germs of open subsets
of a topological space\, and the Takahashi representation of Hilbert modu
les as continuous fields of Hilbert spaces.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Shaowei Lin
DTSTART;VALUE=DATE-TIME:20210422T170000Z
DTEND;VALUE=DATE-TIME:20210422T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/16
DESCRIPTION:Title: Proofs as programs: challenges and strategies for
program synthesis\nby Shaowei Lin as part of Topos Institute Colloqui
um\n\n\nAbstract\nThe Curry-Howard correspondence between proofs and progr
ams suggests that we can exploit proof assistants for writing software. I
will discuss the challenges behind a naïve execution of this idea\, and s
ome preliminary strategies for overcoming them. As an example\, we will or
ganize higher-order information in knowledge graphs using dependent type t
heory\, and automate the answering of queries using a proof assistant. In
another example\, we will explore how decentralized proof assistants can e
nable mathematicians or programmers to work collaboratively on a theorem o
r application. If time permits\, I will outline connections to canonical s
tructures (ssreflect)\, reflection (ssreflect)\, transport\, unification a
nd universe management.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Geoffrey Cruttwell
DTSTART;VALUE=DATE-TIME:20210708T170000Z
DTEND;VALUE=DATE-TIME:20210708T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/17
DESCRIPTION:Title: Categorical differential structures and their rol
e in abstract machine learning\nby Geoffrey Cruttwell as part of Topos
Institute Colloquium\n\n\nAbstract\nA fundamental component of many machi
ne learning algorithms is differentiation. Thus\, if one wishes to abstra
ct and generalize aspects of machine learning\, it is useful to have an ab
stract perspective on differentiation. There has been much work on catego
rical differential structures in the past few years with the advent of dif
ferential categories\, Cartesian differential categories\, and tangent cat
egories. In this talk I'll focus on Cartesian reverse differential catego
ries\, a recent variant of Cartesian differential categories\, and touch o
n how they can be used in abstract machine learning.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Walter P Tholen
DTSTART;VALUE=DATE-TIME:20210722T170000Z
DTEND;VALUE=DATE-TIME:20210722T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/18
DESCRIPTION:Title: What is monoidal topology?\nby Walter P Thole
n as part of Topos Institute Colloquium\n\n\nAbstract\nMonoidal topology m
ay be seen as being inspired by some visionary remarks in Hausdorff‘s
„Grundzüge der Mengenlehre“ of 1914\, and it takes its modern lead fr
om two distinct seminal contributions of the early 1970s: the Manes-Barr p
resentation of topological spaces in terms of ultrafilter convergence axio
ms\, and Lawvere’s presentation of metric spaces as small categories enr
iched in the extended non-negative half-line of the reals. Both types of s
paces become instances of small so-called (T\,V)-categories\, where T is a
Set-monad and V a (commutative) quantale\, i.e. a small\, thin and (symme
tric) monoidal-closed category. The setting therefore allows for a general
study of „spaces“ that combines geometric and numerical aspects in a
natural way.\n\nIn this talk we present some key elements of the theory an
d its applications\, showing in particular how the strictification and inv
ersion of some naturally occurring inequalities in this lax-monoidal sett
ing leads to interesting topological properties and unexpected connections
. Time permitting\, we will also point to some on-going and future work in
the area.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Marcy Robertson
DTSTART;VALUE=DATE-TIME:20210729T220000Z
DTEND;VALUE=DATE-TIME:20210729T230000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/19
DESCRIPTION:Title: Topological Inspiration for Infinity Modular Oper
ads\nby Marcy Robertson as part of Topos Institute Colloquium\n\n\nAbs
tract\nA modular operad can be thought of as an undirected network which a
llows for feedback “loops”. An infinity modular operad is such a netwo
rk where operations can be continuously varied with respect to time. The
goal of this talk is to give a gentle introduction to a Segal model for in
finity modular operads\, focusing on the topological origins of the idea.
The audience is not expected to be familiar with operads or topology. This
talk will cover snippets of joint work with Luci Bonatto\, Pedro Boavida\
, Philip Hackney \, Geoffroy Horel and Donald Yau.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Eugene Lerman
DTSTART;VALUE=DATE-TIME:20210610T170000Z
DTEND;VALUE=DATE-TIME:20210610T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/20
DESCRIPTION:Title: A category of hybrid systems\nby Eugene Lerma
n as part of Topos Institute Colloquium\n\n\nAbstract\nHybrid systems are
dynamical systems that exhibit both continuous time evolution and abrupt t
ransitions. Examples include mechanical systems (e.g.\, a ball bouncing of
f a floor) and cyber-physical systems (e.g.\, a room with a thermostat). D
efinitions of a hybrid dynamical systems vary widely in literature but the
y usually include directed graphs\, spaces with vector fields attached to
the nodes of graphs and partial maps or\, more generally\, relations attac
hed to the edges of graphs. The vector fields are used to model continuous
evolution and the relations the abrupt transitions.\n\nI wanted to unders
tand if analogues of coupled cell networks of Golubitsky\, Stewart and the
ir collaborators (these are highly structured coupled systems of ODEs) mak
e sense for hybrid dynamical systems. In order to do that I needed to mak
e sense of open hybrid systems\, their interconnection\, networks of hybri
d systems and maps between networks of hybrid systems.\n\nProceeding by an
alogy with continuous time systems I introduced the notion of a hybrid pha
se space and its underlying manifold. A hybrid phase space can be succinc
tly defined as double functor. Hybrid phase spaces form a category HyPh
with morphisms coming from vertical natural transformations. A hybrid dyna
mical system is a pair (A\,X) where A is a hybrid phase space and X is a v
ector field on the manifold U(A) underlying A. I then constructed a catego
ry HyDS of hybrid dynamical system. The definition of HyDS passes a couple
of sanity checks.\n\nUsing the foundation laid out above James Schmidt an
d I showed that one can also define hybrid surjective submersions\, hybri
d open systems\, their interconnections and networks of hybrid systems. T
his way one can model systems of bouncing balls and several interconnected
rooms with separate thermostats.\n\nReferences: arXiv:1612.01950 [math.DS
] and arXiv:1908.10447 [math.DS] (DOI: 10.1016/j.geomphys.2019.103582).\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jonathan Gorard
DTSTART;VALUE=DATE-TIME:20210429T170000Z
DTEND;VALUE=DATE-TIME:20210429T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/21
DESCRIPTION:Title: Fast Diagrammatic Reasoning and Compositional App
roaches to Fundamental Physics\nby Jonathan Gorard as part of Topos In
stitute Colloquium\n\n\nAbstract\nThe Wolfram Model — a discrete spaceti
me model based upon hypergraph rewriting — can be naively formalized as
a conventional double-pushout rewriting system over a partial adhesive cat
egory of (directed) hypergraphs. However\, the abstract rewriting structur
e of the model also permits an elegant interpretation in terms of dagger c
ompact categories\, with considerable formal analogies to FdHilb and the f
oundations of categorical quantum mechanics\, yet with an additional causa
l semantics definable in terms of a second symmetric strict partial monoid
al structure (such that the entire system can be formalized\, for instance
\, in terms of a double category or a weak 2-category). In addition to pot
entially defining a general categorical semantics for discrete models of q
uantum gravity\, this formalism presents a fundamentally new approach to p
erforming efficient diagrammatic reasoning over combinatorial structures\,
by suggesting various generalizations of the standard deductive inference
rules of resolution\, superposition\, paramodulation and factoring in the
Knuth-Bendix completion approach to automated theorem-proving\, and by ma
king more explicit use of the causal structure of the abstract rewriting s
ystem in the choice of which inference rules to apply. We show how this ap
proach can be applied to the problem of enacting fast diagrammatic simplif
ication of circuits in quantum information theory\, as well as (time-permi
tting) the problem of efficiently discretizing the Cauchy problem in numer
ical general relativity\, showcasing comparisons against some existing sof
tware frameworks and algorithms.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Todd Trimble
DTSTART;VALUE=DATE-TIME:20210805T170000Z
DTEND;VALUE=DATE-TIME:20210805T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/22
DESCRIPTION:Title: From 2-rigs to lambda-rings\nby Todd Trimble
as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk will summar
ize some aspects of recent work with John Baez and Joe Moeller\, which aim
s to tie together representations of symmetric groups\, Schur functors\, a
nd lambda rings from the point of view of 2-rigs\, which are a categorific
ation of ordinary 'rigs' or rings without negatives. A common theme in thi
s area is the notion of 'plethory'. We sketch how the archetypal plethory
of lambda rings arises simply and naturally from the simplest possible '2-
plethory'\, and applying decategorification to it.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pawel Sobocinski
DTSTART;VALUE=DATE-TIME:20210930T150000Z
DTEND;VALUE=DATE-TIME:20210930T160000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/23
DESCRIPTION:Title: Algebraic theories with string diagrams\nby P
awel Sobocinski as part of Topos Institute Colloquium\n\n\nAbstract\nIn La
wvere theories the central role is played by categories with finite produc
ts. The free category with finite products on one object (FinSet^op) is th
e Lawvere theory of the empty algebraic theory\, and the free category wit
h finite products on a signature (of an algebraic theory) has a concrete d
escription as a category of classical syntactic terms. But\, using a theor
em due to Thomas Fox\, we can also capture these categories nicely using s
tring diagrams.\n\nThe string diagrammatic approach gets you further than
ordinary syntax. In a POPL 21 paper with Ivan Di Liberti\, Fosco Loregian
and Chad Nester\, we developed a Lawvere-style approach to algebraic theor
ies with partially defined operations. It turns out that in this setting\,
instead of categories with finite products\, the relevant concept is disc
rete cartesian restriction categories (dcrc). And string diagrams are the
right syntax for this setting: they let us describe the free dcrc on an ob
ject and the free dcrc on a signature. I will sketch some of our results a
nd talk about some of the ramifications\, including a string diagrammatic
description of categories with free finite limits.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Bourke
DTSTART;VALUE=DATE-TIME:20210909T170000Z
DTEND;VALUE=DATE-TIME:20210909T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/24
DESCRIPTION:Title: Tensor products\, multimaps and internal homs
\nby John Bourke as part of Topos Institute Colloquium\n\n\nAbstract\nThe
notions of monoidal category\, multicategory and closed category are close
ly related\, with each having their own advantages. Considering the relat
ionship between them leads naturally to skew variants — skew monoidal ca
tegories\, skew multicategories and skew closed categories — and I will
explore some of these variants in this talk.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew J. Blumberg
DTSTART;VALUE=DATE-TIME:20210923T170000Z
DTEND;VALUE=DATE-TIME:20210923T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/25
DESCRIPTION:Title: Abstract homotopy theory for topological data ana
lysis\nby Andrew J. Blumberg as part of Topos Institute Colloquium\n\n
\nAbstract\nA starting point for the modern perspective on algebraic topol
ogy is the Eilenberg-Steenrod axioms characterizing homology theories. Mo
re generally\, there has been a great deal of work starting from insights
of Verdier\, Quillen\, and Dwyer-Kan that gives abstract characterizations
of the structures of homotopy theory in terms of formal cylinder and susp
ension objects or mapping spaces. This talk will be about efforts to unde
rstand the invariants of topological data analysis from an abstract perspe
ctive. There will be many more questions than answers.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lawrence Paulson
DTSTART;VALUE=DATE-TIME:20210701T170000Z
DTEND;VALUE=DATE-TIME:20210701T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/26
DESCRIPTION:Title: Formalising Contemporary Mathematics in Simple Ty
pe Theory\nby Lawrence Paulson as part of Topos Institute Colloquium\n
\n\nAbstract\nA long-standing question in mathematics is the relevance of
formalisation to practice. Rising awareness of fallibility among mathemati
cians suggests formalisation as a remedy. But are today's proof assistants
up to the task? And what is the right formalism?\n\nA wide variety of mat
hematical topics have been formalised in simple type theory using Isabelle
/HOL. The partition calculus was introduced by Erdös and R. Rado in 1956
as the study of “analogues and extensions of Ramsey’s theorem”. High
ly technical results were obtained by Erdös-Milner\, Specker and Larson (
among many others) for the case of ordinal partition relations\, which is
concerned with countable ordinals and order types. Much of this material w
as formalised last year (with the assistance of Džamonja and Koutsoukou-A
rgyraki). \n\nGrothendieck's Schemes have also been formalised in Isabelle
/HOL. This achievement is notable because some prominent figures had conje
ctured that schemes were beyond the reach of simple type theory.\n\nSome h
ighlights of this work will be presented along with general observations a
bout role of type theory in the formalisation of mathematics.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jamie Vicary
DTSTART;VALUE=DATE-TIME:20210916T170000Z
DTEND;VALUE=DATE-TIME:20210916T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/27
DESCRIPTION:Title: Understanding free infinity-categories\nby Ja
mie Vicary as part of Topos Institute Colloquium\n\n\nAbstract\nInfinity-c
ategories have a reputation for being difficult algebraic objects to defin
e and work with. In this talk I will present a new definition of free infi
nity-category that demystifies them\, and makes them easy to understand fr
om an algebraic perspective. The definition is given as a sequence of indu
ctive-recursive data structures\, and we explore how this relates to Groth
endieck's original ideas on infinity-categories. No knowledge of infinity-
categories is required to follow this talk!\n\nThis is joint work with Chr
istopher Dean\, Eric Finster\, Ioannis Markakis and David Reutter.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Valeria de Paiva
DTSTART;VALUE=DATE-TIME:20210819T170000Z
DTEND;VALUE=DATE-TIME:20210819T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/28
DESCRIPTION:Title: Categorical Explicit Substitutions\nby Valeri
a de Paiva as part of Topos Institute Colloquium\n\n\nAbstract\nThe advant
ages of functional programming are well-known: programs are easier to writ
e\, understand and verify than their imperative counterparts. However\, fu
nctional languages tend to be more memory intensive and these problems hav
e hindered their wider use in industry. The xSLAM project tried to address
these issues by using *explicit substitutions* to construct and implement
more efficient abstract machines\, proved correct by construction.\n\nIn
this talk I recap two results from the xSLAM project which haven't been su
fficiently discussed. First\, we provided categorical models for the calcu
li of explicit substitutions (linear and cartesian) that we are interested
in. No one else seems to have provided categorical models for explicit su
bstitutions calculi\, despite the large number of explicit substitutions s
ystems available in the literature. Indexed categories provide models of
cartesian calculi of explicit substitutions. However\, these structures ar
e inherently non-linear and hence cannot be used to model *linear* calculi
of explicit substitutions. Our work replaces indexed categories with pre
-sheaves\, thus providing a categorical semantics covering both the linear
and cartesian cases. Our models satisfy soundness and completeness\, as e
xpected. \n\nSecondly\, we recall a different linear-non-linear type theor
y\, built from Barber and Plotkin DILL ideas\, which\, like DILL\, is bett
er for implementations. Unlike DILL\, this type theory\, called ILT\, sat
isfies an internal language theorem. Thus we describe ILT\, show categoric
al semantics for it and sketch the proof of its internal language theorem
\, thus justifying its use in implementations. These results are examples
of `(categorically) structured deep syntax'\, to borrow Hyland's characte
rization.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anders Mortberg
DTSTART;VALUE=DATE-TIME:20211007T150000Z
DTEND;VALUE=DATE-TIME:20211007T160000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/29
DESCRIPTION:Title: Cubical Methods in Homotopy Type Theory and Univa
lent Foundations\nby Anders Mortberg as part of Topos Institute Colloq
uium\n\n\nAbstract\nOne of the aims of Homotopy Type Theory and Univalent
Foundations (HoTT/UF) is to provide a practical foundation for computer fo
rmalization of mathematics by building on deep connections between type th
eory\, homotopy theory and (higher) category theory. Some of the key inven
tions of HoTT/UF include Voevodsky's univalence axiom relating equality an
d equivalence of types\, the internal stratification of types by the compl
exity of their equality\, as well as higher inductive types which allow sy
nthetic reasoning about spaces in type theory. In order to provide computa
tional support for these notions various cubical type theories have been i
nvented. In particular\, the Agda proof assistant now has a cubical mode w
hich makes it possible to work and compute directly with the concepts of H
oTT/UF. In the talk I will discuss some of the mathematical ideas which mo
tivate these developments\, as well as show examples of how computer mecha
nization of mathematics looks like in Cubical Agda. I will not assume expe
rt knowledge of HoTT/UF and key concepts will be introduced throughout the
talk.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andreas Blass
DTSTART;VALUE=DATE-TIME:20211014T170000Z
DTEND;VALUE=DATE-TIME:20211014T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/30
DESCRIPTION:Title: A topos view of axioms of choice for finite sets<
/a>\nby Andreas Blass as part of Topos Institute Colloquium\n\n\nAbstract\
nTarski proved (in set theory without choice) that if one assumes that\nal
l families of 2-element sets have choice functions then one can\nprove tha
t all families of 4-element sets have choice functions.\nMostowski (1937)
investigated similar implications\, giving\nnumber-theoretic and group-the
oretic conditions\, some necessary and\nsome sufficient for such implicati
ons. But some questions remained\nunsolved\, in particular: Do choice fro
m 3-element sets\, from 5-element\nsets\, and from 13-element sets togethe
r imply choice from 15-element\nsets. Gauntt (1970) resolved those remain
ing questions\, using\ngroup-theoretic criteria. I plan to describe some
of this work and to\nexplain what it has to do with topos theory.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chris Kapulkin
DTSTART;VALUE=DATE-TIME:20211021T170000Z
DTEND;VALUE=DATE-TIME:20211021T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/31
DESCRIPTION:Title: Cubical setting for Discrete Homotopy Theory\
nby Chris Kapulkin as part of Topos Institute Colloquium\n\n\nAbstract\nDi
screte homotopy theory\, developed by H. Barcelo and collaborators\, is a
homotopy theory of (simple) graphs. Homotopy invariants of graphs have fou
nd numerous applications\, for instance\, in the theory of matroids\, hype
rplane arrangements\, and time series analysis. Discrete homotopy theory i
s also a special instance of a homotopy theory of simplicial complexes\, d
eveloped by R. Atkin\, to study social and technological networks.\n\nIn t
he talk\, I will introduce the main concepts and open problems of discrete
homotopy theory. I will also report on the joint work with D. Carranza on
developing a new foundation for discrete homotopy theory in the category
of cubical sets\, which offers solutions to a number of long standing open
problems in the field.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dorette Pronk
DTSTART;VALUE=DATE-TIME:20211028T170000Z
DTEND;VALUE=DATE-TIME:20211028T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/32
DESCRIPTION:Title: Doubly Lax Colimit of Double Categories with Appl
ications\nby Dorette Pronk as part of Topos Institute Colloquium\n\n\n
Abstract\nThus far\, lax and oplax pseudo colimits of double categories ha
ve been considered in two flavours [2]: horizontally lax and vertically la
x\, based on the notions of horizontal and vertical transformations (respe
ctively) between double functors. Also\, the diagrams of double categories
have typically been indexed by a 2-category.\n\nIn this work we introduce
diagrams indexed by a double category\; in order to make sense of this we
will map into a version of the quintets of the category of double categor
ies\, because this category itself is only enirched in double categories a
nd is often taken as a 2-category. Between the new indexing functors we in
troduce a new notion of transformation\, namely doubly lax transformation.
We then introduce a double categorical version of the Grothendieck constr
uction and show that it has a universal property as doubly lax colimit of
the diagram\; i.e.\, a colimit that is lax with respect to the new transfo
rmations.\n\nAs applications we obtain:\n\n— a universal property as lax
colimit for the Grothendieck construction for bicategories described in [
1]\;\n\n— a universal property for the elements construction for double
categories\;\n\n— a notion of fibration for double categories\, differen
t from the internal one described by Street and others\;\n\n— a double c
ategorical generalization of the classical tom Dieck fundamental groupoid
for a space with an action by a topological group.\n\nThis is joint work w
ith Marzieh Bayeh (University of Ottawa) and Martin Szyld (Dalhousie Unive
rsity).\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kevin Buzzard
DTSTART;VALUE=DATE-TIME:20210812T170000Z
DTEND;VALUE=DATE-TIME:20210812T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/33
DESCRIPTION:Title: What is the point of Lean's maths library?\nb
y Kevin Buzzard as part of Topos Institute Colloquium\n\n\nAbstract\nLean
is a computer proof checker developed by Microsoft Research. Over the last
four years I have been part of a team of mathematicians and computer scie
ntists who have got it into their heads that it is somehow "obviously" a g
ood idea to build a formally verified library of modern mathematics in Lea
n. You can think of it as a 21st century Bourbaki if you like\, although o
ur plans are actually far grander than Bourbaki's. I will talk about two t
hings: (1) how it's going and (2) why we're doing it. No background in com
puter proof checkers will be necessary to follow the talk.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Conor McBride
DTSTART;VALUE=DATE-TIME:20210826T170000Z
DTEND;VALUE=DATE-TIME:20210826T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/34
DESCRIPTION:Title: Cats and Types: Best Friends?\nby Conor McBri
de as part of Topos Institute Colloquium\n\n\nAbstract\nIntensional Type T
heory and Category Theory ought to fit well together\, but the current pra
ctical experience of representing concepts from one with the tools of the
other is often quite strained. On the one hand\, fibrational approaches to
dependency often seem heavy. On the other hand\, definitional equality in
type systems often falls way short of delivering even the simplest of coh
erences. In this talk\, I shall reflect on the problems and search for opp
ortunities. What has to change to make type theoretic proof assistants a g
ood medium for categorical approaches to programming and proof? I wish I k
new the answer to that question! I can at least offer a few clues. For exa
mple\, I shall exhibit a universe of indexed inductively defined datatypes
which exhibit nontrivial presheaf structure by construction.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Evan Patterson
DTSTART;VALUE=DATE-TIME:20211202T170000Z
DTEND;VALUE=DATE-TIME:20211202T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/35
DESCRIPTION:Title: Categories of diagrams in data migration and comp
utational physics\nby Evan Patterson as part of Topos Institute Colloq
uium\n\n\nAbstract\nDiagrams are among the most fundamental and ubiquitous
concepts of category theory. Less appreciated are the several notions of
morphism between diagrams in a category. After reviewing the resulting cat
egories of diagrams\, this talk will explain their central role in two rec
ent projects by the author and collaborators. First\, due to their close c
onnections with limits and colimits\, the categories of diagrams provide a
natural syntax for defining flexible data migrations between categorical
databases. We describe a prototype implementation of this system in Catlab
.jl. In the second part of the talk\, we explain how "Tonti diagrams\," di
agrammatic presentations of physics equations expressed in vector calculus
or exterior calculus\, can be formalized using category-theoretic diagram
s. When combined with a suitable discretization scheme\, such as the discr
ete exterior calculus (DEC)\, the result is a diagrammatic and composition
al approach to building numerical simulators of physical systems.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robert Harper
DTSTART;VALUE=DATE-TIME:20211209T170000Z
DTEND;VALUE=DATE-TIME:20211209T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/36
DESCRIPTION:Title: Phase Distinctions in Type Theory\nby Robert
Harper as part of Topos Institute Colloquium\n\n\nAbstract\n(Joint work wi
th Jon Sterling and Yue Niu)\n\nThe informal phase distinction between com
pile-time and run-time in programming languages is formally manifested by
the distinction between kinds\, which classify types\, and types\, which c
lassify code. The distinction underpins standard programming methodology w
hereby code is first type-checked for consistency before being compiled fo
r execution. When used effectively\, types help eliminate bugs before they
occur.\n\nProgram modules\, in even the most rudimentary form\, threaten
the distinction\, comprising as they do both types and programs in a singl
e unit. Matters worsen when considerating "open" modules\, with free modul
e variables standing for its imports. To maintain the separation in their
presence it is necessary to limit the dependency of types\, the static par
ts of a module\, to their imported types. Such restrictions are fundamenta
l for using dependent types to express modular structure\, as originally s
uggested by MacQueen.\n\nTo address this question Moggi gave an "analytic"
formulation of program modules in which modules are explicitly separated
into their static and dynamic components using tools from category theory.
Recent work by Dreyer\, Rossberg\, and Russo develops this approach fully
in their account of ML-like module systems. In this talk we consider inst
ead a "synthetic" formulation using a proposition to segregate the static
from the dynamic\, in particular to define static equivalence to manage ty
pe sharing and type dependency\n\nRobert Harper is a Professor of Computer
Science at Carnegie Mellon\, where he\nhas been a member of faculty since
1988. He is past recipient of the Allen\nNewell Award for research excell
ence and the Herbert Simon Award for teaching\nexcellence. He is author of
Practical Foundations for Programming Languages\, a\ntextbook account of
programming language theory. His work focuses on the\napplication of type
theory to program development\, language design\, compiler\nconstruction\
, and mechanized proof.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paolo Perrone
DTSTART;VALUE=DATE-TIME:20211118T170000Z
DTEND;VALUE=DATE-TIME:20211118T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/37
DESCRIPTION:Title: The rise of quantitative category theory\nby
Paolo Perrone as part of Topos Institute Colloquium\n\n\nAbstract\nIn seve
ral domains of applications\, category theory can be useful to add concept
ual clarity and scalability to mathematical models.\nHowever\, ordinary ca
tegories often fail to grasp some quantitative aspects: the total cost of
a certain strategy\, the number of composite steps\, the discrepancy betwe
en a concrete construction and its ideal model\, and so on.\n\nIn order to
incorporate these aspects\, it is helpful to switch to a "quantitative" v
ersion of categories: weighted categories. These are particular enriched c
ategories where each arrow carries a number\, or "weight"\, as in a weight
ed graph. The composition of paths comes with a triangle inequality\, anal
ogous to the one of metrics and norms\, which equips universal properties
with quantitative bounds. Most results in category theory have a weighted
analogue\, which often carries additional geometric or analytic significan
ce.\nWeighted categories have been around since early work of Lawvere\, bu
t only in the last few years researchers are starting to recognize their i
mportance. More and more recent papers are using them in fields as diverse
as topological data analysis\, geometry\, and probability theory\, some t
imes even rediscovering the concepts independently.\n\nIn this talk we are
going to see what it's like to work with weighted categories\, their rela
tionship with graphs\, and the quantitative aspects about limits and colim
its. We will also define a weighted analogue of lenses\, and use it to exp
ress liftings of transport plans between probability measures.\n\nRelevant
literature: arxiv.org/abs/2110.06591 and additional work in preparation.\
n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Florian Rabe
DTSTART;VALUE=DATE-TIME:20210902T170000Z
DTEND;VALUE=DATE-TIME:20210902T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/38
DESCRIPTION:Title: MMT: A UniFormal Approach to Knowledge Representa
tion\nby Florian Rabe as part of Topos Institute Colloquium\n\n\nAbstr
act\nUniFormal is the idea of representing all aspects of knowledge unifor
mly\, including narration\, deduction\, computation\, and databases.\nMore
over\, it means to abstract from the multitude of individual systems\, whi
ch not only often focus on just one aspect but are doing so in mutually in
compatible ways\, thus creating a universal framework of formal knowledge.
\n\nMMT is a concrete representation language to that end.\nIt systematica
lly abstracts from assumptions typically inherent in the syntax and semant
ics of concrete systems\, and focuses on language-independence\, modularit
y\, and system interoperability.\nWhile constantly evolving in order to co
nverge towards UniFormal\, its design and implementation have become very
mature.\nIt is now a readily usable high-level platform for the design\, a
nalysis\, and implementation of formal systems.\n\nThis talk gives an over
view of the current state of MMT\, its existing successes and its future c
hallenges.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jeremy Avigad
DTSTART;VALUE=DATE-TIME:20211104T180000Z
DTEND;VALUE=DATE-TIME:20211104T190000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/39
DESCRIPTION:Title: Formal mathematics\, dependent type theory\, and
the Topos Institute\nby Jeremy Avigad as part of Topos Institute Collo
quium\n\n\nAbstract\nModern logic tells us that mathematics can be formali
zed\, in principle. Computational proof assistants\, developed over the la
st half century\, make it possible to do so in practice. In this talk\, I
will briefly survey the state of the field today and discuss some of the r
easons that formalization is desirable. I will discuss one particular proo
f assistant\, Lean\, and its library\, mathlib. I will explain why depende
nt type theory\, Lean's underlying logical framework\, provides an attract
ive platform for formalization. Finally\, I will consider ways that formal
mathematics can support and enhance the Topos Institute's missions.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Danks
DTSTART;VALUE=DATE-TIME:20220217T170000Z
DTEND;VALUE=DATE-TIME:20220217T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/40
DESCRIPTION:Title: Ethics in AI\, not Ethics of AI\nby David Dan
ks as part of Topos Institute Colloquium\n\n\nAbstract\nDiscussions of the
ethical (and societal) impact of AI often implicitly assume that ethical
issues arise only once the AI Is deployed or used. If AI is “just math
” or “just a tool\,” then one might think that ethics is simply irre
levant to research and development of AI systems. In contrast\, I will arg
ue that ethical issues arise throughout every step of AI creation\, includ
ing research efforts that seem to be outside of the scope of ethics. That
is\, ethics is an intrinsic part of AI\, not something that arises only af
ter the fact. Throughout this argument\, I will provide examples of practi
cal tools and practices to improve the ethics in one’s AI systems. These
insights and examples will apply to technology development in general\, i
ncluding fundamental mathematical research.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bob Coecke
DTSTART;VALUE=DATE-TIME:20220224T170000Z
DTEND;VALUE=DATE-TIME:20220224T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/41
DESCRIPTION:Title: Compositional Intelligence\nby Bob Coecke as
part of Topos Institute Colloquium\n\n\nAbstract\nThis talk will be fairly
high-level and requires no prior technical background. We will introduce
the notion of compositional intelligence that my Oxford-based CQ-team is
trying to achieve. \n\nIn particular\, starting from the compositional ma
tch between natural language and quantum\, which also extends to other dom
ains [1]\, we will argue that a new generation of AI can emerge when fully
pushing this analogy while exploiting the completeness of categorical qua
ntum mechanics [2]. \n\nWe also discuss the notion of compositionality it
self\, which takes many different forms within many different contexts\, a
nd how the one we need goes beyond previous ones [3]. \n\n[1] Vincent Wan
g-Mascianica\, BC (2021) Talking Space: inference from spatial linguistic
meanings. https://arxiv.org/abs/2109.06554 \n\n[2] BC\, Dom Horsman\, Ale
ks Kissinger\, Quanlong Wang (2021) Kindergarden quantum mechanics graduat
es (...or how I learned to stop gluing LEGO together and love the ZX-calcu
lus). https://arxiv.org/abs/2102.10984\n\n[3] BC (2021) Compositionality
as we see it\, everywhere around us. https://arxiv.org/abs/2110.05327\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maaike Zwart
DTSTART;VALUE=DATE-TIME:20220331T170000Z
DTEND;VALUE=DATE-TIME:20220331T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/43
DESCRIPTION:Title: Lessons from failing distributive laws\nby Ma
aike Zwart as part of Topos Institute Colloquium\n\n\nAbstract\nComposing
monads via distributive laws is tricky business\, as too often small mista
kes are overlooked. After failing to find a distributive law for the list
monad over itself\, I started proving that finding such a distributive law
is impossible. At the same time\, Dan Marsden was studying the famous cou
nterexample by Gordon Plotkin that probability does not distribute over no
n-determinism. Together we developed an algebraic method to find and gener
alise such counterexamples\, resulting in our no-go theorems. In this talk
I will explain the main ideas behind our method\, illustrated by a proof
that 'plus does not distribute over times'. Then\, I will highlight some c
rucial steps in our method\, which tell us which type of monads are "high
risk" in failing to compose with other monads. Lastly (time permitting)\,
I will say a few words about my current research on combining monads with
guarded recursion.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thierry Coquand
DTSTART;VALUE=DATE-TIME:20220602T170000Z
DTEND;VALUE=DATE-TIME:20220602T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/44
DESCRIPTION:Title: Sheaf Cohomology in Univalent Type Theory\nby
Thierry Coquand as part of Topos Institute Colloquium\n\n\nAbstract\nIn t
he introduction of his book on Higher Topos Theory\, Jacob Lurie motivates
this theory by the fact that it allows an elegant and general treatment o
f sheaf cohomology. It was realised early on that these ideas could be exp
ressed in the setting of univalent foundations/homotopy type theory (cf. t
he blog post of Mike Shulman on cohomology\, 24 July 2013). I will try to
explain recent insights which show that this can be done in a maybe surpri
singly direct way. Furthermore\, all this can be formulated in a construct
ive meta theory\, avoiding the non effective notion of injective resolutio
ns.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Zoé Christoff
DTSTART;VALUE=DATE-TIME:20220317T170000Z
DTEND;VALUE=DATE-TIME:20220317T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/45
DESCRIPTION:Title: The logic of social influence in networks\nby
Zoé Christoff as part of Topos Institute Colloquium\n\n\nAbstract\nThis
talk gives an introduction to the use of logical tools in understanding so
cial influence and social networks phenomena. Individuals often form their
opinions by interpreting the behavior of others around them\, and by reas
oning about how those others have formed their opinions. This leads to sev
eral well-known herd phenomena\, such as informational cascades\, bystande
r effect\, pluralistic ignorance\, bubbles\, and polarization. For instanc
e\, in the case of informational cascades\, agents in a sequence imitate o
ne another’s choices despite having diverging private evidence\, sometim
es leading the whole community to make the worst possible choice. Similar
cascading mechanisms are at the heart of diffusion phenomena in social net
works. \n\nI first show how an epistemic logic modeling allows to make pre
cise the conditions for such cascades to form\, as well as prove their ine
scapability. I then turn to what logical tools can do for analysing inform
ation flow and influence in social networks. I illustrate how extremely si
mplified models can yield surprising new results\, for instance about stab
ilization conditions of diffusion processes. Finally\, I discuss how logic
might help us further understand how social networks affect collective de
cision making processes.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giuseppe Rosolini
DTSTART;VALUE=DATE-TIME:20220407T170000Z
DTEND;VALUE=DATE-TIME:20220407T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/46
DESCRIPTION:Title: When an elementary quotient completion is a quasi
topos\nby Giuseppe Rosolini as part of Topos Institute Colloquium\n\n\
nAbstract\nThe elementary quotient completion of an elementary doctrine ge
neralises the exact completion of a category with finite products and weak
equalisers. I intend to present a characterisation of those elementary qu
otient completions which produce a quasitopos. As a corollary one gets a c
haracterisation of the elementary quotient completions which give an eleme
ntary topos. Our work is reminiscent of\, and gathers ideas\, from others:
in particular\, Carboni and Vitale’s characterisation of exact completi
ons in terms of their projective objects\, Carboni and Rosolini’s charac
terisation of locally cartesian closed exact completions\, also in the rev
ision by Emmenegger\, and Menni’s characterisation of the exact completi
ons which are elementary toposes. This is joint work with Maria Emilia Mai
etti and Fabio Pasquali.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tai-Danae Bradley
DTSTART;VALUE=DATE-TIME:20220526T170000Z
DTEND;VALUE=DATE-TIME:20220526T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/47
DESCRIPTION:Title: Entropy as an Operad Derivation\nby Tai-Danae
Bradley as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk fe
atures a small connection between information theory\, algebra\, and topol
ogy—namely\, a correspondence between Shannon entropy and derivations of
the operad of topological simplices. We will begin with a brief review of
operads and their representations with topological simplices and the real
line as the main example. We then give a general definition for a derivat
ion of an operad in any category with values in an abelian bimodule over t
he operad. The main result is that Shannon entropy defines a derivation of
the operad of topological simplices\, and that for every derivation of th
is operad there exists a point at which it is given by a constant multiple
of Shannon entropy. We show this is compatible with\, and relies heavily
on\, a well-known characterization of entropy given by Faddeev in 1956 and
a recent variation given by Leinster.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dominic Verity
DTSTART;VALUE=DATE-TIME:20220324T200000Z
DTEND;VALUE=DATE-TIME:20220324T210000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/48
DESCRIPTION:Title: Zen and the art of ∞-categories\nby Dominic
Verity as part of Topos Institute Colloquium\n\n\nAbstract\nYou may well
have heard the rumour that ∞-category theory is “really just like cate
gory theory with a little homotopy theory thrown in”. Inspired by that c
omment\, you might even have headed to a book on ∞-categories or to the
nLab to find out more\, only to find that things in the ∞-world are far
from that simple.\n\nFirstly you will have discovered that there is no uni
versal agreement on what an ∞-category actually is. Instead\, you’ve b
een met with a proliferation of ∞-categorical models\; simplicially enri
ched categories\, quasi-categories\, (iterated) complete Segal spaces\, co
mplicial sets\, Θ-spaces and so on. Then you discover\, to your horror\,
that each one of these models supports its own particular interpretations
of common categorical concepts\, some of which appear far more familiar th
an others. Finally\, you realise that the relationships between the catego
ry theories developed for each model are also much less than clear.\n\nIf
this weren’t enough to leave anyone reaching for the Aspirin bottle\, th
ere is more bad news to come. It quickly becomes clear that there exists q
uite a large gap between the informal language used to describe ∞-catego
rical arguments\, in blog posts and wiki articles\, and the corresponding
formal arguments expressed in any particular model of ∞-categories. Most
of these are given either as concrete constructions with simplicial (or i
ncreasingly cubical) objects or as abstract model category theoretic argum
ents. Now I have no doubt that we “all” love a good simplicial argumen
t\, but encoding things in this way does very little to aid our categorica
l intuition.\n\nThere must be a better way!\n\nIn this talk we discuss rec
ent developments in ∞-technology that seek to address these issues. Spec
ifically\, we review the current state of the art in model agnostic ∞-ca
tegory theory [2]\, which seeks to provide a unified account of ∞-catego
ry theory freed from the straight jacket of a specific model. This allows
both for the model independent\, synthetic development of ∞-categorical
results and for the transport of analytically derived such results from on
e model to another. We shall also see how these techniques are rapidly bei
ng reframed in type theoretic terms\, through the development of directed
type theory [1\,3]\, thereby promising a more natural language for the for
mal development of ∞-categorical concepts and results.\n\nReferences\n\n
[1] E. Riehl\, M. Shulman\, A type theory for synthetic ∞-categories\, H
igh. Struct. 1 (2017) 147224.\n\n[2] E. Riehl\, D. Verity\, Elements of
∞-category theory\, Cambridge University Press\, 2022.\n\n[3] J. Weinber
ger\, A synthetic perspective on (∞\,1)-category theory: Fibrational and
semantic aspects\, arXiv Preprint arXiv:2202.13132. (2022).\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Glynn Winskel
DTSTART;VALUE=DATE-TIME:20220303T170000Z
DTEND;VALUE=DATE-TIME:20220303T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/50
DESCRIPTION:Title: Making concurrency functional\nby Glynn Winsk
el as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk bridges
between two major paradigms in computation\, the *functional*\, at basis c
omputation from input to output\, and the *interactive*\, where computatio
n reacts to its environment while underway. Central to any compositional
theory of interaction is the dichotomy between a system and its environmen
t. Concurrent games and strategies address the dichotomy in fine detail\,
very locally\, in a distributed fashion\, through distinctions between Pla
yer moves (events of the system) and Opponent moves (those of the environm
ent). A functional approach has to handle the dichotomy much more ingeniou
sly\, through its blunter distinction between input and output. This has l
ed to a variety of functional approaches\, specialised to particular inte
ractive demands. Through concurrent games we can more clearly see what sep
arates and connects the differing paradigms\, and show how: \n\n\n— to l
ift functions to strategies\; the "Scott order" intrinsic to \nconcurrent
games plays a key role in turning functional dependency to causal depende
ncy. \n\n— several paradigms of functional programming and logic arise n
aturally as subcategories of concurrent games\, \nincluding stable domain
theory\; nondeterministic dataflow\; geometry of interaction\; the dialec
tica interpretation\; lenses and optics\; and \ntheir extensions to contai
ners in dependent lenses and optics. \n\n— to transfer enrichments of
strategies (such as to probabilistic\, quantum or real-number computation)
to functional cases.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leo McElroy
DTSTART;VALUE=DATE-TIME:20220414T170000Z
DTEND;VALUE=DATE-TIME:20220414T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/51
DESCRIPTION:Title: Making Microworlds: A Framework for Making Sense
by Making Things\nby Leo McElroy as part of Topos Institute Colloquium
\n\n\nAbstract\nPeople learn best by making things they care about\, which
they share with others. The role of an educational technologist is to com
municate this principle through tools provided to learners. A primary item
in this toolmakers’ toolkit is the microworld\, a concept developed by
Seymour Papert as a “growing place for a specific species of powerful id
eas or intellectual structures.” A microworld presents someone with a sm
all set of ideas in an explorable environment which helps the learner reco
mpose those ideas for their own personal expression. Following the develop
ment of a collection of microworlds\, we will uncover the meta-structure o
f the “growing place” for intellectual structures\, with the aim of id
entifying a framework for making tools\, for making sense\, by making thin
gs.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alexandra Silva
DTSTART;VALUE=DATE-TIME:20220519T170000Z
DTEND;VALUE=DATE-TIME:20220519T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/52
DESCRIPTION:Title: Learning Weighted Automata over Principal Ideal D
omains\nby Alexandra Silva as part of Topos Institute Colloquium\n\n\n
Abstract\nIn the first part of this talk\, we discuss active learning algo
rithms for weighted automata over a semiring. We show that a variant of An
gluin's seminal L* algorithm works when the semiring is a principal ideal
domain\, but not for general semirings such as the natural numbers. In the
second part\, we present some preliminary work on active learning for pro
babilistic automata\, and in particular discuss what the setup of the prob
lem looks like and how that leads (or not) to impossibility results.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Moshe Vardi
DTSTART;VALUE=DATE-TIME:20220623T170000Z
DTEND;VALUE=DATE-TIME:20220623T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/53
DESCRIPTION:Title: Ethics Washing in AI\nby Moshe Vardi as part
of Topos Institute Colloquium\n\n\nAbstract\nOver the past decade Artifici
al Intelligence\, in general\, and Machine Laerning\, in particular\, have
made impressive advancements\, in image recognition\, game playing\, natu
ral-language understanding and more. But there were also several instances
where we saw the harm \nthat these technologies can cause when they are d
eployed too hastily. A Tesla crashed on Autopilot\, killing the driver\; a
self-driving Uber crashed\, killing a pedestrian\; and commercial face-re
cognition systems performed terribly in audits on dark-skinned people. In
response to that\, there has been much recent talk of AI ethics. Many orga
nizations produced AI-ethics guidelines and companies publicize their newl
y established responsible-AI teams.\n\nBut talk is cheap. "Ethics washing"
— also called “ethics theater” — is the practice of fabricating o
r exaggerating a company’s interest in equitable AI systems that work fo
r everyone. An example is when a company promotes “AI for good” initia
tives with one hand\, while selling surveillance tech to governments and c
orporate customers with the other. I will argue that the ethical lens is t
oo narrow. The real issue is how to deal with technology's impact on socie
ty. Technology is driving the future\, but who is doing the steering?\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nicolas Behr
DTSTART;VALUE=DATE-TIME:20220609T170000Z
DTEND;VALUE=DATE-TIME:20220609T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/54
DESCRIPTION:Title: Fundamentals of Compositional Rewriting Theory\nby Nicolas Behr as part of Topos Institute Colloquium\n\n\nAbstract\nTh
is presentation is based upon [1] (joint work with R. Harmer and J. Krivin
e). \n\nCategorical rewriting theory is a research field in both computer
science and applied category theory\, with a rich history spanning over 50
years of active developments\, starting with the pioneering work of Ehrig
in the 1970s.\n\nIn this talk\, I will present recent results [1] on a no
vel foundation for reasoning about rewriting theories via so-called compos
itional rewriting double categories (crDCs). The design principles followe
d in this approach are the typical "unify and conquer" strategy of applied
category theory and a particular variant of the notion of compositionalit
y. \n\nTo wit\, crDCs permit to formulate a wide variety of categorical re
writing semantics uniformly\, whereby the horizontal category for a given
semantics models the rewriting rules\, while the vertical category models
matchings and co-matchings of rules into objects\, and where the squares m
odel so-called direct derivations (i.e.\, individual rewriting steps). Eve
n before considering compositionality\, it is already noteworthy that in o
rder for crDCs to be well-defined\, strong constraints are imposed upon th
e horizontal and vertical categories and the squares of the crDC\, which i
n effect suggest categories with adhesivity properties (e.g.\, toposses\,
quasi-toposses\, adhesive HLR categories\,...) as natural starting points
for constructing crDCs. In this sense\, the notion of crDCs thus permits t
o justify the by now standard approach for categorical rewriting theories
developed over the past 20 years as being based upon categories with adhes
ivity properties (starting with the seminal work of Lack and Sobocinski on
adhesive categories) from a clear mathematical high-level perspective.\n\
nCompositionality\, on the other hand\, is a much deeper mathematical prop
erty that a categorical rewriting theory may carry. This property entails
the existence of so-called Concurrency and Associativity Theorems. The for
mer concerns being able to reason on two-step rewriting sequences via impl
ementing the overall effect of the two-step rewrite via a composite rule a
pplied in a single rewrite step\, and vice versa. The Associativity Theore
m then implies that the operation of forming compositions of rewriting rul
es is\, in a certain sense\, associative. Compositionality is a necessary
and crucial ingredient in the stochastic mechanics and rule algebra formal
ism developed by Behr et al. since 2015\, and which permits to provide a m
athematically fully consistent and universal formalism for continuous- [2]
and discrete-time Markov Chains [3] (central to applications of rewriting
to bio- and organo-chemistry\, social network modeling\, etc.) and rule-a
lgebraic combinatorics [4].\n\nA central result of [1] is then that a suff
icient set of conditions on a double category to model a *compositional* r
ewriting theory consists in requiring certain fibrational properties for t
he vertical source and target functors from squares of the double categori
es\, i.e.\, that they are (residual) multi-opfibrations. I will sketch how
these fibrational properties in conjunction with the other crDC axioms yi
eld a completely uniform proof of both the Concurrency and the Associativi
ty Theorems\, and\, time permitting\, how a large variety of categorical r
ewriting semantics indeed fall under the umbrella of our novel crDC formal
ism. \n\nFinally\, I will provide an overview of open questions and potent
ial fruitful cross-connections of crDC theory with the TIC and broader ACT
communities.\n\n\n[1] N. Behr\, R. Harmer and J. Krivine\, "Fundamentals
of Compositional Rewriting Theory"\, https://arxiv.org/abs/2204.07175 \n\n
[2] N. Behr\, J. Krivine\, J.L. Andersen\, D. Merkle (2021)\, "Rewriting t
heory for the life sciences: A unifying theory of CTMC semantics"\, https:
//doi.org/10.1016/j.tcs.2021.07.026\n\n[3] N. Behr\, B.S. Bello\, S. Ehme
s\, R. Heckel (2021)\, "Stochastic Graph Transformation For Social Network
Modeling"\, https://doi.org/10.4204/EPTCS.350.3\n\n[4] N. Behr (2021)\,
"On Stochastic Rewriting and Combinatorics via Rule-Algebraic Methods"\, h
ttp://dx.doi.org/10.4204/EPTCS.334.2\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Martín Escardó
DTSTART;VALUE=DATE-TIME:20220428T170000Z
DTEND;VALUE=DATE-TIME:20220428T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/55
DESCRIPTION:Title: Compact totally separated types in constructive u
nivalent type theory\nby Martín Escardó as part of Topos Institute C
olloquium\n\n\nAbstract\nIf a type X is finite\, then for every map p: X
→ 𝟚 we can tell\, by exhaustive search\, whether p has a root (we can
exhibit x with p x = 0) or not (for every x : X we have that p x = 1). Pe
rhaps surprisingly\, there are infinite types X for which this decision is
constructively possible. We call such types compact. It turns out that th
ere are plenty of infinite compact types in any 1-topos. A basic\, but per
haps surprising\, example is the type ℕ∞ of decreasing infinite binary
sequences. There are plenty more\, and the purpose of this talk is to exh
ibit them. No matter how hard we tried to avoid that\, all searchable type
s we could find happen to be well-ordered. But this is just as well\, beca
use we can use ordinals to measure how complicated the compact types that
we can write down in constructive univalent type theory are. Much of the a
bove discussion can be carried out in (the internal language of) a 1-topos
. But then some of our constructions go beyond that\, by considering the t
ype of all ordinals in a universe\, which is itself an ordinal in the next
universe\, and requires univalence and hence moves us to the realm of ∞
-toposes. It remains to address the notion of total separatedness of a typ
e X. This is the condition that there are plenty of maps X → 𝟚 to "se
parate the points of X" in a suitable sense. I'll rigorously define this a
nd exhibit plenty of compact\, totally separated\, well-ordered types in u
nivalent type theory. I will mention Johnstone's topological topos as an e
xample of where "compact" and "totally separated" acquire their usual topo
logical meaning. There is an old\, non-constructive\, theorem of topology
that characterizes the compact countable Hausdorff spaces as the countable
ordinals with the interval topology. In the topological topos\, assuming
a non-constructive meta-language to reason about it\, the searchable objec
ts we get are of this form.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christoph Benzmueller
DTSTART;VALUE=DATE-TIME:20220616T170000Z
DTEND;VALUE=DATE-TIME:20220616T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/56
DESCRIPTION:Title: Logico-pluralistic exploration of foundational th
eories with computers\nby Christoph Benzmueller as part of Topos Insti
tute Colloquium\n\n\nAbstract\nSymbolic knowledge representation and reaso
ning (KR&R) is a key aspect of human intelligence. Among other things\, it
enables scientists to explore new theories\, declaratively describe them\
, and share them with colleagues. In the natural sciences\, abstract theor
ies often arise from observations and experiments\; in other fields\, such
as metaphysics\, they may result from pure thought experiments\, possibly
without data from which to start (and learn from). Strong AI without exp
licit symbolic KR&R capabilities thus seems unthinkable. But how can the e
xploration of abstract theories\, especially fundamental theories of metap
hysics and mathematics\, including logical formalisms\, be fruitfully supp
orted on computers? \n\nIn this talk\, I review recent contributions in wh
ich a logico-pluralistic KR&R methodology and infrastructure\, called Logi
KEy\, has been successfully applied to the exploration and assessment of f
oundational theories in metaphysics and mathematics. One such exploratory
study on the axiomatic foundations of category theory\, conducted jointly
with Dana Scott and students at FU Berlin\, will be described in some more
detail. Since LogiKEy also supports exploration and assessment of ethical
and legal theories\, it also has applications in the areas of trusted AI
and AI&Law.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrej Bauer
DTSTART;VALUE=DATE-TIME:20220512T170000Z
DTEND;VALUE=DATE-TIME:20220512T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/57
DESCRIPTION:Title: The countable reals\nby Andrej Bauer as part
of Topos Institute Colloquium\n\n\nAbstract\nJoint work with James E. Hans
on from the University of Maryland\, https://james-hanson.github.io.\n\nIn
1874 Georg Cantor published a theorem stating that every sequence of real
s is avoided by some real\, thereby showing that the reals are not countab
le. Cantor's proof uses classical logic. There are constructive proofs\, a
lthough they all rely on the axiom of countable choice. Can the real numbe
rs be shown uncountable without excluded middle and without the axiom of c
hoice? An answer has not been found so far\, although not for lack of tryi
ng.\n\nWe show that there is a topos in which the real numbers are countab
le\, i.e.\, there is an epimorphism from the object of natural numbers to
the object of Dedekind reals. Therefore\, higher-order intuitionistic logi
c cannot show the reals to be uncountable.\n\nThe starting point of our co
nstruction is a sequence of reals\, shown to exist by Joseph S. Miller fro
m University of Wisconsin–Madison\, with a strong counter-diagonalizatio
n property: if an oracle Turing machine computes a specific real number\,
when given any oracle representing Miller's sequence\, then the number app
ears in the sequence. One gets the idea that the reals ought to be countab
le in a realizability topos built from Turing machines with oracles for Mi
ller's sequence. However\, we cannot just use ordinary realizability\, bec
ause all realizability toposes validate countable choice and consequently
the uncountability of the reals.\n\nTo obtain a topos with countable reals
\, we define a variant of realizability which we call parameterized realiz
ability. First we define parameterized partial combinatory algebras (ppca)
\, which are partial combinatory algebras whose evaluation depends on a pa
rameter. We then define parameterized realizability toposes. In these real
izers witness logical statements uniformly in the parameters. The motivati
ng example is the parameterized realizability topos built from the ppca of
oracle Turing machines parameterized by oracles for Miller's sequence. In
this topos\, Miller's sequence is the desired epimorphism from natural nu
mbers to Dedekind reals.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Terilla
DTSTART;VALUE=DATE-TIME:20220505T170000Z
DTEND;VALUE=DATE-TIME:20220505T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/58
DESCRIPTION:Title: Rethinking language\nby John Terilla as part
of Topos Institute Colloquium\n\n\nAbstract\nLanguage is essential to bein
g human. Without it\, no aspect of modern life could exist. But what is
language exactly? How precisely does meaning emerge from sequences constr
ucted from a small collection of basic symbols or sounds? Biologists\, li
nguists\, and philosophers have been debating this question---still unansw
ered---for thousands of years. \n\nNow\, at a pivotal moment when intelli
gent machines are beginning to acquire human language skills\, new insight
s into the nature of language are emerging. Some old beliefs about langu
age can probably be cast aside and achievements in artificial intelligence
are inspiring some new ways of thinking of language.\n\nI will present an
argument for rethinking language and give a tour of some relevant mathema
tical ideas. The talk will be prepared keeping in mind the four themes of
the Topos Institute Colloquium: ethics and societal impact of mathematic
s\, applied category theory\, foundation models\, and technology and tools
.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Eduardo Dubuc
DTSTART;VALUE=DATE-TIME:20220915T170000Z
DTEND;VALUE=DATE-TIME:20220915T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/59
DESCRIPTION:Title: On localizations via homotopies\nby Eduardo D
ubuc as part of Topos Institute Colloquium\n\n\nAbstract\n(joint work with
J. Gilabert based on work by Descotte-Dubuc-Szyld).\n\nLet $\\mathcal{C}$
be a category and $\\Sigma$ be a class of morphisms. The localization of
\n$\\mathcal{C}$ at $\\Sigma$ is a category $\\mathcal{C}[\\Sigma^{-1}]$ t
ogether with a functor $q: \\mathcal{C} \\longrightarrow \\mathcal{C}[\\Si
gma^{-1}]$ such that $q(s)$ is an isomorphism for all $s \\in \\Sigma$\, a
nd which is initial among such functors. The 2-localization is a 2-catego
ry $\\mathcal{C}[\\Sigma^{\\sim 1}]$ together with a functor \n$q: \\mathc
al{C} \\longrightarrow \\mathcal{C}[\\Sigma^{\\sim 1}]$ such that $q(s)$ i
s a equivalence for all $s \\in \\Sigma$\, and which is initial among such
functors. In this talk I will consider the construction of such localizat
ions by means of cylinders and its corresponding homotopies\, which will d
etermine the 2-cells of $\\mathcal{C}[\\Sigma^{\\sim 1}]$. I will examine
the case where $\\Sigma = \\mathcal{W}$ is the class of weak equivalences
of a Quillen's model category\, and in particular the role of the fibrant
and cofibrant replacements. I will elaborate about functorial versus non
functorial factorizations in this construction. \nI will recall informally
but with sufficient precision the necessary definitions so that the non
experts can grasp the ideas and follow the proofs.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Noam Zeilberger
DTSTART;VALUE=DATE-TIME:20220630T170000Z
DTEND;VALUE=DATE-TIME:20220630T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/60
DESCRIPTION:Title: Parsing as a lifting problem and the Chomsky-Sch
ützenberger representation theorem\nby Noam Zeilberger as part of Top
os Institute Colloquium\n\n\nAbstract\nJoint work with Paul-André Melliè
s.\n\nIn “Functors are Type Refinement Systems” [1]\, we argued for th
e idea that rather than being modelled merely as categories\, type systems
should be modelled as functors p : D → T from a category D whose morphi
sms are typing derivations to a category T whose morphisms are the terms c
orresponding to the underlying subjects of those derivations. One advantag
e of this fibrational point of view is that the notion of typing judgment
receives a simple mathematical status\, as a triple (R\,f\,S) consisting o
f two objects R\, S in D and a morphism f in T such that p(R)=dom(f) and p
(S)=cod(f). The question of finding a typing derivation for a typing judgm
ent (R\,f\,S) then reduces to the lifting problem of finding a morphism α
: R → S such that p(α)=f. We developed this perspective in a series of
papers\, and believe that it may be usefully applied to a large variety o
f deductive systems\, beyond type systems in the traditional sense. In thi
s work [2]\, we focus on derivability in context-free grammars\, a classic
topic in formal language theory with wide applications in computer scienc
e.\n\nThe talk will begin by explaining how derivations in any context-fre
e grammar G may be naturally encoded by a functor of operads p : Free S
→ W[Σ] from a freely generated operad into a certain “operad of splic
ed words”. This motivates the introduction of a more general notion of c
ontext-free grammar over any category C\, defined as a finite species S eq
uipped with a color denoting the start symbol and a functor of operads p :
Free S → W[C] into the operad of spliced arrows in C. We will see that
many standard concepts and properties of context-free grammars and languag
es can be formulated within this framework\, thereby admitting simpler ana
lysis\, and that parsing may indeed be profitably considered from a fibrat
ional perspective\, as a lifting problem along a functor from a freely gen
erated operad.\n\nThe second half of the talk will be devoted to a new pro
of of the Chomsky-Schützenberger Representation Theorem. An important ing
redient is the identification of a left adjoint C[−] : Operad → Cat to
the operad of spliced arrows functor W[−] : Cat → Operad. This constr
uction builds the contour category C[O] of any operad O\, whose arrows hav
e a geometric interpretation as “oriented contours” of operations. A d
irect consequence of the contour / splicing adjunction is that every finit
e species equipped with a color induces a universal context-free grammar\,
generating a language of tree contour words. Finally\, we prove a general
ization of the Chomsky-Schützenberger Representation Theorem\, establishi
ng that any context-free language of arrows over a category C is the funct
orial image of the intersection of a C-chromatic tree contour language and
a regular language.\n\n[1] P.-A. Melliès and N. Zeilberger\, Functors ar
e type refinement systems\, POPL 2015\n\n[2] P.-A. Melliès and N. Zeilber
ger\, Parsing as a lifting problem and the Chomsky-Schützenberger represe
ntation theorem\, to appear at MFPS 2022\, preliminary version available a
t https://hal.archives-ouvertes.fr/hal-03702762\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dan Koditschek
DTSTART;VALUE=DATE-TIME:20221013T170000Z
DTEND;VALUE=DATE-TIME:20221013T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/61
DESCRIPTION:Title: Working Compositions for Correct Execution of Rob
ot Task Specifications\nby Dan Koditschek as part of Topos Institute C
olloquium\n\n\nAbstract\nA long tradition in robotics has deployed dynamic
al primitives as empirical modules of behavior [1]. Physically grounded fo
rmalization of these practices offers the prospect of an expressive progra
mming language of work for dynamically dexterous robotics whose programs l
ead to task and motion planners with associated controllers that are corre
ct by design [2]. This talk will offer a brief progress report on a bottom
-up robotics research agenda seeking to formalize the use of Lagrangian en
ergy landscapes as “letters” whose hierarchical [3]\, parallel [4] and
sequential [5] compositions yield “words” of hybrid dynamical systems
with guaranteed behavioral properties. Attention then shifts to an emergi
ng architecture for top-down task and motion planning [6] that offers the
promise of abstract\, semantic\, formal specification [7] for mobile mani
pulation tasks carried out by general purpose robots [8] in learned\, geom
etrically complicated environments [9].\n\nThe talk concludes with a more
speculative appraisal of the prospects for a unified programming environme
nt allowing the expressive top-down specification of robot behavior with a
utomatic compilation into bottom-up words of work that are correct by desi
gn. A recent categorical treatment [10] of robot hybrid dynamical systems
[11] encodes a well-grounded version of sequential composition [12] and a
weak but still practicable version of hierarchical composition [3]\, while
neglecting the consideration of cross-talk [4] in its idealization of par
allel composition as a monoidal product. Subsequent results imbue a slight
ly restricted version of this hybrid dynamical category [10] with a versio
n of Conley’s fundamental theorem [13] guaranteeing the existence of glo
bal Lyapunov functions that decompose a suitably formulated relaxation of
the hybrid state space into a covering by attractor basins and their bound
aries [14]. Thus equipped with generalized energy landscapes\, more physi
cally grounded refinements of this hybrid dynamical category may yield a p
racticable type theory whose associated resource-aware linear logic clause
s might be integrated into the more expressive linear temporal logic inter
face to the task and motion planning architecture of [7]. Such future dev
elopments would greatly advance the longer term agenda toward an empirical
ly practicable theory of “programming work” [2].\n\n[1] M. H. Raibert\
, Legged Robots That Balance. Cambridge: MIT Press\, 1986.\n\n[2] D. E. Ko
ditschek\, “What Is Robotics? Why Do We Need It and How Can We Get It?\,
” Annu. Rev. Control Robot. Auton. Syst.\, vol. 4\, no. 1\, pp. 1–33\,
May 2021\, doi: 10.1146/annurev-control-080320-011601.\n\n[3] R. J. Full
and D. E. Koditschek\, “Templates and anchors: neuromechanical hypothese
s of legged locomotion on land\,” J. Exp. Biol.\, vol. 202\, pp. 3325–
3332\, 1999.\n\n[4] A. De\, S. A. Burden\, and D. E. Koditschek\, “A hyb
rid dynamical extension of averaging and its application to the analysis o
f legged gait stability:\,” Int. J. Robot. Res.\, vol. 37\, no. 2–3\,
pp. 266–286\, Mar. 2018\, doi: 10.1177/0278364918756498.\n\n[5] R. R. Bu
rridge\, A. A. Rizzi\, and D. E. Koditschek\, “Toward a systems theory f
or the composition of dexterous robot behaviours\,” Robot. Res. Seventh
Int. Symp. ISRR’95\, pp. 149–161.\n\n[6] V. Vasilopoulos et al.\, “R
eactive Semantic Planning in Unexplored Semantic Environments Using Deep P
erceptual Feedback\,” IEEE Robot. Autom. Lett.\, vol. 5\, no. 3\, pp. 44
55–4462\, Jul. 2020\, doi: 10.1109/LRA.2020.3001496.\n\n[7] V. Vasilopou
los\, Y. Kantaros\, G. Pappas\, and D. Koditschek\, “Reactive Planning f
or Mobile Manipulation Tasks in Unexplored Semantic Environments\,” IEEE
Int. Conf. Robot. Autom. ICRA\, May 2021\, [Online]. Available: https://r
epository.upenn.edu/ese_papers/880\n\n[8] T. T. Topping\, V. Vasilopoulos\
, A. De\, and D. Koditschek E.\, “Composition of Templates for Transitio
nal Pedipulation Behaviors\,” in Proc. Int. Symp. Rob. Res.\, 2019. [Onl
ine]. Available: https://repository.upenn.edu/ese_papers/860/\n\n[9] V. Va
silopoulos\, G. Pavlakos\, K. Schmeckpeper\, K. Daniilidis\, and D. E. Kod
itschek\, “Reactive navigation in partially familiar planar environments
using semantic perceptual feedback\,” Int. J. Robot. Res.\, vol. 41\, n
o. 1\, pp. 85–126\, Jan. 2022\, doi: 10.1177/02783649211048931.\n\n[10]
J. Culbertson\, P. Gustafson\, D. E. Koditschek\, and P. F. Stiller\, “F
ormal composition of hybrid systems\,” Theory Appl. Categ.\, vol. 35\, n
o. 45\, pp. 1634–1682\, Oct. 2020.\n\n[11] A. M. Johnson\, S. A. Burden\
, and D. E. Koditschek\, “A hybrid systems model for simple manipulation
and self-manipulation systems\,” Int. J. Robot. Res.\, vol. 35\, no. 11
\, pp. 1354--1392\, Sep. 2016\, doi: 10.1177/0278364916639380.\n\n[12] R.
R. Burridge\, A. A. Rizzi\, and D. E. Koditschek\, “Sequential Compositi
on of Dynamically Dexterous Robot Behaviors\,” Int. J. Robot. Res.\, vol
. 18\, no. 6\, pp. 534–555\, 1999\, doi: 10.1177/02783649922066385.\n\n[
13] C. R. Robinson\, Dynamical Systems: Stability\, Symbolic Dynamics\, an
d Chaos\, Second. Boca Raton\, FL: CRC Press\, 1999. Accessed: Jan. 29\, 2
017. [Online]. Available: http://imb-biblio.u-bourgogne.fr/Record.htm?reco
rd=325212414349&idlist=1\n\n[14] M. D. Kvalheim\, P. Gustafson\, and D. E.
Koditschek\, “Conley’s Fundamental Theorem for a Class of Hybrid Syst
ems\,” SIAM J. Appl. Dyn. Syst.\, pp. 784–825\, Jan. 2021\, doi: 10.11
37/20M1336576.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrea Censi
DTSTART;VALUE=DATE-TIME:20220825T170000Z
DTEND;VALUE=DATE-TIME:20220825T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/62
DESCRIPTION:Title: Categorification of Negative Information\nby
Andrea Censi as part of Topos Institute Colloquium\n\n\nAbstract\nI will p
resent some very recent and in-progress work about dealing\nwith “negati
ve information” categorically. This need arises naturally\nin applicatio
ns. For example\, in motion planning problems\, providing\nan optimal solu
tion is the same as giving a feasible solution (the\n“positive” inform
ation) together with a proof of the fact that there\ncannot be feasible so
lutions better than the one given (the “negative”\ninformation). We mo
del negative information by introducing the concept\nof “norphisms”\,
as opposed to the positive information of morphisms. A\n“nategory” is
a category that has “Nom”-sets in addition to hom-sets\,\nand specifie
s the compatibility rules between norphisms and morphisms.\nWith this setu
p we can choose to work in “coherent” “subnategories”:\nsubcategor
ies that describe a potential instantiation of the world in\nwhich all mor
phisms and norphisms are compatible. We derive the\ncomposition rules for
norphisms in a coherent subnategory\; we show\nthat norphisms do not compo
se by themselves\, but rather they need to\nuse morphisms as catalysts. We
have two distinct rules of the type\nmorphism + norphism → norphism. We
then show that those complex rules\nfor norphism inference are actually a
s natural as the ones for\nmorphisms\, from the perspective of enriched ca
tegory theory.\n\nThis is joint work with Dr. Jonathan Lorand and Ph.D. st
udent Gioele Zardini.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Angeliki Koutsoukou Argyraki
DTSTART;VALUE=DATE-TIME:20221006T170000Z
DTEND;VALUE=DATE-TIME:20221006T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/63
DESCRIPTION:Title: The new era of formalised mathematics and the ALE
XANDRIA Project\nby Angeliki Koutsoukou Argyraki as part of Topos Inst
itute Colloquium\n\n\nAbstract\nThe formalisation of mathematics with proo
f assistants has recently seen a \nconsiderable increase in activity\, wit
h fast-expanding\, flourishing communities attracting computer scientists\
, mathematicians and students. I will discuss the philosophy and motivatio
n behind the use of modern proof assistants to formalise mathematics\, ref
erring to the state of the art and potential of the area and to recent dev
elopments involving the formalisation of advanced\, research-level mathema
tics. I will share my experiences from my participation in the ERC project
"ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician" (htt
ps://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/) at the University of Cambr
idge led by Professor Lawrence C. Paulson FRS and I will give an overview
of the main contributions and achievements of the project so far.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Richard Zanibbi
DTSTART;VALUE=DATE-TIME:20221027T160000Z
DTEND;VALUE=DATE-TIME:20221027T170000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/65
DESCRIPTION:Title: Mathematical Information Retrieval: Searching wit
h Formulas and Text\nby Richard Zanibbi as part of Topos Institute Col
loquium\n\n\nAbstract\nMathematical information is essential for technical
work\, but its creation\, interpretation\, and search are challenging. In
the hopes of helping users locate mathematical information more easily\,
multimodal retrieval models and search interfaces that support both formul
as and text have been developed.\n\nIn this talk we will start by discussi
ng some differences between the information needs and search behaviors of
mathematical experts vs. non-experts. We will then examine techniques used
for retrieving math formulas\, and math-aware search engines that support
queries containing both formulas and text. Finally\, we will consider fut
ure research directions for math-aware search\, including tasks involving
Natural Language Processing (NLP) for mathematical texts.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Jaz Myers
DTSTART;VALUE=DATE-TIME:20220908T170000Z
DTEND;VALUE=DATE-TIME:20220908T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/66
DESCRIPTION:Title: A synthetic approach to orbifolds\nby David J
az Myers as part of Topos Institute Colloquium\n\n\nAbstract\nOrbifolds ar
e smooth spaces where the points may have finitely many internal symmetrie
s. These spaces often arise as quotients of manifolds by the actions of di
screte groups --- that is\, in situations with discrete symmetries\, such
as in crystallography. \n\nFormally\, the notion of orbifold has been pres
ented in a number of different guises -- from Satake's V-manifolds to Moer
dijk and Pronk's proper étale groupoids -- which do not on their face res
emble the informal definition. The reason for this divergence between form
alism and intuition is that the points of spaces cannot have internal symm
etries in traditional\, set-level foundations. In this talk\, we will see
a formal definition which closely tracks the informal idea of an orbifold.
\n\nBy working with the axioms of synthetic differential geometry in cohes
ive homotopy type theory\, we will give a synthetic definition of orbifold
(subsuming the traditional definitions) which closely resembles the infor
mal definition: an orbifold is a microlinear type where the type of identi
fications between any two points is properly finite. In homotopy type theo
ry\, we can construct these orbifolds simply by giving their type of point
s.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jacques Carette
DTSTART;VALUE=DATE-TIME:20220922T170000Z
DTEND;VALUE=DATE-TIME:20220922T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/67
DESCRIPTION:Title: What I learned from formalizing Category Theory i
n Agda\nby Jacques Carette as part of Topos Institute Colloquium\n\n\n
Abstract\nAn interesting side-effect of formalizing mathematics in a theor
em prover is that such efforts frequently leads to learning new details (*
) about a known topic. I'll discuss these "little gems" that become much m
ore apparent via formalization. While the focus will be mostly on items le
arned through formalizing Category Theory\, a few nuggets from other domai
ns (Universal Algebra\, and the theory of programming languages) will also
be thrown in.\n\n(*) These details are frequently known to select experts
\, but rarely ever recorded in print.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chad Scherrer
DTSTART;VALUE=DATE-TIME:20220901T170000Z
DTEND;VALUE=DATE-TIME:20220901T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/68
DESCRIPTION:Title: Applied Measure Theory for Composable Statistical
Modeling\nby Chad Scherrer as part of Topos Institute Colloquium\n\n\
nAbstract\nStatistics is often framed in terms of probability distribution
s. Distributions are special cases of measures\; we find that working in t
hese more general terms leads more naturally to a composable system. For e
xample\, a univariate probability density function is defined relative to
Lebesgue measure. Bayesian inference often leaves us with an unnormalized
posterior\, which (until normalized) is not a distribution at all\, but a
measure.\n\nThe MeasureTheory.jl ecosystem takes a principled approach to
design\, identifying primitives (measures like Lebesgue and Counting measu
re that cannot be described in terms of other measures)\, and a rich set o
f combinators for building new measures from existing ones. This approach
gives good performance and makes it easy to describe measures and related
structures (kernels\, likelihoods\, etc) that are awkward or impossible to
express in other systems.\n\nAfter introducing some fundamental concepts
relevant to the field of measure theory\, this talk will give an overview
of the MeasureTheory.jl library\, finally closing with a brief introductio
n to Tilde.jl\, a probabilistic programming language that specifically tar
gets MeasureTheory.jl.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Josef Urban
DTSTART;VALUE=DATE-TIME:20220707T170000Z
DTEND;VALUE=DATE-TIME:20220707T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/69
DESCRIPTION:Title: Combining learning and deduction over formal math
corpora\nby Josef Urban as part of Topos Institute Colloquium\n\n\nAb
stract\nThe talk will give a brief overview of recent methods that combine
learning and deduction over large formal libraries. I will mention the "
hammer" linkups between ITPs and ATPs\, systems that learn and perform dir
ect tactical guidance of ITPs\, discuss learning of premise selection over
large libraries\, and learning-based guidance of saturation-style and tab
leau-style automated theorem provers (ATPs) trained over the large proof c
orpora. I will also mention feedback loops between proving and learning in
this setting\, and show some autoformalization and conjecturing experimen
ts.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Johan Commelin
DTSTART;VALUE=DATE-TIME:20220929T170000Z
DTEND;VALUE=DATE-TIME:20220929T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/70
DESCRIPTION:Title: Breaking the one-mind-barrier in mathematics usin
g formal verification\nby Johan Commelin as part of Topos Institute Co
lloquium\n\n\nAbstract\nIn this talk I will argue that formal verification
helps break the\none-mind-barrier in mathematics. Indeed\, formal verific
ation allows a\nteam of mathematicians to collaborate on a project\, witho
ut one person\nunderstanding all parts of the project. At the same time\,
it also\nallows a mathematician to rapidly free mental RAM in order to wor
k on a\ndifferent component of a project. It thus also expands the\none-mi
nd-barrier by reducing cognitive load.\n\nI will use the Liquid Tensor Exp
eriment as an example\, to illustrate\nthe above two points. This project
recently finished the formalization\nof the main theorem of liquid vector
spaces\, following up on a\nchallenge by Peter Scholze.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gilles Dowek
DTSTART;VALUE=DATE-TIME:20221110T170000Z
DTEND;VALUE=DATE-TIME:20221110T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/72
DESCRIPTION:Title: From the Universality of Mathematical Truth to th
e Interoperability of Proof Systems\nby Gilles Dowek as part of Topos
Institute Colloquium\n\n\nAbstract\nThe development of computerized proof
systems is a major step forward in the never ending quest of mathematical
rigor. But it jeopardizes once again the universality of mathematical trut
h\, each proof system defining its own language for mathematical statement
s and its own truth conditions for these statements. One way to address t
his issue is to view the formalisms implemented in these systems as theori
es expressed in a common logical framework\, such as Predicate logic\, λ-
Prolog\, Isabelle\, the Edinburgh logical framework\, or Dedukti. We show
in the talk how theories\, such as Simple type theory\, Simple type theor
y with polymorphism\, Simple type theory with predicate subtyping\, the Ca
lculus of constructions... can be expressed in Dedukti. Proofs developed
with proof processing systems then can be expressed in these theories\, in
dependently of the system they have been developed with\, and used in any
system that supports the axioms they use.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pawel Sobocinski
DTSTART;VALUE=DATE-TIME:20221201T170000Z
DTEND;VALUE=DATE-TIME:20221201T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/74
DESCRIPTION:Title: Electrical circuits with string diagrams\nby
Pawel Sobocinski as part of Topos Institute Colloquium\n\n\nAbstract\nOne
of the goals of applied category theory is to develop new mathematics for
reasoning about open systems of various kinds. In this talk\, I will intro
duce a string diagrammatic methodology for reasoning about and manipulatin
g non-passive electrical circuits\, which are a classical and well-known e
xample of open system. This joint work with Guillaume Boisseau is\, on the
one hand\, a rigorous\, compositional\, sound and complete equational cal
culus\, while on the other hand\, it retains elements of the intuitive\, c
lassical diagrammatic syntax for circuits. It is based on previous work on
Affine Graphical Algebra\, joint work with Bonchi\, Piedeleu and Zanasi w
hich I will first introduce.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robin Cockett
DTSTART;VALUE=DATE-TIME:20221020T170000Z
DTEND;VALUE=DATE-TIME:20221020T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/75
DESCRIPTION:Title: Turing categories\nby Robin Cockett as part o
f Topos Institute Colloquium\n\n\nAbstract\nThis talk is based on the foll
owing papers/notes:\n\n(1) "Introduction to Turing categories" with Pieter
Hofstra\n\n(2) "Timed set\, functional complexity\, and computability" wi
th Boils\, Gallagher\, Hrubes\n\n(3) "Total maps of Turing categories" wit
h Pieter Hofstra and Pavel Hrubes\n\n(4) "Estonia notes" on my website\n\n
Turing categories are the theory of "abstract computability". Their devel
opment followed my meeting Pieter Hofstra. He was in Ottawa at the time a
nd he subsequently joined me as a postdoc. The core theory was developed
in Calgary before he returned to Ottawa as a faculty member. Tragically h
e died earlier this year when there was still so much to do and\, indeed\,
that he had done\, but had not published.\n\nTuring categories are import
ant because they characterize computability in a minimal traditional conte
xt. These ideas are not original to Pieter and I: De Paola\, Heller\, Lon
go\, Moggi\, and others had all travelled in this terrain before we did.
Pieter and I simply took the ideas polished them a bit and moved them a s
tep further on a road which still stretches ahead. \n\nSo\, the purpose o
f the talk is to try and explain what all this was about ... and what we w
ere striving to accomplish. To do this I have to introduce restriction ca
tegories and Turing categories in that context. Then I will describe a fa
mily of models which are fundamental to computer science. Finally\, I wil
l take a quick look along the road at some open issues.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bryce Clarke
DTSTART;VALUE=DATE-TIME:20221103T170000Z
DTEND;VALUE=DATE-TIME:20221103T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/76
DESCRIPTION:Title: A double-categorical approach to lenses via algeb
raic weak factorisation systems\nby Bryce Clarke as part of Topos Inst
itute Colloquium\n\n\nAbstract\nThe goal of this talk is to draw a common
thread between three concepts: double categories\, lenses\, and algebraic
weak factorisation systems (AWFS). A double category is a 2-dimensional ca
tegorical structure consisting of objects\, horizontal and vertical morphi
sms\, and cells between them. In applied category theory\, lenses are a ki
nd of morphism which consist of a forwards component and a backwards compo
nent. An AWFS on a category C consists of a compatible comonad L and monad
R on the arrow category of C\, such that each morphism factors into an L-
coalgebra followed by an R-algebra. In each case\, two classes of morphism
s play a central role — horizontal and vertical\, forwards and backwards
\, coalgebras and algebras — and it is natural to wonder if there is a d
eeper relationship between these three concepts. \n\nIn this talk\, I will
develop a double-categorical approach to lenses via AWFS. The approach bu
ilds upon the work of Bourke and Garner\, which characterises AWFS as cert
ain kinds of double categories\, and the work of Johnson\, Rosebrugh\, and
Wood\, which implicitly characterises lenses as members of the right clas
s of an AWFS. Combining these results leads indirectly to a double-categor
ical approach to lenses. However\, there is also a direct approach which c
onstructs a generalised notion of lens inside any double category\, using
a process called the "right-connected completion". I will compare these tw
o approaches\, and explore settings where they coincide.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrei Rodin
DTSTART;VALUE=DATE-TIME:20221215T170000Z
DTEND;VALUE=DATE-TIME:20221215T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/77
DESCRIPTION:Title: Univalent Foundations and Applied Mathematics
\nby Andrei Rodin as part of Topos Institute Colloquium\n\n\nAbstract\nIn
a series of lectures given in 2003 Vladimir Voevodsky identified two strat
egic goals for his further mathematical research. The goal number one was
to develop a "computerised library of mathematical knowledge". This line o
f research eventually led Voevodsky to the idea of Univalent Foundations a
nd its implementation with the UniMath library. The goal number two was t
o "bridge pure and applied mathematics". Voevodsky's research towards the
second goal did not bring published results but in an interview given in 2
012 he expressed his intention to return to this project in the future and
explained a possible role of Univalent Foundations in it. \n\nIn this tal
k based on archival sources I reconstruct Voevodsky’s original strategy
of bridging pure and applied mathematics\, illustrate it with some example
s\, and argue that Applied Univalent Foundations is a viable research prog
ram. \n\n[1] Andrei Rodin\, Voevodsky’s Unfinished Project: Bridging the
Gap between Pure and Applied Mathematics\, BioSystems\, 204 (2021)\, 1043
91\; preprint arXiv : 2012.01150\n\n[2] UniMath Library : https://github.c
om/UniMath/UniMath\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alexandre Miquel
DTSTART;VALUE=DATE-TIME:20221208T170000Z
DTEND;VALUE=DATE-TIME:20221208T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/78
DESCRIPTION:Title: Implicative algebras: a new foundation for realiz
ability and forcing\nby Alexandre Miquel as part of Topos Institute Co
lloquium\n\n\nAbstract\nIn this talk\, I will present implicative algebras
\, a simple algebraic\nstructure generalizing complete Heyting algebras an
d abstract Krivine\nstructures\, and based on a surprising identification
between the\nnotions of a realizer and of a type. I will show that this s
tructure\nnaturally induces a family of triposes - the implicative tripose
s -\nthat encompass all triposes known so far\, namely: Heyting triposes\,
\nBoolean triposes\, intuitionistic realizability triposes and classical\n
realizability triposes\, thus providing a unified framework for\nexpressin
g forcing and realizability\, both in intuitionistic and\nclassical logic.
Finally\, I will discuss about some recent\ncompleteness results about th
e very notion of implicative model\, both\nin higher-order logic and first
-order logic.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paige North
DTSTART;VALUE=DATE-TIME:20230202T170000Z
DTEND;VALUE=DATE-TIME:20230202T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/79
DESCRIPTION:Title: Fuzzy type theory\nby Paige North as part of
Topos Institute Colloquium\n\n\nAbstract\nIn this talk\, I will report on
progress developing a fuzzy type theory\, a project that started as part o
f the ACT 2022 Adjoint School. The motivation is to develop a logic which
can model opinions\, and we do this by generalizing Martin-Löf type theor
y. Martin-Löf type theory provides a system in which one can construct a
proof (aka a term) of a proposition (aka a type)\, and we usually interpre
t such a term as saying that the proposition holds. Fuzzy type theory is a
similar system in which one can provide or construct evidence (aka a fuzz
y term) to support an opinion (aka a type)\, but the evidence (fuzzy term)
comes with a parameter\, for instance a real number between 0 and 1\, whi
ch expresses to what extent the opinion holds. Martin-Löf type theory is
closely related to category theory: from such a type system one can constr
uct a category in which (very roughly) the types become objects and the te
rms become morphisms\, and this can be made part of an equivalence. Thus\,
we base our development of fuzzy type theory to be the thing which corres
ponds to categories enriched in a category of fuzzy sets in the same way t
hat Martin-Löf type theory corresponds to categories (enriched in sets).\
n\nThis is joint work with Shreya Arya\, Greta Coraglia\, Sean O’Connor\
, Hans Riess\, and Ana Tenório.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Prakash Panangaden
DTSTART;VALUE=DATE-TIME:20230209T170000Z
DTEND;VALUE=DATE-TIME:20230209T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/83
DESCRIPTION:Title: Nuclear ideals in monoidal *-categories\nby P
rakash Panangaden as part of Topos Institute Colloquium\n\n\nAbstract\nThi
s talk is based on 25-year old material developed in joint work with Samso
n Abramsky\nand Richard Blute. I hope that this talk will stimulate other
s (any myself) to look at\nthese topics in light on modern developments.
Our goal was to develop quantitative\nanalogues of the concept of binary r
elations. In particular\, we were interested in\nfinding a suitable defin
ition of probabilistic relations.\n\nThe formulation that we came up with
arose by generalizing the notion of nuclear maps from\nfunctional analysis
by defining nuclear ideals in monoidal *-categories. The compact\nclosed
structure associated with the category of relations does not generalize d
irectly\,\ninstead one obtains nuclear ideals.\n\nMany such categories hav
e a large class of morphisms which behave as if they were part of\na compa
ct closed category\, i.e. they allow one to transfer variables between the
domain\nand the codomain. We introduce the notion of nuclear ideals to a
nalyze these classes of\nmorphisms. In compact closed categories all morp
hisms are nuclear\, and in the category of\nHilbert spaces\, the nuclear m
orphisms are the Hilbert-Schmidt maps.\n\nWe also introduce two new exampl
es of monoidal *-categories\, in which integration plays\nthe role of comp
osition. In the first\, morphisms are a special class of distributions\,\n
which we call tame distributions. The second example is based on measure
and probability\nand serves as a possible candidate for probabilistic rela
tions.\n\nSince our original paper was published\, other examples of this
phenomenon were discovered.\nWe also explored concepts associated with tra
ce ideals\, I will briefly talk about these.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sergey Goncharov
DTSTART;VALUE=DATE-TIME:20230216T170000Z
DTEND;VALUE=DATE-TIME:20230216T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/84
DESCRIPTION:Title: Towards a Higher-Order Mathematical Operational S
emantics\nby Sergey Goncharov as part of Topos Institute Colloquium\n\
n\nAbstract\nCompositionality proofs in higher-order languages are notorio
usly involved\, and general \nsemantic frameworks guaranteeing composition
ality are hard to come by. In particular\, Turi and Plotkin’s \nbialgebr
aic abstract GSOS framework\, which has been successfully applied to obtai
n off-the-shelf \ncompositionality results for first-order languages\, so
far did not apply to higher-order languages. I \nwill present a recently e
merged development of the theory of abstract GSOS specifications for \nhig
her-order languages\, in effect transferring the core principles of Turi a
nd Plotkin’s framework to a \nhigher-order setting. In the present frame
work\, the operational semantics of higher-order languages is \nrepresente
d by certain dinatural transformations\, we dub **higher-order GSOS laws<
/b>. I will present a \ngeneral compositionality result w.r.t. the strong
variant of Abramsky’s applicative bisimilarity that \napplies to all sys
tems specified in this way. For presentation purposes\, I will stick to a
variant of \nthe combinatory logic\, as a main vehicle.\n\nThe talk is bas
ed on a recent POPL'23 paper\, which is a joint work with: Stefan Milius\,
Lutz Schröder\, \nStelios Tsampas\, and Henning Urbat.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Justin Curry
DTSTART;VALUE=DATE-TIME:20230302T170000Z
DTEND;VALUE=DATE-TIME:20230302T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/85
DESCRIPTION:Title: Algebraic and Geometric Models for Space Networki
ng\nby Justin Curry as part of Topos Institute Colloquium\n\n\nAbstrac
t\nIn this talk I will describe recent and ongoing work dedicated to devel
oping scalable autonomous routing protocols for a future solar system wide
internet. At the heart of the talk will be a description of a new coordin
ate system (based on cosheaves and persistence) for time-varying graphs. I
n this new coordinate system\, we can describe distances between various s
pace networking scenarios\, as well as model routing (with propagation del
ay) using matrix multiplication in a modified coefficient system valued in
semi-rings. To demonstrate these models in practice\, we use simulations
of Earth-Moon-Mars systems generated in SOAP (Satellite Orbital Analysis P
rogram) ranging from 10s to 100s of nodes in size. These simulations are p
art of a growing codebase being developed by SUNY Albany and NASA Glenn Re
search Center under the TIMAEUS project.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Urs Schreiber
DTSTART;VALUE=DATE-TIME:20230413T170000Z
DTEND;VALUE=DATE-TIME:20230413T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/87
DESCRIPTION:Title: Effective Quantum Certification via Linear Homoto
py Types\nby Urs Schreiber as part of Topos Institute Colloquium\n\n\n
Abstract\nThe intricacies of realistic — namely: of classically controll
ed and (topologically) error-protected — quantum algorithms arguably mak
e computer-assisted verification a practical necessity\; and yet a satisfa
ctory theory of dependent quantum data types had been missing\, certainly
one that would be aware of topological error-protection.\n\nTo solve this
problem we present Linear homotopy type theory (LHoTT) as a programming an
d certification language for quantum computers with classical control and
topologically protected quantum gates\, focusing on (1.) its categorical s
emantics\, which is a homotopy-theoretic extension of that of Proto-Quippe
r and a parameterized extension of Abramsky et al.'s quantum protocols\, (
2.) its expression of quantum measurement as a computational effect induce
d from dependent linear type formation and reminiscent of Lee at al.'s dyn
amic lifting monad but recovering the interacting systems of Coecke et al.
's "classical structures" monads.\n\nNamely\, we have recently shown that
classical dependent type theory in its novel but mature full-blown form of
Homotopy Type Theory (HoTT) is naturally a certification language for rea
listic topological logic gates. But given that categorical semantics of Ho
TT is famously provided by parameterized homotopy theory\, we had argued e
arlier [Sc14] for a quantum enhancement LHoTT of classical HoTT\, now with
semantics in parameterized stable homotopy theory. This linear homotopy t
ype theory LHoTT has meanwhile been formally described\; here we explain i
t as the previously missing certified quantum language with monadic dynami
c lifting\, as announced in.\n\nConcretely\, we observe that besides its s
upport\, inherited from HoTT\, for topological logic gates\, LHoTT intrins
ically provides a system of monadic computational effects which realize wh
at in algebraic topology is known as the ambidextrous form of Grothendieck
’s "Motivic Yoga"\; and we show how this naturally serves to code quantu
m circuits subject to classical control implemented via computational effe
cts. Logically this emerges as a linearly-typed quantum version of epistem
ic modal logic inside LHoTT\, which besides providing a philosophically sa
tisfactory formulation of quantum measurement\, makes the language validat
e the quantum programming language axioms proposed by Staton\; notably the
deferred measurement principle is verified by LHoTT.\n\nFinally we indica
te the syntax of a domain-specific programming language QS (an abbreviatio
n both for "Quantum Systems" and for "QS^0 -modules" aka spectra) which su
gars LHoTT to a practical quantum programming language with all these feat
ures\; and we showcase QS-pseudocode for simple forms of key algorithm cla
sses\, such as quantum teleportation\, quantum error-correction and repeat
-until-success quantum gates.\n\n(This is joint work with D. J. Myers\, M.
Riley and H. Sati. Slides will be available at: ncatlab.org/schreiber/sho
w/Quantum+Certification+via+Linear+Homotopy+Types)\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Corfield
DTSTART;VALUE=DATE-TIME:20230309T170000Z
DTEND;VALUE=DATE-TIME:20230309T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/88
DESCRIPTION:Title: Philosophical perspectives on category theory
\nby David Corfield as part of Topos Institute Colloquium\n\n\nAbstract\nF
or the whole length of my academic career\, I have looked to make philosop
hical sense of (higher) category theory. My earliest interests concerned c
ategory theory as a new structuralist foundational language for mathematic
s and for mathematical physics. Later at the n-Category Café there were a
lso attempts to make category-theoretic sense of probability theory\, lear
ning theory and diagrammatic reasoning. Today\, alongside successes in log
ic\, mathematics and physics\, we find a flourishing world of applied cate
gory theory\, involving work in probability theory\, causal reasoning\, le
arning theory\, natural language processing\, and so on. These are all top
ics of profound interest to philosophy. In this talk\, I will discuss ways
in which philosophy can come into a fruitful relationship with category t
heory.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christina Vasilakopoulou
DTSTART;VALUE=DATE-TIME:20230323T170000Z
DTEND;VALUE=DATE-TIME:20230323T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/89
DESCRIPTION:Title: Dual algebraic structures and enrichment\nby
Christina Vasilakopoulou as part of Topos Institute Colloquium\n\n\nAbstra
ct\nIn this talk\, we will provide a detailed overview of the sometimes ca
lled “Sweedler theory” for algebras and modules. This begins by establ
ishing an enrichment of the category of algebras in the category of coalge
bras\, as well as an enrichment of a global category of modules in a globa
l category of comodules\, giving rise to a structure described as an enric
hed fibration. Moreover\, by investigating a many-object generalization in
volving categories and modules\, we will discuss further directions and ap
plications of this framework to operadic structures.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Simon Willerton
DTSTART;VALUE=DATE-TIME:20230330T170000Z
DTEND;VALUE=DATE-TIME:20230330T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/90
DESCRIPTION:Title: Metric spaces\, entropic spaces and convexity
\nby Simon Willerton as part of Topos Institute Colloquium\n\n\nAbstract\n
A certain notion of convexity of sets can be captured by a monad\, known a
s a convexity monad or barycentric monad\; this is a finite version of so-
called probability monads. Various authors (including Mardare-Panangaden-
Plotkin\, and Fritz-Perrone) have looked at convexity/probability monads o
n categories of metric spaces. The work of Fritz-Perrone can be recast in
terms of enriched categories if you consider metric spaces as categories e
nriched over the quantale of extended non-negative real numbers.\n\nOne ca
n then do a similar thing for any 'suitably convex' quantale R and define
a convexity monad on the category of R-categories. In particular\, if R i
s the extended real line [-oo. oo] with the opposite order to that used in
metric spaces\, then R-categories are what Lawvere called 'entropic space
s' and argued gave a necessary structure for state spaces in thermodynamic
s. The category of strict algebras with lax algebra maps for the convexity
monad in this case is the category of convex entropic spaces with concave
maps. The hope is that this connects the Lawvere approach to thermodynam
ics with the recent approach of Baez-Lynch-Moeller which involves convex s
paces and concave maps (without the entropic structure).\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Davide Trotta
DTSTART;VALUE=DATE-TIME:20230420T170000Z
DTEND;VALUE=DATE-TIME:20230420T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/91
DESCRIPTION:Title: Generalized existential completions and applicati
ons\nby Davide Trotta as part of Topos Institute Colloquium\n\n\nAbstr
act\nThis talk presents an overview of the "generalized existential comple
tion" of Lawvere doctrines and its applications. I present this constructi
on that freely adds (generalized) existential quantifiers to a given doctr
ine and I will provide an intrinsic characterization of this notion based
on an algebraic description of the logical concept of existential-free for
mulas.\nThis characterization provides a useful tool to recognize a wide v
ariety of examples of doctrines arising as generalized existential complet
ions. These include the subobjects doctrine and the weak subobjects doctri
ne as well all realizability triposes and\, among localic triposes\, only
the supercoherent ones.\n\nI will also present some applications of the co
nstruction to the dialectica interpretation\, showing how our algebraic de
scription of quantifier-free formulas allows us to prove that the logical
principles involved in the dialectica interpretation are satisfied in the
categorical setting\, establishing a tight correspondence between the logi
cal system and the categorical framework given by dialectica doctrines.\n\
nThis talk is based on the following works:\n\n- Maria Emilia Maietti\, Da
vide Trotta (2023). A characterization of generalized existential completi
ons. In Annals of Pure and Applied Logic.\n\n- Davide Trotta\, Matteo Spad
etto\, Valeria de Paiva (2023). Dialectica principles via Gödel doctrines
. In Theoretical Computer Science.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Georges Gonthier
DTSTART;VALUE=DATE-TIME:20230427T170000Z
DTEND;VALUE=DATE-TIME:20230427T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/92
DESCRIPTION:Title: Foothills and cathedrals: organising the librarie
s behind big proofs\nby Georges Gonthier as part of Topos Institute Co
lloquium\n\n\nAbstract\nWhile mathematics is amongst the best organized fo
rms of knowledge\, the level of detail of computer-assisted formal mathema
tics demands an even higher degree of structuring. The cathedrals that are
the computer proofs of famous results such as the Four Color or the Odd O
rder theorems rest on the foothills of large\, architected libraries of pr
erequisites\, ranging from the trivial and elementary to undergraduate and
graduate curricula. While these can often be crafted to resemble traditio
nal course material\, the extra attention to detail also motivates differe
nces\, some examples of which we will highlight.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michael Barany
DTSTART;VALUE=DATE-TIME:20230504T170000Z
DTEND;VALUE=DATE-TIME:20230504T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/93
DESCRIPTION:Title: How Categories Come to Matter: On the history and
sociology of categories in modern mathematics\nby Michael Barany as p
art of Topos Institute Colloquium\n\n\nAbstract\nI will situate categories
and related mathematical principles in the history of modern mathematics
from the late nineteenth century to the present. The worldviews and perspe
ctives adopted by the Topos Institute derive from specific transformations
in the nature and scale of mathematical research over the last century-an
d-a-bit. These connect the ideas of modern mathematics to its people\, ins
titutions\, and infrastructures. I will consider two main senses in which
categories "come to matter": first\, how categories of various kinds becam
e meaningful\, salient\, and important as ways of seeing the mathematical
world and and the worlds of mathematicians\; and second\, how such categor
ies were encoded\, translated\, reproduced\, and made to move on and acros
s various kinds of material media (i.e. physical matter) such as blackboar
ds\, index cards\, and printed journals. I contend that these two senses a
re historically connected\, in ways that relate to the continuing goals an
d challenges of the Topos community.\n
LOCATION:
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:20240803T044943Z
UID:ToposInstituteColloquium/94
DESCRIPTION:Title: Category theory outreach panel\nby Riehl\, Br
adley\, Cheng\, Dancstep\, and Lugg as part of Topos Institute Colloquium\
n\n\nAbstract\nCategory theory is a wonderful subject\, deep and broad\, s
panning the breadth of mathematics and having applications throughout scie
nce\, engineering\, technology\, and the arts. But for people outside of a
cademia\, it can be a difficult subject to learn. Topos Institute is hosti
ng a panel discussion\, moderated by Emily Riehl\, featuring panelists who
are actively involved in producing category theory books and videos for a
non-expert audience. The panellists will discuss their philosophy and tec
hniques\, and provide support and encouragement for others to join in this
important work. They will also take questions from viewers to help people
get a better handle on how they may begin to learn the subject and to hel
p category theorists understand what they can do to facilitate this proces
s.\n\nFor more information\, including how to submit questions\, please se
e https://topos.site/ct-outreach-self-learners/\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chad Giusti
DTSTART;VALUE=DATE-TIME:20230511T170000Z
DTEND;VALUE=DATE-TIME:20230511T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/95
DESCRIPTION:Title: Toward a useful category for persistent homology<
/a>\nby Chad Giusti as part of Topos Institute Colloquium\n\n\nAbstract\nP
ersistent homology is the central tool in modern applied topology. Briefly
\, given a (finite) sample from a distribution on a topological space embe
dded in a metric space\, one builds a multi-scale combinatorial representa
tion of the sample called a filtered Vietoris-Rips complex. Applying homol
ogy\, we summarize this multi-scale structure as an object called a persis
tence module. When the samples come from real-world data\, practitioners a
pply domain knowledge and ad hoc reasoning to understand how the persisten
ce module reflects organizational principles of the system of interest.\n\
nIf we wish to formalize this reasoning process\, or apply more sophistica
ted methods from algebraic topology to data analysis\, a first step is to
develop a notion of functoriality for persistent homology. This pipeline i
nherits the usual functoriality of homology\, taking maps of simplicial co
mplexes to maps on persistence modules\, and substantial progress has been
made in cycle registration\, a formalism for comparing persistence module
s using this structure. However\, in practice one usually compares samples
from unknown spaces\; there are relatively few settings where the require
d map of the combinatorial encodings (or underlying spaces) is likely to b
e known. In this talk\, we describe our recent efforts to develop techniqu
es that provide a notion of "induced map" using the kind of data reasonabl
y available in applied settings\, and the challenges that remain in develo
ping a full categorical framework for applied topology. Various parts of t
his work are joint with Iris Yoon\, Robert Ghrist\, Niko Schonsheck\, Greg
ory Henselman-Petrusek\, and Lori Ziegelmeier\, amongst others.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Elaine Landry
DTSTART;VALUE=DATE-TIME:20230525T170000Z
DTEND;VALUE=DATE-TIME:20230525T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/96
DESCRIPTION:Title: As If Category Theory were a Foundation\nby E
laine Landry as part of Topos Institute Colloquium\n\n\nAbstract\nThe aim
of this talk is to show that when we shift our focus from solving philosop
hical problems to solving mathematical ones\, we see that an as-if interpr
etation of mathematics can be used to provide an account of both the pract
ice and the applicability of mathematics. I begin first with Plato to show
that much philosophical milk has been spilt owing to our conflating the m
ethod of mathematics with the method of philosophy. I then use my reading
of Plato to develop what I call as-ifism\, the view that\, in mathematics\
, we treat our hypotheses as if they were true first principles and we do
this with the purpose of solving mathematical problems not philosophical o
nes. I next extend as-ifism to modern mathematics wherein the method of ma
thematics becomes the axiomatic method\, noting that this engenders a shif
t from as-if hypotheses to as-if axioms. I next distinguish as-ifism from
if-thenism\, and use this to develop my structural as-ifist position. I en
d by showing that taking a methodological as-ifist route\, by placing our
focus on what is needed for the practice and applicability of mathematics\
, we are neither committed to the unconditional consistency of our mathema
tical axioms nor the unconditional truth of our background meta-mathematic
al theory. Simply\, it is methodological considerations\, and not metaphys
ical ones\, that “condition” our as if assumptions of both the consist
ency of our mathematical axioms and the truth of our background meta-mathe
matical theory. Finally\, I use my methodological as-ifism to reconsider t
he “foundations debate”\, specifically\, that between set theory and c
ategory theory.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tom Hirschowitz
DTSTART;VALUE=DATE-TIME:20230608T170000Z
DTEND;VALUE=DATE-TIME:20230608T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/97
DESCRIPTION:Title: Abstraction in programming language theory: Howe'
s method\nby Tom Hirschowitz as part of Topos Institute Colloquium\n\n
\nAbstract\nResearch in programming languages mostly proceeds language by\
nlanguage. This in particular means that key ideas are often introduced\nf
or one typical language\, and must then be adapted to other languages.\n\n
A prominent example of this is Howe's method for proving that\napplicative
bisimilarity\, a notion of program equivalence in\ncall-by-name λ-calcul
us\, is a congruence. This method has been adapted\nto call-by-value λ-ca
lculus\, PCF\, λ-calculus with delimited\ncontinuations\, higher-order π
-calculus\,…\n\nIn this work\, using category theory\, we establish an a
bstract congruence\ntheorem for applicative bisimilarity\, of which most e
xisting adaptations\nof Howe's method are instances.\n\nThis is joint work
with Ambroise Lafont.\n\nSee also Ugo Dal Lago\, Francesco Gavazzo\, and
Paul Levy. Effectful applicative bisimilarity: Monads\, relators\, and How
e’s method. LICS 2017. Extended version: https://arxiv.org/abs/1704.0464
7 .\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Taco Cohen
DTSTART;VALUE=DATE-TIME:20230615T170000Z
DTEND;VALUE=DATE-TIME:20230615T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/98
DESCRIPTION:Title: Categorical Causality & Systems Theory\nby Ta
co Cohen as part of Topos Institute Colloquium\n\n\nAbstract\nCategorical
Systems theory is a general framework for modelling systems whose state ev
olves depending on some inputs or actions\, and which produce some observa
ble outputs. This framework is general enough to describe arbitrary classi
cal physical systems\, and generalizes the Partially Observed Markov Decis
ion Process commonly used in AI. Causal models\, formalized as string diag
rams in CD-categories\, provide a convenient high-level framework for reas
oning about how intervening on some outcome variables would affect others.
In this talk I will provide a high-level introduction to both frameworks\
, and discuss their relations. In particular we ask when a system can be a
ccurately described by a causal model\, and show that this is not generall
y possible\, thus highlighting the limitations of existing causal modellin
g frameworks.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Clark Barrett
DTSTART;VALUE=DATE-TIME:20230518T170000Z
DTEND;VALUE=DATE-TIME:20230518T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/99
DESCRIPTION:Title: Proof Certificates in Satisfiability Modulo Theor
ies\nby Clark Barrett as part of Topos Institute Colloquium\n\n\nAbstr
act\nSatisfiability modulo theories (SMT) is an automated reasoning paradi
gm that can automatically prove a wide variety of first-order logic theore
ms relating to theories that commonly occur when reasoning about computer
systems (e.g.\, arithmetic\, arrays\, strings\, etc.). Together with my c
olleagues at U Iowa\, Bar-Ilan\, and UF Minas Gerais\, we have for the pas
t few years been developing a way to produce proof certificates from the c
vc5 SMT solver. These proof certificates provide enough detail to allow a
n independent proof checker to confirm the correctness of the theorem prov
ed. The obvious benefit is that this drastically reduces the code that mu
st be trusted to ensure correct results. A less obvious benefit is that p
roof certificates open up the possibility of integrating SMT solvers into
skeptical proof assistants such as Coq\, Isabelle/HOL\, or Lean. In this
talk\, I will give an overview of the proof production and proof checking
mechanisms we are developing for cvc5 and explain how we are leveraging th
ese to provide trusted SMT automation in proof assistants.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Martsinkovsky
DTSTART;VALUE=DATE-TIME:20230601T170000Z
DTEND;VALUE=DATE-TIME:20230601T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/100
DESCRIPTION:Title: How to interpret cotorsion\nby Alex Martsink
ovsky as part of Topos Institute Colloquium\n\n\nAbstract\nTwo important f
eatures of a linear control system are its controllability and observabili
ty. \nFrom the algebraic prospective\, a system is a module over a ring of
differential operators (with constant\, polynomial\, or analytic coeffic
ients). The part of the system that cannot be controlled \nis called the a
utonomy of the system. In the algebraic language\, this is just the torsio
n submodule \nof the module. Thus the controllable part is described by th
e torsion-free quotient of the module. \n\nThere is a duality between the
controllability of the system and the observability of the dual \nsystem.
The goal of this talk is to propose a conjectural algebraic analog of the
observability\, \ncalled cotorsion. As a justification for the conjecture\
, we will see a duality between cotorsion \nand torsion\, effected by the
Auslander-Gruson-Jensen functor. The latter seems to be a \nrecurring them
e\, found in a variety of functor categories. It is to be hoped that\, des
pite the \nalgebraic nature of this talk\, the non-algebraic members of th
e audience would recognize \nfamiliar (enriched) categorical patterns.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jared Culbertson
DTSTART;VALUE=DATE-TIME:20230622T170000Z
DTEND;VALUE=DATE-TIME:20230622T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/101
DESCRIPTION:Title: Applying Categorical Thinking to Practical Domai
ns\nby Jared Culbertson as part of Topos Institute Colloquium\n\n\nAbs
tract\nEmbracing a categorical perspective has proven to be a useful way t
o formalize many intuitive and ad hoc compositional approaches across a di
verse set of practical fields. In this talk\, we will discuss work in thre
e primary domains including probabilistic modeling\, hierarchical clusteri
ng\, and robotics. After briefly surveying prior work in the first two\, w
e will focus on formalizing what it means to "apply a behavior" in a very
concrete context of legged robots whose controllers are modeled as hybrid
dynamical systems. Central to this approach is developing a common framewo
rk for describing (i) sequential composition of hybrid systems (enabled by
a cospan description of interfaces and a generalization of Conley's (epsi
lon\,T)-chains to the hybrid setting)\; (ii) transformations of hybrid sys
tems (modeled as hybrid semiconjugacies and integrated with sequential com
position via a double category)\; and (iii) hierarchical composition of hy
brid systems (where hybrid subdivisions satisfying a certain fiber product
condition enable composing spans of template/anchor pairs). Throughout\,
we will highlight some specific practical lessons that were learned in app
lying categorical formalisms to these real-world problem domains.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nathaniel Osgood
DTSTART;VALUE=DATE-TIME:20230629T170000Z
DTEND;VALUE=DATE-TIME:20230629T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/103
DESCRIPTION:Title: Towards Compositional System Dynamics for Public
Health\nby Nathaniel Osgood as part of Topos Institute Colloquium\n\n
\nAbstract\nFor decades\, System Dynamics (SD) modeling has served as a pr
ominent\, diagram-centric methodology used for public health modeling. Muc
h of its strength arises from its versatile use of 3 types of diagrams\, w
ith each serving both to elevate transparency across the interdisciplinary
teams responsible for most impactful models\, and to reason about pattern
s of system behavior. Causal loop diagrams (CLDs) are used in semi-qualita
tive processes early in the modeling process and seek to support insight i
nto feedback structure\, behavioral modes\, and leverage points. As model
ing proceeds\, system structure diagrams further distinguish stocks (accum
ulations) from flows and material from informational dependencies. Stock &
flow diagrams build on that representation to characterize mathematical d
ependencies\, quantify parameters and initial values for stocks\, and have
been particularly widely used in scenario simulation in public health and
mathematical epidemiology. While ubiquitous use of diagrams renders SD m
odeling markedly effective in supporting team science and shaping stakehol
ders’ mental models\, existing tools suffer from a number of shortcoming
s. These include poor support for modularity\, cumbersome and obscurant m
odel stratification\, and an inability to capture the relationships betwee
n the 3 diagram types. Within this talk\, we describe initial progress tow
ards creating a framework for compositional System Dynamics\, including th
eory\, API support via StockFlow.jl within AlgebraicJulia\, and ModelColla
b -- a real-time collaborative tool to support interdisciplinary teams in
modularly building\, composing and flexibly analyzing Stock & Flow diagram
s. Our approach separates syntax from semantics\, and characterizes diagra
ms using copresheaves with a schema category. Diagram composition draws on
the theory of structured cospans and undirected wiring diagrams\, and emp
loys pullbacks for model stratification. Model interpretation is achieved
via functorial semantics\, with ordinary differential equations being just
one of several semantic domains supported. After describing the current s
tate of implementation\, we describe plans for future work\, including enr
iching support for CLDs\, and adding support for several computational sta
tistics algorithms and additional types of structurally-informed model ana
lyses. This is joint work with John Baez\, Evan Patterson\, Nicholas Mead
ows\, Sophie Libkind\, Alex Alegre and Eric Redekopp.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Urs Schreiber
DTSTART;VALUE=DATE-TIME:20230824T170000Z
DTEND;VALUE=DATE-TIME:20230824T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/104
DESCRIPTION:Title: Quantum Programming via Linear Homotopy Types\nby Urs Schreiber as part of Topos Institute Colloquium\n\n\nAbstract\nT
he intricacies of realistic — namely: of classically controlled and\n(to
pologically) error-protected — quantum algorithms arguably make\ncompute
r-assisted verification a practical necessity\; and yet a\nsatisfactory th
eory of dependent quantum data types had been missing\,\ncertainly one tha
t would be aware of topological error-protection.\n\nTo solve this problem
we present Linear homotopy type theory (LHoTT)\nas a programming and cert
ification language for quantum computers with\nclassical control and topol
ogically protected quantum gates\, focusing\non (1.) its categorical seman
tics\, which is a homotopy-theoretic\nextension of that of Proto-Quipper a
nd a parameterized extension of\nAbramsky et al.'s quantum protocols\, (2.
) its expression of quantum\nmeasurement as a computational effect induced
from dependent linear\ntype formation and reminiscent of Lee at al.‘s d
ynamic lifting monad\nbut recovering the interacting systems of Coecke et
al.‘s "classical\nstructures" monads.\n\nNamely\, we have recently shown
that classical dependent type theory in\nits novel but mature full-blown
form of Homotopy Type Theory (HoTT) is\nnaturally a certification language
for realistic topological logic\ngates. But given that categorical semant
ics of HoTT is famously\nprovided by parameterized homotopy theory\, we ha
d argued earlier\n[Sc14] for a quantum enhancement LHoTT of classical HoTT
\, now with\nsemantics in parameterized stable homotopy theory. This linea
r\nhomotopy type theory LHoTT has meanwhile been formally described\; here
\nwe explain it as the previously missing certified quantum language\nwith
monadic dynamic lifting\, as announced in.\n\nConcretely\, we observe tha
t besides its support\, inherited from HoTT\,\nfor topological logic gates
\, LHoTT intrinsically provides a system of\nmonadic computational effects
which realize what in algebraic topology\nis known as the ambidextrous fo
rm of Grothendieck’s “Motivic Yoga”\;\nand we show how this naturall
y serves to code quantum circuits subject\nto classical control implemente
d via computational effects. Logically\nthis emerges as a linearly-typed q
uantum version of epistemic modal\nlogic inside LHoTT\, which besides prov
iding a philosophically\nsatisfactory formulation of quantum measurement\,
makes the language\nvalidate the quantum programming language axioms prop
osed by Staton\;\nnotably the deferred measurement principle is verified b
y LHoTT.\n\nFinally we indicate the syntax of a domain-specific programmin
g\nlanguage QS (an abbreviation both for “Quantum Systems” and for “
QS^0\n-modules” aka spectra) which sugars LHoTT to a practical quantum\n
programming language with all these features\; and we showcase\nQS-pseudoc
ode for simple forms of key algorithm classes\, such as\nquantum teleporta
tion\, quantum error-correction and\nrepeat-until-success quantum gates.\n
\n(This is joint work with D. J. Myers\, M. Riley and H. Sati.\nSlides wil
l be available at:\nncatlab.org/schreiber/show/Quantum+Certification+via+L
inear+Homotopy+Types)\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jonathan Sterling
DTSTART;VALUE=DATE-TIME:20230928T170000Z
DTEND;VALUE=DATE-TIME:20230928T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/105
DESCRIPTION:Title: Synthetic Domains in the 21st Century\nby Jo
nathan Sterling as part of Topos Institute Colloquium\n\n\nAbstract\nIt is
easy to teach a student how to give a naïve denotational semantics to a
typed lambda calculus without recursion\, and then use it to reason about
the equational theory: a type might as well be a set\, and a program might
as well be a function\, and equational adequacy at base type is establish
ed using a logical relation between the initial model and the category of
sets. Adding any non-trivial feature to this language (e.g. general recurs
ion\, polymorphism\, state\, etc.) immediately increases the difficulty be
yond the facility of a beginner: to add recursion\, one must replace sets
and functions with domains and continuous maps\, and to accommodate polymo
rphism and state\, one must pass to increasingly inaccessible variations o
n this basic picture.\n\nThe dream of the 1990s was to find a category tha
t behaves like SET in which even general recursive and effectful programmi
ng languages could be given naïve denotational semantics\, where types ar
e interpreted as “sets” and programs are interpreted as a “functions
”\, without needing to check any arduous technical conditions like conti
nuity. The benefit of this synthetic domain theory is not only that it loo
ks “easy” for beginners\, as more expert-level constructions like powe
rdomains or even domain equations for recursively defined semantic worlds
become simple and direct. Although there have been starts and stops\, the
dream of synthetic domain theory is alive and well in the 21st Century. To
day’s synthetic domain theory is\, however\, both more modular and more
powerful than ever before\, and has yielded significant results in program
ming language semantics including simple denotational semantics for an sta
te of the art programming language with higher-order polymorphism\, depend
ent types\, recursive types\, general reference types\, and first-class mo
dule packages that can be stored in the heap.\n\nIn this talk\, I will exp
lain some important classical results in synthetic domain theory as well a
s more recent results that illustrate the potential impact of “naïve de
notational semantics” on the life of a workaday computer scientist.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nat Shankar
DTSTART;VALUE=DATE-TIME:20230831T170000Z
DTEND;VALUE=DATE-TIME:20230831T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/106
DESCRIPTION:Title: Abstraction Engineering with the Prototype Verif
ication System (PVS)\nby Nat Shankar as part of Topos Institute Colloq
uium\n\n\nAbstract\nLogic has always played a central role in computing.
One successful\napplication of logic is its use in specifying and modeling
\ncomputational behavior\, and in proving properties of computation\nsyste
ms. SRI's PVS was released thirty years ago with the goal of\ndemocratizi
ng interactive theorem proving by combining an expressive\nformalism with
powerful automated reasoning tools for building and\nmaintaining complex f
ormalizations and proofs. We describe some of\nthe features of PVS for de
fining and reasoning with mathematical\nabstractions and bridging the gap
between informal and formalized\nmathematical discourse. PVS features an
expressive-order logic with\nalgebraic/coalgebraic datatypes\, dependent p
redicate subtypes\, and\nparametric theories. The interactive theorem pro
ver employs a range\nof automated proof strategies for simplification\, re
writing\, and case\nanalysis\, along with built-in decision procedures for
SAT and SMT\nsolving. The applicative fragment of PVS can be viewed as a
\nfunctional programming language\, and efficient executable code can be\n
generated in Common Lisp and C\, among other languages. PVS includes\next
ensive libraries spanning a range of topics in mathematics and\ncomputing.
The talk is an informal overview of the underlying\ntheoretical foundati
ons\, and the proof and code generation\ncapabilities of PVS.\n\nBio: Dr.
Natarajan Shankar is a Distinguished Senior Scientist and SRI\nFellow at t
he SRI Computer Science Laboratory. He received a\nB.Tech. degree in Elec
trical Engineering from the Indian Institute of\nTechnology\, Madras\, and
Ph.D. in Computer Science from the University\nof Texas at Austin. He is
the author of the book\, "Metamathematics\,\nMachines\, and Godel's Proof
"\, published by Cambridge University Press.\nDr. Shankar is the co-develo
per of a number of technologies including\nthe PVS interactive proof assis
tant\, the SAL model checker\, the Yices\nSMT solver\, and the Arsenal sem
antic parser. He is a co-recipient of\nthe 2012 CAV Award and the recipie
nt of the 2022 Herbrand Award.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Brandon Shapiro
DTSTART;VALUE=DATE-TIME:20231102T170000Z
DTEND;VALUE=DATE-TIME:20231102T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/107
DESCRIPTION:Title: (Higher) category theory in Cat^#\nby Brando
n Shapiro as part of Topos Institute Colloquium\n\n\nAbstract\nThe double
category Cat^#\, which can be built out of polynomial comonads\, provides
a computation-friendly mathematical language for categorical database theo
ry\, effects handlers in programming\, and discrete open dynamical systems
. It has categories as objects\, cofunctors as arrows\, and prafunctors as
pro-arrows. Monads among prafunctors\, such as the free category monad on
graphs\, have algebras including categories\, n-categories (strict or wea
k)\, double categories\, multicategories (symmetric or plain)\, monoids\,
monoidal categories (of nearly any variety)\, and in fact any algebraic no
tion of higher category whose definition is of a particular form. I will i
ntroduce the Cat^# approach to defining (higher) categories and survey som
e constructions from (higher) category theory that can be expressed in the
language of Cat^#\, including higher categorical nerves and "algebraic pr
afunctors" such as the free monoidal category monad on Cat.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Simona Paoli
DTSTART;VALUE=DATE-TIME:20231019T170000Z
DTEND;VALUE=DATE-TIME:20231019T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/108
DESCRIPTION:Title: Simplicial delta versus fat delta in higher cate
gory theory\nby Simona Paoli as part of Topos Institute Colloquium\n\n
\nAbstract\nMany structures in higher category theory have been described
using the combinatorics of simplicial objects\, based on the category simp
licial delta. A prototype example is that a category can be described as a
simplicial set satisfying appropriate conditions (the so called Segal con
ditions) via the nerve functor.\nIn dimension two\, simplicial objects in
Cat can be used to describe strict 2-categories and double categories. Amo
ng the latter\, one can identity the category of weakly globular double ca
tegories which gives a model of weak 2-categories via a new paradigm to we
aken higher categorical structures: the notion of weak globularity.\nThe f
at delta\, introduced by Joachim Kock\, carries some intuition similar to
the simplicial delta\, yet it has a different and rich structure. Kock use
d it to define fair 2-categories\, encoding weak 2-categories with strict
composition laws.\nIn this talk I illustrate a direct comparison between f
air 2-categories and weakly globular double categories which enables to in
terpret the weak globularity condition in terms of weak units. This compar
ison is based on a rich interplay between the simplicial delta and the fat
delta\, and on several novel properties of the latter.\nI will finally ex
plain the significance of this result in terms of potential higher dimensi
onal generalizations.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Julie Bergner
DTSTART;VALUE=DATE-TIME:20231207T170000Z
DTEND;VALUE=DATE-TIME:20231207T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/109
DESCRIPTION:Title: Models for (∞\,n)-categories with discreteness
conditions\nby Julie Bergner as part of Topos Institute Colloquium\n\
n\nAbstract\nThere are two ways of turning Segal spaces into models for up
-to-homotopy categories\, or (∞\,1)-categories: either asking that the s
pace of objects be discrete\, or requiring Rezk's completeness condition.
When generalizing to higher (∞\,n)-categories\, both of these approache
s have been taken to multisimplicial models\, in the form of Segal n-categ
ories and n-fold complete Segal spaces\, but models given by Θ_n-diagrams
have focused on the completeness conditions. In this talk\, we'll discus
s how to get a Θ_n-model with discreteness conditions\, but also address
the question of when these conditions can be mixed and matched with one an
other.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leonardo de Moura
DTSTART;VALUE=DATE-TIME:20230907T170000Z
DTEND;VALUE=DATE-TIME:20230907T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/110
DESCRIPTION:Title: Lean 4: Empowering the Formal Mathematics Revolu
tion and Beyond\nby Leonardo de Moura as part of Topos Institute Collo
quium\n\n\nAbstract\nThis talk presents Lean 4\, the latest version of the
Lean proof assistant\, and its impact on the mathematical community. We f
irst introduce the project's design and objectives\, followed by the missi
on of the newly established Lean Focused Research Organization (FRO).\nThe
advent of Lean and similar proof assistants has sparked a transformation
in mathematical practice\, an era we refer to as the "Formal Mathematics R
evolution". We'll explore how Lean 4 contributes to this revolution\, with
its tools and structures enabling mathematicians to formalize complex the
ories and proofs with unprecedented ease. A key aspect of our philosophy i
s facilitating decentralized innovation. We discuss the strategies employe
d to empower a diverse community of researchers\, developers\, and enthusi
asts to contribute to formalized mathematics.\nWe will also delve into the
usage of Lean as a functional programming language. With Lean 4\, we have
not only created an environment for formalizing mathematics but also an e
ffective tool for writing software\, enabling a smooth interaction between
mathematical and computational aspects. Finally\, we will look ahead\, sh
aring our vision and planned steps for the future of Lean 4 and the Lean F
RO. We'll discuss how we aim to further grow the user base\, continue impr
oving usability\, and deepen the reach of formal methods into mathematics
and computer science.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dominic Orchard
DTSTART;VALUE=DATE-TIME:20231012T170000Z
DTEND;VALUE=DATE-TIME:20231012T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/111
DESCRIPTION:Title: Programming for the Planet\nby Dominic Orcha
rd as part of Topos Institute Colloquium\n\n\nAbstract\nClimate change is
one of the greatest challenges of our time. Assessing its risks and our pr
ogress towards mitigating its worst effects requires a wealth of data abou
t our natural environment that we rapidly process into accurate indicators
\, assessments\, and predictions\, with sufficient trust in the resulting
insights to make decisions that affect the lives of billions worldwide\, b
oth now and in the future. However\, in the last decade\, climate modellin
g has faced diminishing returns from current hardware trends and software
techniques. Furthermore\, developing the required models and analysis tool
s to effectively process\, explore\, archive\, and derive policy decisions
\, with a high degree of transparency and trust\, remains difficult. I arg
ue that more cross-disciplinary effort between mathematics\, computer scie
nce\, software engineering\, and data science is needed to help close the
gap between where we are and where we need to be. I will discuss our work
at the Institute of Computing for Climate Science and the critical role of
programming in addressing the needs of climate science. I will also make
connections to relevant areas of category theory which could be leveraged
to develop more flexible climate models in the future.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michael Levin
DTSTART;VALUE=DATE-TIME:20230921T170000Z
DTEND;VALUE=DATE-TIME:20230921T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/112
DESCRIPTION:Title: Emergent Selves and Unconventional Intelligences
: where philosophy and engineering meet\nby Michael Levin as part of T
opos Institute Colloquium\n\n\nAbstract\nWe are composites\, made out an a
gential material. In this talk\, I \nwill describe how molecular pathways\
, cells\, tissues\, and organs display \nintelligence - problem-solving an
d creative behavior in a variety of \ndiverse problem spaces. I will descr
ibe evolutionary aspects of this \namazing multiscale competency architect
ure\, and how the cognition of \ncells scales up to the grandiose goals of
morphogenetic\, behavioral\, and \nlinguistic collectives. I will show da
ta from my lab that uses \ndevelopmental biophysics\, computer science\, a
nd behavioral science to \nunderstand diverse intelligence and work toward
s practical\, biomedical \napplications of these ideas (in areas of regene
ration birth defects\, and \ncancer). I will also describe our synthetic l
ife forms\, which we use to \nunderstand the latent space of goals for col
lective systems without an \nevolutionary history.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tom Leinster
DTSTART;VALUE=DATE-TIME:20231026T170000Z
DTEND;VALUE=DATE-TIME:20231026T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/113
DESCRIPTION:Title: Entropy and diversity: the axiomatic approach\nby Tom Leinster as part of Topos Institute Colloquium\n\n\nAbstract\nEc
ologists have been debating the best way to measure diversity for more\nth
an 70 years. The concept of diversity is relevant not only in ecology\,\nb
ut also in other fields such as genetics and economics\, as well as being\
nclosely related to information entropy. \n\nThe question of how best to q
uantify diversity has surprising mathematical\ndepth. Indeed\, a general s
tudy of invariants resembling cardinality and\nEuler characteristic led to
the unifying notion of the magnitude of an\nenriched category - a quantit
y which is also closely related to the maximum\ndiversity of a community o
f prescribed species. I will give a high-level\noverview of the concepts o
f entropy\, diversity and magnitude\, and how they\nfit together.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maurice Chiodo
DTSTART;VALUE=DATE-TIME:20231116T170000Z
DTEND;VALUE=DATE-TIME:20231116T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/114
DESCRIPTION:Title: Normalising ethical reasoning for mathematicians
\nby Maurice Chiodo as part of Topos Institute Colloquium\n\n\nAbstrac
t\nIn the past 10 years there has been a significant increase in the level
of attention on issues of ethical and responsible development in mathemat
ics. "Ethics in Mathematics" is now a recognised area of study\, and there
are now substantially more resources to consult on this. However\, such u
nderstanding has not yet permeated into the minds of the bulk of mathemati
cians. Most either have minimal realisation of the need to consider ethica
l and societal issues when carrying out mathematical work\, or lack the sk
ill set needed to carry out such thinking in a thorough and systematic way
. In short: most mathematicians either don't know how to spot ethical issu
es\, or don't know what to do when they have.\nIn this talk I will aim to
address both of these `blindspots' for mathematicians. I will present my "
Teaching Resources for Embedding Ethics in Mathematics" (arXiv:2310.08467)
\, which is a tool to embed ethics in mathematics teaching by way of mathe
matical exercises that normalise ethical considerations. I will also prese
nt my "Manifesto for the Responsible Development of Mathematical Works" (a
rXiv:2306.09131)\, which is a tool to help mathematicians dissect their wo
rkflow and identify the points at which their actions and choices may lead
to harmful consequences. In short: train mathematicians to think about et
hics all the time\, then educate them on what to do when they identify suc
h issues.\nThese are joint works with Dennis Müller\, and form part of th
e Cambridge University Ethics in Mathematics Project (ethics.maths.cam.ac.
uk).\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Cartmell
DTSTART;VALUE=DATE-TIME:20240118T170000Z
DTEND;VALUE=DATE-TIME:20240118T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/115
DESCRIPTION:Title: Aspects of a Mathematical Theory of Data\nby
John Cartmell as part of Topos Institute Colloquium\n\n\nAbstract\nI will
discuss significant aspects of a theory of data and what may be achieved
by representing data specifications as sketches of Range Categories with
additional structure. I will discuss the distinction between relational an
d non-relational physical data specifications and contrast physical and lo
gical data specifications. I will discuss goodness criteria for such speci
fications and define some specific criteria which generalise the classic r
elational goodness criteria i.e. the so called normal forms of Codd\, Fagi
n\, Ling and Goh and others.\n\nMy goal for a fully elaborated Mathematica
l Theory of Data is to effect a change in what is considered best practice
for the way in which data is specified and programmed as as to enable bes
t practice to be shifted from being at the level that data is physically r
epresented and communicated to being at the more abstract level of its log
ical structure.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Minhyong Kim
DTSTART;VALUE=DATE-TIME:20231130T170000Z
DTEND;VALUE=DATE-TIME:20231130T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/116
DESCRIPTION:Title: Who Owns Mathematics: A Question of Identity
\nby Minhyong Kim as part of Topos Institute Colloquium\n\n\nAbstract\nAt
a recent conference on the global history of mathematics\, a question was
raised about the recurrence of Euclid in a number of the talks and the 'We
stern' bias that seemed to appear in a meeting that was concerned with glo
bal history. In this talk\, I will discuss the misconceptions around the i
dentities of historical figures like Euclid\, the deep-rooted confusion su
rrounding ancient identities in general\, and why it might be important fo
r mathematicians of our times to be aware of them.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Susan Niefield
DTSTART;VALUE=DATE-TIME:20240208T170000Z
DTEND;VALUE=DATE-TIME:20240208T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/117
DESCRIPTION:Title: Cauchy Completeness and Adjoints in Double Categ
ories\nby Susan Niefield as part of Topos Institute Colloquium\n\n\nAb
stract\nIn his 1973 paper (TAC Reprints\, 2002)\, Lawvere observed that a
metric space Y is a category enriched in the extended reals\, and showed t
hat Y is Cauchy complete if and only if every bimodule (i.e.\, profunctor)
with codomain Y has a right adjoint. More recently\, Paré (2021) conside
red adjoints and Cauchy completeness in double categories\, and showed tha
t an (S\,R)-bimodule M has a right adjoint in the double category of commu
tative rings if and only if it is finitely generated and projective as an
S-module. It is well known that the latter property characterizes the exis
tence of a left adjoint to tensoring with M on the category of S-modules\,
and this was generalized to rigs and quantales in a 2017 paper by Wood an
d the speaker.\n\nThis talk consists of two parts. First\, after recalling
the relevant definitions\, we present examples of Cauchy complete objects
in some "familiar" double categories. Second\, we incorporate the two abo
ve mentioned projectivity results into a version of the 2017 theorem with
Wood which we then apply to (not-necessarily commutative) rings\, rigs\, a
nd quantales.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Juan Pablo Vigneaux
DTSTART;VALUE=DATE-TIME:20240125T170000Z
DTEND;VALUE=DATE-TIME:20240125T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/118
DESCRIPTION:Title: Cohomological aspects of information\nby Jua
n Pablo Vigneaux as part of Topos Institute Colloquium\n\n\nAbstract\nThis
talk will discuss the cohomological aspects of information functions with
in the framework of information cohomology (first introduced by Baudot and
Bennequin in 2015). Several known functionals can be identified as cohomo
logy classes in this framework\, including the Shannon entropy of discrete
probability measures and the differential entropy and underlying dimensio
n of continuous measures. I’ll try to provide an accessible overview of
the foundations of the theory\, which should require only a basic familiar
ity with category theory and homological algebra\, and survey the main kno
wn results. Finally\, I'll discuss some perspectives and open problems: fi
rstly in connection with Renyi's information dimension and other (possibly
geometric) invariants of laws taking values on manifolds\, and secondly w
ith notions of entropy for categories (akin to Leinster's diversity of met
ric spaces).\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:André Joyal
DTSTART;VALUE=DATE-TIME:20231214T170000Z
DTEND;VALUE=DATE-TIME:20231214T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/119
DESCRIPTION:Title: Higher topos theory and Goodwillie Calculus\
nby André Joyal as part of Topos Institute Colloquium\n\n\nAbstract\nLuri
e's higher topos theory is a vast extension of Grothendieck's topos theory
. I will compare the two theories\, stressing similarities and differences
. The fact that the ∞-category of parametrised spectra is a higher topos
has no analog in Grothendieck topos theory. It is the first stage of the
Goodwillie tower associated to any left exact localization of a higher top
os. The tower can be understood in analogy with the completion tower of a
n ideal in a commutative ring. For many purposes\, a topos has the dual as
pects of a space (the topos) and of a ring (the logos). The category of lo
goi (=the opposite of the category of topoi) has many properties in common
with the category of commutative rings.\n\nIn collaboration with Mathieu
Anel\, Georg Biedermann and Eric Finster.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robert Paré
DTSTART;VALUE=DATE-TIME:20240111T170000Z
DTEND;VALUE=DATE-TIME:20240111T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/120
DESCRIPTION:Title: The functorial difference operator\nby Rober
t Paré as part of Topos Institute Colloquium\n\n\nAbstract\nAs a tool for
studying the structure of endofunctors F of Set\, \nwe introduce the diff
erence operator△\n\n△[F](X) = F(X + 1) \\ F(X).\n\nThis is analogous t
o the classical difference operator for real\nvalued functions\, a discret
e form of the derivative.\n\nThe \\ above is set difference and can't be
expected to be functorial\,\nbut it is for a large class of functors\, th
e taut functors of Manes\, \nwhich include polynomial functors and many mo
re.\n\nWe obtain combinatorial versions of classical identities\, often\n'
'improved'. Many examples will be given.\n\nThe talk should be accessible
to everyone. The only prerequisite \nis some very basic category theory.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:André Joyal
DTSTART;VALUE=DATE-TIME:20240215T170000Z
DTEND;VALUE=DATE-TIME:20240215T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/121
DESCRIPTION:Title: Free bicompletion of categories revisited (part
1)\nby André Joyal as part of Topos Institute Colloquium\n\n\nAbstrac
t\nWhitman's theory of free lattices can be extended to free lattices enri
ched over a quantales\, to free bicomplete enriched categories and even to
free bicomplete enriched oo-categories. It has applications to the semant
ic of Linear Logic (Hongde Hu and J.)\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joachim Kock
DTSTART;VALUE=DATE-TIME:20240222T170000Z
DTEND;VALUE=DATE-TIME:20240222T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/122
DESCRIPTION:Title: Polynomial functors — from elementary arithmet
ic to infinity-operads\nby Joachim Kock as part of Topos Institute Col
loquium\n\n\nAbstract\nIn their simplest form\, polynomial functors are en
dofunctors of the category of sets built from sums and products. At first
they can be considered a categorification of the notion of polynomial func
tion\, but it has turned out the theory of polynomial functors is more gen
erally an efficient toolbox for dealing with induction\, nesting\, and sub
stitution. The talk will highlight some of these aspects in combinatorics\
, logic\, and homotopy theory.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Steven Clontz
DTSTART;VALUE=DATE-TIME:20240328T170000Z
DTEND;VALUE=DATE-TIME:20240328T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/123
DESCRIPTION:Title: Sociotechnical infrastructure for mathematics re
search\nby Steven Clontz as part of Topos Institute Colloquium\n\n\nAb
stract\nThe National Science Foundation defines "cyberinfrastructure" as "
the hardware\, software\, networks\, data and people that underpin today's
advanced computing technology"\, particularly technologies that advance s
cientific discovery. In particular\, this infrastructure is incomplete wit
hout its "people"\, leading some to prefer the terminology "sociotechnical
infrastructure" to emphasize the importance of how these technologies con
nect human researchers\, and how human researchers in turn use and develop
these technologies in order to create new knowledge. In mathematics resea
rch\, even theoretical mathematics\, we use many technologies\, and engage
with many different communities\, but there is little scholarship on the
ad hoc research infrastructure itself that we implicitly rely on from day
to day. This talk will provide an overview of some of the work I've done a
s part of my spring 2024 sabbatical dedicated to the research and developm
ent of improved sociotechnical infrastructure for mathematics research.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Po-Shen Loh
DTSTART;VALUE=DATE-TIME:20240404T170000Z
DTEND;VALUE=DATE-TIME:20240404T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/124
DESCRIPTION:Title: Uniting Game Theory\, Math Stars\, and Actors To
Build Human Intelligence in the AI Age\nby Po-Shen Loh as part of Top
os Institute Colloquium\n\n\nAbstract\nOne of the central challenges of be
yond-standard-curriculum instruction (such as "gifted" education) is how t
o achieve equitably-distributed scale. Making matters worse\, generative
AI such as ChatGPT is increasingly adept at solving standard curricular ta
sks\, so it is urgent to scalably deliver teaching that goes beyond curren
t standards. Fortunately\, there is an area close to math which devises so
lutions in which problems solve themselves even through self-serving human
behavior: Game Theory.\n\nThe speaker will describe his recent work\, whi
ch uses Game Theory to create a novel alignment of incentives\, which conc
urrently solves pain points in disparate sectors. At the heart of the inno
vation is a new\, mutually-beneficial cooperation between high school math
stars and professionally trained actors and comedians. This creates a hig
hly scalable community of extraordinary coaches with sufficient capacity t
o teach large numbers of middle schoolers seeking to learn critical thinki
ng and creative analytical problem solving (https://live.poshenloh.com). A
t the same time\, it creates a new pathway for high school math stars to s
ignificantly strengthen their emotional intelligence. The whole program is
conducted virtually\, so it reaches through geographical barriers. The sp
eaker will also share his experience extending this work to build talent d
evelopment pipelines in underprivileged communities\, identifying and supp
orting highly motivated middle school students who otherwise did not have
access to coaching.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rodrigo Ochigame
DTSTART;VALUE=DATE-TIME:20240815T170000Z
DTEND;VALUE=DATE-TIME:20240815T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/125
DESCRIPTION:by Rodrigo Ochigame 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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gioele Zardini
DTSTART;VALUE=DATE-TIME:20240425T170000Z
DTEND;VALUE=DATE-TIME:20240425T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/126
DESCRIPTION:Title: Co-Design of Complex Systems: From Autonomy to F
uture Mobility\nby Gioele Zardini as part of Topos Institute Colloquiu
m\n\n\nAbstract\nWhen designing complex systems\, we need to consider mult
iple trade-offs at various abstraction levels and scales\, and choices of
single components need to be studied jointly. For instance\, the design of
future mobility solutions (e.g.\, autonomous vehicles\, micromobility) an
d the design of the mobility systems they enable are closely coupled. Inde
ed\, knowledge about the intended service of novel mobility solutions woul
d impact their design and deployment process\, while insights about their
technological development could significantly affect transportation manage
ment policies. Optimally co-designing sociotechnical systems is a complex
task for at least two reasons. On one hand\, the co-design of interconnect
ed systems (e.g.\, large networks of cyber-physical systems) involves the
simultaneous choice of components arising from heterogeneous natures (e.g.
\, hardware vs. software parts) and fields\, while satisfying systemic con
straints and accounting for multiple objectives. On the other hand\, compo
nents are connected via collaborative and conflicting interactions between
different stakeholders (e.g.\, within an intermodal mobility system). In
this talk\, I will present a framework to co-design complex systems\, leve
raging a monotone theory of co-design and tools from applied category theo
ry. The framework will be instantiated in the task of designing future mob
ility systems\, all the way from the policies that a city can design\, to
the autonomy of vehicles as part of an autonomous mobility-on-demand servi
ce. Through various case studies\, I will show how the proposed approaches
allow one to efficiently answer heterogeneous questions\, unifying differ
ent modeling techniques and promoting interdisciplinarity\, modularity\, a
nd compositionality. I will then discuss open challenges for compositional
systems design optimization\, and present my agenda to tackle them.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mason Porter
DTSTART;VALUE=DATE-TIME:20240627T170000Z
DTEND;VALUE=DATE-TIME:20240627T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/127
DESCRIPTION:Title: Topological Data Analysis of Spatial Systems
\nby Mason Porter as part of Topos Institute Colloquium\n\n\nAbstract\nI w
ill discuss topological data analysis (TDA)\, which uses ideas from topolo
gy to quantify the "shape" of data. I will focus in particular on persiste
nt homology (PH)\, which one can use to find "holes" of different dimensio
ns in data sets. I will briefly introduce these ideas and then discuss a s
eries of examples of TDA of spatial systems. The examples that I'll discus
s include voting data\, the locations of polling sites\, and the webs of s
piders under the influence of various drugs.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nicola Gambino
DTSTART;VALUE=DATE-TIME:20240523T170000Z
DTEND;VALUE=DATE-TIME:20240523T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/128
DESCRIPTION:Title: Monoidal bicategories\, differential linear logi
c\, and analytic functors\nby Nicola Gambino as part of Topos Institut
e Colloquium\n\n\nAbstract\nThe aim of this talk is to present bicategoric
al counterparts of the notions of a linear explonential comonad\, as consi
dered in the study of linear logic\, and of a codereliction transformation
\, introduced in the study of differential linear logic via differential c
ategories. As an application\, the differential calculus of Joyal's analyt
ic functors will be extended to analytic functors between presheaf categor
ies\, in a way that is analogous to how ordinary calculus extends from a s
ingle variable to many variables. This is based on joint work with Marcelo
Fiore and Martin Hyland (https://arxiv.org/abs/2405.05774).\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Spencer Breiner
DTSTART;VALUE=DATE-TIME:20240905T170000Z
DTEND;VALUE=DATE-TIME:20240905T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/129
DESCRIPTION:by Spencer Breiner as part of Topos Institute Colloquium\n\nIn
teractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bj
dVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstr
act: TBA\n
LOCATION:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Eugenio Moggi
DTSTART;VALUE=DATE-TIME:20240509T170000Z
DTEND;VALUE=DATE-TIME:20240509T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/130
DESCRIPTION:Title: Categories of Classes for Collection Monads\
nby Eugenio Moggi as part of Topos Institute Colloquium\n\n\nAbstract\nIn
1998 Manes introduced the notion of collection monad on the category of se
ts as a suitable semantics for collection types. The canonical example of
collection monad is the finite powerset monad.\n\nIn order to account for
the algorithmic aspects the category of sets should be replaced with othe
r categories\, whose arrows are maps computable by "low complexity" algori
thms.\n\nWe extends Manes' definition of collection monad to models for we
ak versions of Algebraic Set Theory (AST). AST was proposed by Joyal and
Moerdijk in the '90 as a category-theoretic counterpart of Bernays' set th
eory based on classes.\n\nWe give a systematic way to construct such model
s\, which include\ncategories whose arrows are "low complexity" functions
between countable sets.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Will Crichton
DTSTART;VALUE=DATE-TIME:20240822T170000Z
DTEND;VALUE=DATE-TIME:20240822T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/131
DESCRIPTION:by Will Crichton 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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Elena Di Lavore
DTSTART;VALUE=DATE-TIME:20240516T170000Z
DTEND;VALUE=DATE-TIME:20240516T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/132
DESCRIPTION:Title: Effectful trace semantics via effectful streams<
/a>\nby Elena Di Lavore as part of Topos Institute Colloquium\n\n\nAbstrac
t\nEffectful streams are a coinductive semantic universe for effectful dat
aflow programming and traces. As an example\, we formalise the stream ciph
er cryptographic protocol. In monoidal categories with conditionals and ra
nges\, effectful streams particularize to families of morphisms satisfying
a causality condition. Effectful streams allow us to develop notions of t
race and bisimulation for effectful Mealy machines\; bisimulation implies
effectful trace equivalence.\n\nThis is recent joint work with Filippo Bon
chi and Mario Román.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Edward Lee
DTSTART;VALUE=DATE-TIME:20240418T170000Z
DTEND;VALUE=DATE-TIME:20240418T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/133
DESCRIPTION:Title: Certainty or Intelligence: Pick One!\nby Edw
ard Lee as part of Topos Institute Colloquium\n\n\nAbstract\nMathematical
models can yield certainty\, as can probabilistic models where the probabi
lities degenerate. The field of formal methods emphasizes developing such
certainty about engineering designs. In safety critical systems\, such cer
tainty is highly valued and\, in some cases\, even required by regulatory
bodies. But achieving reasonable performance for sufficiently complex envi
ronments appears to require the use of AI technologies\, which resist such
certainty. This talk suggests that certainty and intelligence may be fund
amentally incompatible.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Steve Vickers
DTSTART;VALUE=DATE-TIME:20240530T170000Z
DTEND;VALUE=DATE-TIME:20240530T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/134
DESCRIPTION:Title: The Fundamental Theorem of Calculus: point-free<
/a>\nby Steve Vickers as part of Topos Institute Colloquium\n\n\nAbstract\
nPoint-free topology is known in various guises (locales\, formal topology
)\, but can be boiled down to a procedure of defining the points of a spac
e not (“point-set”) as elements of a set\, but as models of a logical
theory. This is for a constrained “geometric” logic\, so that the open
s of the space correspond to propositional formulae derived from the theor
y: thus the theory defines both the points and the topology. Then continui
ty of maps just means that they are constructed in accordance with the con
straints of the logic.\n\nWhy bother to do topology that way? After all\,
the logic is even more constrained than constructive reasoning\, and we st
ill don’t know how far it reaches.\n\nThe first reason is that it quite
painlessly extends to toposes\, viewed as generalized spaces. This uses th
e machinery of classifying toposes\, but only in an unobtrusive way [1]. M
any proper classes can then be viewed as point-free spaces - just write do
wn a geometric theory whose models are the elements of the class.\n\nThe s
econd reason follows from the first but can then be applied back to ungene
ralized spaces in a very natural treatment of bundles. Theory presentation
s can themselves be described as the models of a geometric theory\, and th
is allows us to view bundles as continuously mapping base points to spaces
(the fibres). For physics in particular\, this invites exploration of how
much can be done using geometric methods. See eg [2].\n\nMeanwhile\, ther
e is the question of how much ordinary mathematics\, and in particular rea
l analysis\, can be done in this style. I present as a case study the Fund
amental Theorem of Calculus [3]. This illustrates some typically geometric
features of the reasoning\, such as attention paid to one-sided reals and
the use of hyperspaces and their analogues\, and some exploitation of the
geometric fact that everything is continuous\, as well as a cute new tric
k using uniform probability measures.\n\n[1] Steven Vickers “Topical cat
egories of domains”\, Mathematical Structures in Computer Science 9 (199
9)\n[2] Bas Spitters\, Steven Vickers and Sander Wolters “Gelfand spectr
a in Grothendieck toposes using geometric mathematics"\, Electronic Procee
dings in Theoretical Computer Science 158 (2014)\n[3] Steven Vickers “Th
e Fundamental Theorem of Calculus point-free\, with applications to expone
ntials and logarithms"\, arXiv:2312.05228\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Simpson
DTSTART;VALUE=DATE-TIME:20240606T170000Z
DTEND;VALUE=DATE-TIME:20240606T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/135
DESCRIPTION:Title: Three toposes for probability and randomness
\nby Alex Simpson as part of Topos Institute Colloquium\n\n\nAbstract\nI s
hall give a brief guided tour of three toposes that have arisen in a resea
rch programme to model aspects of probability and randomness from a topos
perspective. The first topos of "probability sheaves" supports a syntheti
c style of probabilistic reasoning about random variables. The second "ran
dom topos" makes sense of the notion of "random element" and models a wor
ld in which all sets are measurable. The third topos of "random probabilit
y sheaves" combines the previous two and provides a home for a more radica
l style of "synthetic probability theory" expunged of all concerns about s
igma-algebras\, measurability and the like.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kathrin Stark
DTSTART;VALUE=DATE-TIME:20240801T170000Z
DTEND;VALUE=DATE-TIME:20240801T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/136
DESCRIPTION:Title: On Taming Differentiable Logics\nby Kathrin
Stark as part of Topos Institute Colloquium\n\n\nAbstract\nFor performance
and verification in machine learning\, new methods have recently been pro
posed that optimise learning systems to satisfy formally expressed logical
properties. Among these methods\, differentiable logics (DLs) are used to
translate propositional or first-order formulae into loss functions deplo
yed for optimisation in machine learning. At the same time\, recent attemp
ts to give programming language support for verification of neural network
s showed that DLs can be used to compile verification properties to machin
e-learning backends. This situation is calling for stronger guarantees abo
ut the soundness of such compilers\, the soundness and compositionality of
DLs\, and the differentiability and performance of the resulting loss fun
ctions. In this talk\, I report on recent work to 1.) give uniform semanti
cs to and 2.) to formalise existing DLs using the Mathematical Components
library in the Coq proof assistant. This work is meant as a stepping stone
for the development of programming language support for verification of m
achine learning.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Filippo Bonchi
DTSTART;VALUE=DATE-TIME:20240502T170000Z
DTEND;VALUE=DATE-TIME:20240502T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/137
DESCRIPTION:Title: Diagrammatic Algebra of First Order Logic\nb
y Filippo Bonchi as part of Topos Institute Colloquium\n\n\nAbstract\nWe i
ntroduce the calculus of neo-Peircean relations\, a string diagrammatic ex
tension of the calculus of binary relations that has the same expressivity
as first order logic and comes with a complete axiomatisation. The axioms
are obtained by combining two well known categorical structures: cartesia
n and linear bicategories.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bartosz Milewski
DTSTART;VALUE=DATE-TIME:20240613T170000Z
DTEND;VALUE=DATE-TIME:20240613T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/139
DESCRIPTION:Title: Parametric Profunctor Preoptics\nby Bartosz
Milewski as part of Topos Institute Colloquium\n\n\nAbstract\nLocally grad
ed categories and parametric optics provide a compositional model of neura
l networks. I will show how to generalize this approach to pre-optics. I'l
l introduce a parametric profunctor representation of preoptics and use it
to implement a perceptron in Haskell.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Cyrus Omar
DTSTART;VALUE=DATE-TIME:20240829T170000Z
DTEND;VALUE=DATE-TIME:20240829T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/140
DESCRIPTION:by Cyrus Omar 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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Seth Frey
DTSTART;VALUE=DATE-TIME:20240926T170000Z
DTEND;VALUE=DATE-TIME:20240926T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/141
DESCRIPTION:by Seth Frey as part of Topos Institute Colloquium\n\nInteract
ive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09w
ZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstract: T
BA\n
LOCATION:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Arthur J Parzygnat
DTSTART;VALUE=DATE-TIME:20240808T170000Z
DTEND;VALUE=DATE-TIME:20240808T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/142
DESCRIPTION:Title: A generalization of inversion using Bayes' rule
with applications to quantum\nby Arthur J Parzygnat as part of Topos I
nstitute Colloquium\n\nInteractive livestream: https://topos-institute.zoo
m.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: th
e 5th Fermat prime\nView-only livestream: https://www.youtube.com/live/URZ
3grG7xKI\n\nAbstract\nBayes' rule has recently been given a categorical de
finition in terms of string diagrams due to Cho and Jacobs. This definitio
n of Bayesian inversion\, however\, is not robust enough for categories th
at include reasoning about quantum systems due to the no-cloning theorem.
In this talk\, I will explain how semi-cartesian categories (which have le
ss structure than Markov categories) provide a suitable framework to defin
e Bayesian inversion categorically. In particular\, I will provide axioms
for such an abstract form of Bayesian inversion. It remains an open questi
on whether these axioms characterize Bayesian inversion for quantum system
s.\n
LOCATION:https://www.youtube.com/live/URZ3grG7xKI
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
URL:https://www.youtube.com/live/URZ3grG7xKI
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fabio Gadducci
DTSTART;VALUE=DATE-TIME:20240711T170000Z
DTEND;VALUE=DATE-TIME:20240711T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/143
DESCRIPTION:Title: From gs-monoidal to cartesian categories: a stru
ctural analysis\nby Fabio Gadducci as part of Topos Institute Colloqui
um\n\n\nAbstract\nIt is now folklore that cartesian categories can be view
ed as symmetric monoidal ones equipped with two natural transformations\,
modelling diagonals and projections. In this talk we explore the taxonomy
obtained by relaxing the naturality requirement\, from gs-monoidal/cd-cate
gories to restriction and Markov ones. We show how these possibly order-en
riched categories are related by suitable commutative monads and the shape
of the arrows of the free categories generated by an algebraic signature.
\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Amélia Liao
DTSTART;VALUE=DATE-TIME:20241003T170000Z
DTEND;VALUE=DATE-TIME:20241003T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/145
DESCRIPTION:by Amélia Liao as part of Topos Institute Colloquium\n\nInter
active livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS
09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstract
: TBA\n
LOCATION:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thomas Powell
DTSTART;VALUE=DATE-TIME:20241017T170000Z
DTEND;VALUE=DATE-TIME:20241017T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/146
DESCRIPTION:by Thomas Powell 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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:C. Thi Nguyen
DTSTART;VALUE=DATE-TIME:20241010T170000Z
DTEND;VALUE=DATE-TIME:20241010T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/147
DESCRIPTION:by C. Thi Nguyen 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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nina Otter
DTSTART;VALUE=DATE-TIME:20241024T170000Z
DTEND;VALUE=DATE-TIME:20241024T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/148
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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
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:20240803T044943Z
UID:ToposInstituteColloquium/149
DESCRIPTION:by Christine Tasson 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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chris Fields
DTSTART;VALUE=DATE-TIME:20240919T170000Z
DTEND;VALUE=DATE-TIME:20240919T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/150
DESCRIPTION:by Chris Fields as part of Topos Institute Colloquium\n\nInter
active livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS
09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstract
: TBA\n
LOCATION:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mario Román
DTSTART;VALUE=DATE-TIME:20241031T170000Z
DTEND;VALUE=DATE-TIME:20241031T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/151
DESCRIPTION:by Mario Román as part of Topos Institute Colloquium\n\nInter
active livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS
09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstract
: TBA\n
LOCATION:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
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:20240803T044943Z
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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
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:20240803T044943Z
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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Shaowei Lin
DTSTART;VALUE=DATE-TIME:20241128T170000Z
DTEND;VALUE=DATE-TIME:20241128T180000Z
DTSTAMP;VALUE=DATE-TIME:20240803T044943Z
UID:ToposInstituteColloquium/154
DESCRIPTION:by Shaowei Lin 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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
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:20240803T044943Z
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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
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:20240803T044943Z
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://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ
0QUhTdGhvZ3pUdz09
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
END:VCALENDAR
**