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:20220929T082733Z
UID:ToposInstituteColloquium/1
DESCRIPTION:Title: Poly: a category of remarkable abundance\nby David Sp
ivak as part of Topos Institute Colloquium\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Richard Garner
DTSTART;VALUE=DATE-TIME:20210211T210000Z
DTEND;VALUE=DATE-TIME:20210211T220000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/2
DESCRIPTION:Title: Comodels of an algebraic theory\nby Richard Garner as
part of Topos Institute Colloquium\n\n\nAbstract\nIn 1991 Eugenio Moggi i
ntroduced the monadic approach to computational effects\; this is the mech
anism by which purely functional programming languages such as Haskell can
express computations with side-effects such as output\, input\, or intera
ction with an external store.\n\nAround 2000\, Plotkin and Power refined t
he Moggi perspective by looking not at monads\, but the equational algebra
ic theories which generate them: this amounts to specifying not just a kin
d of side-effect\, but a set of primitive operations by which one can prog
ram with these side-effects.\n\nAlgebraic theories have models\, not only
in the category of sets\, but also in any category with finite products. I
n particular\, one can look at comodels of a theory: a model in the opposi
te of the category of sets. A crucial insight of Power and Shkaravska is t
hat\, if T is a theory encoding interaction with an environment\, then a T
-comodel is a state machine providing an instance of the environment with
which T interacts.\n\nThe objective of this talk is to explain this histor
y\, and to prove a new result: the category of comodels of any algebraic t
heory T is a presheaf category [B\,Set]\, where B is a small category\, wh
ich can be computed explicitly\, that encodes the static and dynamic prope
rties of the side-effects encoded by T.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gunnar E. Carlsson
DTSTART;VALUE=DATE-TIME:20210218T170000Z
DTEND;VALUE=DATE-TIME:20210218T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/3
DESCRIPTION:Title: Relative topology\, motion planning\, and coverage proble
ms\nby Gunnar E. Carlsson as part of Topos Institute Colloquium\n\n\nA
bstract\nAlgebraic topology produces invariants that capture aspects of th
e shape of a space\, or in the case of topological data analysis. Although
these invariants are in general quite rich\, they are somewhat sparse in
low dimensions. On the other hand\, it is possible to consider comma categ
ories of spaces\, for example the category of spaces with reference to a f
ixed base space and morphisms respecting the reference map. When one does
this\, one obtains a much richer set of invariants. I will discuss how to
apply this kind of construction in the setting of evasion problems for sen
sor nets and more general motion planning problems.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Samson Abramsky
DTSTART;VALUE=DATE-TIME:20210311T170000Z
DTEND;VALUE=DATE-TIME:20210311T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/4
DESCRIPTION:Title: The logic of contextuality\nby Samson Abramsky as par
t of Topos Institute Colloquium\n\n\nAbstract\n(joint work with Rui Soares
Barbosa)\n\nContextuality is a key signature of quantum non-classicality\
, which has been shown to play a central role in enabling quantum advantag
e for a wide range of information-processing and computational tasks.\nWe
study the logic of contextuality from a structural point of view\, in the
setting of partial Boolean algebras introduced by Kochen and Specker in th
eir seminal work.\nThese contrast with traditional quantum logic a la Birk
hoff--von Neumann\nin that operations such as conjunction and disjunction
are partial\, only being defined in the domain where they are physically m
eaningful.\n\nWe study how this setting relates to current work on context
uality such as the sheaf-theoretic and graph-theoretic approaches.\nWe int
roduce a general free construction extending the commeasurability relation
on a partial Boolean algebra\, i.e. the domain of definition of the binar
y logical operations.\nThis construction has a surprisingly broad range of
uses.\nWe apply it in the study of a number of issues\, including:\n\n- e
stablishing the connection between the abstract measurement scenarios stud
ied in the contextuality literature and the setting of partial Boolean alg
ebras\;\n\n- formulating various contextuality properties in this setting\
, including probabilistic contextuality as well as the strong\, state-inde
pendent notion of contextuality given by Kochen--Specker paradoxes\, which
are logically contradictory statements validated by partial Boolean algeb
ras\, specifically those arising from quantum mechanics\;\n\n- investigati
ng a Logical Exclusivity Principle\, and its relation to the Probabilistic
Exclusivity Principle widely studied in recent work on contextuality\nas
a step towards closing in on the set of quantum-realisable correlations\;\
n\n- developing some work towards a logical characterisation of the Hilber
t space tensor product\, using logical exclusivity to capture some of its
salient quantum features.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Baez
DTSTART;VALUE=DATE-TIME:20210325T180000Z
DTEND;VALUE=DATE-TIME:20210325T190000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/5
DESCRIPTION:Title: Mathematics in the 21st century\nby John Baez as part
of Topos Institute Colloquium\n\n\nAbstract\nThe climate crisis is part o
f a bigger transformation in which humanity realizes that the Earth is a f
inite system and that no physical quantity can grow exponentially forever.
This transformation may affect mathematics — and be affected by it —
just as dramatically as the agricultural and industrial revolutions did. A
fter a review of the problems\, we discuss how mathematicians can help mak
e this transformation a bit easier\, and some ways in which mathematics ma
y change.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dan Christensen
DTSTART;VALUE=DATE-TIME:20210401T170000Z
DTEND;VALUE=DATE-TIME:20210401T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/6
DESCRIPTION:Title: Reasoning in an ∞-topos with homotopy type theory\n
by Dan Christensen as part of Topos Institute Colloquium\n\n\nAbstract\nTh
is talk will be an introduction to homotopy type theory that will explain
how it can be used to prove theorems that hold in any ∞-topos. I will
introduce the basic ideas of type theory and give some intuition for what
these mean homotopically. I will end by giving examples of results pro
ved in homotopy type theory that tell us new results in any ∞-topos.
No prior knowledge of type theory or ∞-category theory will be assumed.
\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joachim Kock
DTSTART;VALUE=DATE-TIME:20210408T170000Z
DTEND;VALUE=DATE-TIME:20210408T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/7
DESCRIPTION:Title: Noncrossing hyperchords and free probability\nby Joac
him Kock as part of Topos Institute Colloquium\n\n\nAbstract\nFree probabi
lity is a noncommutative probability theory introduced by Voiculescu in th
e 1980s\, motivated by operator algebras and free groups\, and useful in r
andom matrix theory. Where classical independence relates to the tensor pr
oduct of algebras\, free independence relates to the free product of algeb
ras. Speicher discovered the combinatorial substrate of the theory: noncro
ssing partitions. He derived the free cumulant-moment relations from Möbi
us inversion in the incidence algebra of the lattice of noncrossing partit
ions\, and used it\, via two reduction procedures\, to model free multipli
cative convolution. A crucial ingredient\, which has no analogue in the cl
assical setting\, is the notion of Kreweras complement of a noncrossing pa
rtition. In this talk\, after a long introduction to these topics\, I will
explain some more categorical viewpoints. A first step is an operad of no
ncrossing partitions. A second step is a decomposition space (2-Segal spac
e) Y of noncrossing hyperchords\, whose simplicial structure encodes highe
r versions of Kreweras complementation. The incidence bialgebra of Y is a
direct combinatorial model for free multiplicative convolution. It is rela
ted to the previous models by the standard simplicial notion of decalage:
the first decalage of Y gives the (two-sided bar construction of the) oper
ad\, and the second decalage gives the lattice. These two decalages encode
precisely Speicher's two reductions.\n\nThis is joint work with Kurusch E
brahimi-Fard\, Loïc Foissy\, and Frédéric Patras.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Emily Riehl
DTSTART;VALUE=DATE-TIME:20210506T170000Z
DTEND;VALUE=DATE-TIME:20210506T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/8
DESCRIPTION:Title: Contractibility as uniqueness\nby Emily Riehl as part
of Topos Institute Colloquium\n\n\nAbstract\nWhat does it mean for someth
ing to exist uniquely? Classically\, to say that a set A has a unique elem
ent means that there is an element x of A and any other element y of A equ
als x. When this assertion is applied to a space A\, instead of a mere set
\, and interpreted in a continuous fashion\, it encodes the statement that
the space A is contractible\, i.e.\, that A is continuously deformable to
a point. This talk will explore this notion of contractibility as uniquen
ess and its role in generalizing from ordinary categories to infinite-dime
nsional categories.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maria Emilia Maietti
DTSTART;VALUE=DATE-TIME:20210513T170000Z
DTEND;VALUE=DATE-TIME:20210513T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/9
DESCRIPTION:Title: Quotient completions for topos-like structures\nby Ma
ria Emilia Maietti as part of Topos Institute Colloquium\n\n\nAbstract\nIn
this talk we report fundamental results concerning free completions with
quotients of specific Lawvere doctrines for building toposes\, quasi-topos
es and predicative versions of them. Our final goal is to use such complet
ions for modelling foundations of constructive and classical mathematics w
hich are predicative in the sense of Poincaré\, Weyl and Feferman\, inclu
ding that in [M09]. We first recall how the tool of completing an elementa
ry existential Lawvere doctrine with exact quotients is the fundamental co
nstruction behind the tripos-to-topos construction in [HJP80] beside inclu
ding as instances both the exact completion of a regular category and that
of a weakly lex finite product category\, as reported in [MR15]. We then
describe recent work with Fabio Pasquali and Pino Rosolini where we show h
ow the elementary quotient completion of an elementary Lawvere doctrine in
[MR13] is the fundamental construction behind a tripos-to-quasi-topos con
struction including toposes as exact completions of a left exact category
in [Me03] as instances. We also mention a joint work with Davide Trotta wh
ere we extend results in [MPR17] about tripos-to-topos constructions coinc
iding with exact completions of a left exact category. We end by applying
the elementary quotient completion to build examples of predicative topo
ses including the Effective Predicative Topos in [MM21].\n\nReferences\n\n
[HJP80] J.M. Hyland\, P. T. Johnstone and A.M.Pitts. Tripos theory. Math.
Proc. Cambridge Philos. Soc. 88\, 205-232\, 1980\n\n[M09] M.E. Maietti. A
minimalist two-level foundation for constructive mathematics. Annals of Pu
re and Applied Logic\, 160(3): 319-354\, 2009\n\n[MR13] M.E. Maietti and G
. Rosolini. Elementary quotient completion. Theory and Applications of Cat
egories\, 27(17): 445–463\, 2013\n\n[MR15 ] M.E. Maietti and G. Rosolini
. Unifying Exact Completions. Applied Categorical Structures 23(1): 43-52\
, 2015\n\n[MPR17] M.E. Maietti\, F. Pasquali and G. Rosolini. Triposes\, e
xact completions\, and Hilbert's ε-operator. Tbilisi Mathematical Journal
. 10(3): 141-66\, 2017\n\n[Me03] M. Menni. A characterization of the left
exact categories whose exact completions are toposes. Journal of Pure and
Applied Algebra\, 3(177): 287-301\, 2003\n\n[MM21] M.E. Maietti\, S. Masch
io. A predicative variant of Hyland's Effective Topos. To appear in The Jo
urnal of Symbolic Logic\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tobias Fritz
DTSTART;VALUE=DATE-TIME:20210520T170000Z
DTEND;VALUE=DATE-TIME:20210520T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/10
DESCRIPTION:Title: The law of large numbers in categorical probability\
nby Tobias Fritz as part of Topos Institute Colloquium\n\n\nAbstract\nThe
law of large numbers (in its various guises) can be regarded as the most c
entral result of probability theory\, and any serious axiomatic system for
probability must reproduce it in some form. After a general introduction
to categorical probability in terms of Markov categories\, I will explain
how to formulate a form of the strong law of large numbers within this fra
mework\, namely the Glivenko-Cantelli theorem on the convergence of the em
pirical distribution. I will also sketch how to use this statement in orde
r to derive other laws of large numbers from it.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michael Shulman
DTSTART;VALUE=DATE-TIME:20210527T170000Z
DTEND;VALUE=DATE-TIME:20210527T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/11
DESCRIPTION:Title: Two-dimensional semantics of homotopy type theory\nb
y Michael Shulman as part of Topos Institute Colloquium\n\n\nAbstract\nThe
general higher-categorical semantics of homotopy type theory involves (
∞\,1)-toposes and Quillen model categories. However\, for many applicati
ons it suffices to consider (2\,1)-toposes\, which are reasonably concrete
categorical objects built out of ordinary groupoids. In this talk I'll d
escribe how to interpret homotopy type theory in (2\,1)-toposes\, and some
of the applications we can get from\nsuch an interpretation. I will assum
e a little exposure to type theory\, as in Dan Christensen's talk from Apr
il\, but no experience with higher toposes or homotopy theory. This talk w
ill also serve as an introduction to some basic notions of Quillen model c
ategories\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Steve Awodey
DTSTART;VALUE=DATE-TIME:20210603T170000Z
DTEND;VALUE=DATE-TIME:20210603T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/12
DESCRIPTION:Title: Model Structures from Models of HoTT\nby Steve Awode
y as part of Topos Institute Colloquium\n\n\nAbstract\nHomotopical models
of Martin-Löf type theory often make use of the notion of a Quillen model
category\, even if only implicitly. From the interpretation of identitie
s between terms as paths in an abstract space\, to the univalence principl
e identifying identities of types with homotopy equivalences of spaces\, t
he standard tools of abstract homotopy theory provide the means to make ri
gorous the basic intuition behind the homotopical interpretation of the fo
rmal logical system. \nSo good is this kind of model that it turns out to
be possible to invert the process\, in a certain sense\; given a categori
cal model of HoTT of an appropriate kind\, one can construct from it a ful
l Quillen model structure on the underlying category. This can be seen as
a further strengthening of the idea of HoTT as the internal language of a
n $\\infty$-topos.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kathryn Hess
DTSTART;VALUE=DATE-TIME:20210624T180000Z
DTEND;VALUE=DATE-TIME:20210624T190000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/13
DESCRIPTION:Title: From comonads to calculus\nby Kathryn Hess as part o
f Topos Institute Colloquium\n\n\nAbstract\nAbstracting the framework comm
on to most flavors of functor calculus\, one can define a calculus on a ca
tegory M equipped with a distinguished class of weak equivalences to be a
functor that associates to each object x of M a tower of objects in M that
are increasingly good approximations to x\, in some well defined\, Taylor
-type sense. Such calculi could be applied\, for example\, to testing whe
ther morphisms in M are weak equivalences.\n\nIn this talk\, after making
the definition above precise\, I will describe a machine for creating calc
uli on functor categories Fun (C\,M) that is natural in both the source C
and the target M. Our calculi arise by comparison of the source category C
with a tower of test categories\, equipped with cubical structure of prog
ressively higher dimension\, giving rise to sequences of resolutions of fu
nctors from C to M\, built from comonads derived from the cubical structur
e on the test categories. The stages of the towers of functors that we ob
tain measure how far the functor we are analyzing deviates from being a co
algebra over each of these comonads. The naturality of this construction
makes it possible to compare both different types calculi on the same func
tor category\, arising from different towers of test categories\, and the
same type of calculus on different functor categories\, given by a fixed
tower of test categories.\n\n(Joint work with Brenda Johnson)\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Asgar Jamneshan
DTSTART;VALUE=DATE-TIME:20210415T170000Z
DTEND;VALUE=DATE-TIME:20210415T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/14
DESCRIPTION:Title: Topos theory and measurability\nby Asgar Jamneshan a
s part of Topos Institute Colloquium\n\n\nAbstract\nIn point-free (or abst
ract) measure theory measurable spaces are replaced by $\\sigma$-complete
Boolean algebras\, measurable functions by Boolean homomorphisms\, and mea
sure spaces by measure algebras. This more general perspective has some ad
vantages over the traditional pointwise approach to measure theory. For ex
ample\, it facilitates the use of topos-theoretic techniques to study meas
urability. To this effect\, a translation process between the internal lan
guage/ logic of certain Boolean topoi and the "usual" external language/ l
ogic is required which we can accomplish by using the formalism of conditi
onal analysis. We illustrate this with some recent applications in ergodi
c theory.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chris Heunen
DTSTART;VALUE=DATE-TIME:20210617T170000Z
DTEND;VALUE=DATE-TIME:20210617T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/15
DESCRIPTION:Title: Sheaf representation of monoidal categories\nby Chri
s Heunen as part of Topos Institute Colloquium\n\n\nAbstract\nWouldn't it
be great if monoidal categories were nice and easy? They are! We will disc
uss how a monoidal category embeds into a "nice" one\, and how a "nice" mo
noidal category consists of global sections of a sheaf of "easy" monoidal
categories. This theorem cleanly separates "spatial" and "temporal" direct
ions of monoidal categories.\n\nMore precisely\, "nice" means that certain
morphisms into the tensor unit have joins that are respected by tensor pr
oducts\, namely those morphisms that are central and idempotent with respe
ct to the tensor product. By "easy" we mean that the topological space of
which these central idempotents form the opens is a lot like a singleton s
pace\, namely local.\n\nCategorifying flabby sheaves in the appropriate wa
y makes the representation functorial from monoidal categories to schemes
of local monoidal categories. The representation respects many properties
of monoidal categories: if a monoidal category is closed/traced/complete/B
oolean\, then so are its local stalks. As instances we recover the Lambek-
Moerdijk-Awodey sheaf representation for toposes\, the Stone representatio
n of Boolean algebras\, the representation by germs of open subsets of a t
opological space\, and the Takahashi representation of Hilbert modules as
continuous fields of Hilbert spaces.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Shaowei Lin
DTSTART;VALUE=DATE-TIME:20210422T170000Z
DTEND;VALUE=DATE-TIME:20210422T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/16
DESCRIPTION:Title: Proofs as programs: challenges and strategies for progra
m synthesis\nby Shaowei Lin as part of Topos Institute Colloquium\n\n\
nAbstract\nThe Curry-Howard correspondence between proofs and programs sug
gests that we can exploit proof assistants for writing software. I will di
scuss the challenges behind a naïve execution of this idea\, and some pre
liminary strategies for overcoming them. As an example\, we will organize
higher-order information in knowledge graphs using dependent type theory\,
and automate the answering of queries using a proof assistant. In another
example\, we will explore how decentralized proof assistants can enable m
athematicians or programmers to work collaboratively on a theorem or appli
cation. If time permits\, I will outline connections to canonical structur
es (ssreflect)\, reflection (ssreflect)\, transport\, unification and univ
erse management.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Geoffrey Cruttwell
DTSTART;VALUE=DATE-TIME:20210708T170000Z
DTEND;VALUE=DATE-TIME:20210708T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/17
DESCRIPTION:Title: Categorical differential structures and their role in ab
stract machine learning\nby Geoffrey Cruttwell as part of Topos Instit
ute Colloquium\n\n\nAbstract\nA fundamental component of many machine lear
ning algorithms is differentiation. Thus\, if one wishes to abstract and
generalize aspects of machine learning\, it is useful to have an abstract
perspective on differentiation. There has been much work on categorical d
ifferential structures in the past few years with the advent of differenti
al categories\, Cartesian differential categories\, and tangent categories
. In this talk I'll focus on Cartesian reverse differential categories\,
a recent variant of Cartesian differential categories\, and touch on how t
hey can be used in abstract machine learning.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Walter P Tholen
DTSTART;VALUE=DATE-TIME:20210722T170000Z
DTEND;VALUE=DATE-TIME:20210722T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/18
DESCRIPTION:Title: What is monoidal topology?\nby Walter P Tholen as pa
rt of Topos Institute Colloquium\n\n\nAbstract\nMonoidal topology may be s
een as being inspired by some visionary remarks in Hausdorff‘s „Grundz
üge der Mengenlehre“ of 1914\, and it takes its modern lead from two di
stinct seminal contributions of the early 1970s: the Manes-Barr presentati
on of topological spaces in terms of ultrafilter convergence axioms\, and
Lawvere’s presentation of metric spaces as small categories enriched in
the extended non-negative half-line of the reals. Both types of spaces bec
ome instances of small so-called (T\,V)-categories\, where T is a Set-mona
d and V a (commutative) quantale\, i.e. a small\, thin and (symmetric) mon
oidal-closed category. The setting therefore allows for a general study of
„spaces“ that combines geometric and numerical aspects in a natural w
ay.\n\nIn this talk we present some key elements of the theory and its app
lications\, showing in particular how the strictification and inversion of
some naturally occurring inequalities in this lax-monoidal setting leads
to interesting topological properties and unexpected connections. Time pe
rmitting\, we will also point to some on-going and future work in the area
.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Marcy Robertson
DTSTART;VALUE=DATE-TIME:20210729T220000Z
DTEND;VALUE=DATE-TIME:20210729T230000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/19
DESCRIPTION:Title: Topological Inspiration for Infinity Modular Operads
\nby Marcy Robertson as part of Topos Institute Colloquium\n\n\nAbstract\n
A modular operad can be thought of as an undirected network which allows f
or feedback “loops”. An infinity modular operad is such a network wher
e operations can be continuously varied with respect to time. The goal of
this talk is to give a gentle introduction to a Segal model for infinity
modular operads\, focusing on the topological origins of the idea. The aud
ience is not expected to be familiar with operads or topology. This talk w
ill cover snippets of joint work with Luci Bonatto\, Pedro Boavida\, Phili
p Hackney \, Geoffroy Horel and Donald Yau.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Eugene Lerman
DTSTART;VALUE=DATE-TIME:20210610T170000Z
DTEND;VALUE=DATE-TIME:20210610T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/20
DESCRIPTION:Title: A category of hybrid systems\nby Eugene Lerman as pa
rt of Topos Institute Colloquium\n\n\nAbstract\nHybrid systems are dynamic
al systems that exhibit both continuous time evolution and abrupt transiti
ons. Examples include mechanical systems (e.g.\, a ball bouncing off a flo
or) and cyber-physical systems (e.g.\, a room with a thermostat). Definiti
ons of a hybrid dynamical systems vary widely in literature but they usual
ly include directed graphs\, spaces with vector fields attached to the nod
es of graphs and partial maps or\, more generally\, relations attached to
the edges of graphs. The vector fields are used to model continuous evolut
ion and the relations the abrupt transitions.\n\nI wanted to understand if
analogues of coupled cell networks of Golubitsky\, Stewart and their coll
aborators (these are highly structured coupled systems of ODEs) make sense
for hybrid dynamical systems. In order to do that I needed to make sense
of open hybrid systems\, their interconnection\, networks of hybrid syste
ms and maps between networks of hybrid systems.\n\nProceeding by analogy w
ith continuous time systems I introduced the notion of a hybrid phase spac
e and its underlying manifold. A hybrid phase space can be succinctly def
ined as double functor. Hybrid phase spaces form a category HyPh with mo
rphisms coming from vertical natural transformations. A hybrid dynamical s
ystem is a pair (A\,X) where A is a hybrid phase space and X is a vector f
ield on the manifold U(A) underlying A. I then constructed a category HyDS
of hybrid dynamical system. The definition of HyDS passes a couple of san
ity checks.\n\nUsing the foundation laid out above James Schmidt and I sho
wed that one can also define hybrid surjective submersions\, hybrid open
systems\, their interconnections and networks of hybrid systems. This way
one can model systems of bouncing balls and several interconnected rooms
with separate thermostats.\n\nReferences: arXiv:1612.01950 [math.DS] and a
rXiv:1908.10447 [math.DS] (DOI: 10.1016/j.geomphys.2019.103582).\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jonathan Gorard
DTSTART;VALUE=DATE-TIME:20210429T170000Z
DTEND;VALUE=DATE-TIME:20210429T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/21
DESCRIPTION:Title: Fast Diagrammatic Reasoning and Compositional Approaches
to Fundamental Physics\nby Jonathan Gorard as part of Topos Institute
Colloquium\n\n\nAbstract\nThe Wolfram Model — a discrete spacetime mode
l based upon hypergraph rewriting — can be naively formalized as a conve
ntional double-pushout rewriting system over a partial adhesive category o
f (directed) hypergraphs. However\, the abstract rewriting structure of th
e model also permits an elegant interpretation in terms of dagger compact
categories\, with considerable formal analogies to FdHilb and the foundati
ons of categorical quantum mechanics\, yet with an additional causal seman
tics definable in terms of a second symmetric strict partial monoidal stru
cture (such that the entire system can be formalized\, for instance\, in t
erms of a double category or a weak 2-category). In addition to potentiall
y defining a general categorical semantics for discrete models of quantum
gravity\, this formalism presents a fundamentally new approach to performi
ng efficient diagrammatic reasoning over combinatorial structures\, by sug
gesting various generalizations of the standard deductive inference rules
of resolution\, superposition\, paramodulation and factoring in the Knuth-
Bendix completion approach to automated theorem-proving\, and by making mo
re explicit use of the causal structure of the abstract rewriting system i
n the choice of which inference rules to apply. We show how this approach
can be applied to the problem of enacting fast diagrammatic simplification
of circuits in quantum information theory\, as well as (time-permitting)
the problem of efficiently discretizing the Cauchy problem in numerical ge
neral relativity\, showcasing comparisons against some existing software f
rameworks and algorithms.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Todd Trimble
DTSTART;VALUE=DATE-TIME:20210805T170000Z
DTEND;VALUE=DATE-TIME:20210805T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/22
DESCRIPTION:Title: From 2-rigs to lambda-rings\nby Todd Trimble as part
of Topos Institute Colloquium\n\n\nAbstract\nThis talk will summarize som
e aspects of recent work with John Baez and Joe Moeller\, which aims to ti
e together representations of symmetric groups\, Schur functors\, and lamb
da rings from the point of view of 2-rigs\, which are a categorification o
f ordinary 'rigs' or rings without negatives. A common theme in this area
is the notion of 'plethory'. We sketch how the archetypal plethory of lamb
da rings arises simply and naturally from the simplest possible '2-plethor
y'\, and applying decategorification to it.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pawel Sobocinski
DTSTART;VALUE=DATE-TIME:20210930T150000Z
DTEND;VALUE=DATE-TIME:20210930T160000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/23
DESCRIPTION:Title: Algebraic theories with string diagrams\nby Pawel So
bocinski as part of Topos Institute Colloquium\n\n\nAbstract\nIn Lawvere t
heories the central role is played by categories with finite products. The
free category with finite products on one object (FinSet^op) is the Lawve
re theory of the empty algebraic theory\, and the free category with finit
e products on a signature (of an algebraic theory) has a concrete descript
ion as a category of classical syntactic terms. But\, using a theorem due
to Thomas Fox\, we can also capture these categories nicely using string d
iagrams.\n\nThe string diagrammatic approach gets you further than ordinar
y syntax. In a POPL 21 paper with Ivan Di Liberti\, Fosco Loregian and Cha
d Nester\, we developed a Lawvere-style approach to algebraic theories wit
h partially defined operations. It turns out that in this setting\, instea
d of categories with finite products\, the relevant concept is discrete ca
rtesian restriction categories (dcrc). And string diagrams are the right s
yntax for this setting: they let us describe the free dcrc on an object an
d the free dcrc on a signature. I will sketch some of our results and talk
about some of the ramifications\, including a string diagrammatic descrip
tion of categories with free finite limits.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Bourke
DTSTART;VALUE=DATE-TIME:20210909T170000Z
DTEND;VALUE=DATE-TIME:20210909T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/24
DESCRIPTION:Title: Tensor products\, multimaps and internal homs\nby Jo
hn Bourke as part of Topos Institute Colloquium\n\n\nAbstract\nThe notions
of monoidal category\, multicategory and closed category are closely rela
ted\, with each having their own advantages. Considering the relationship
between them leads naturally to skew variants — skew monoidal categorie
s\, skew multicategories and skew closed categories — and I will explore
some of these variants in this talk.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew J. Blumberg
DTSTART;VALUE=DATE-TIME:20210923T170000Z
DTEND;VALUE=DATE-TIME:20210923T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/25
DESCRIPTION:Title: Abstract homotopy theory for topological data analysis\nby Andrew J. Blumberg as part of Topos Institute Colloquium\n\n\nAbstr
act\nA starting point for the modern perspective on algebraic topology is
the Eilenberg-Steenrod axioms characterizing homology theories. More gene
rally\, there has been a great deal of work starting from insights of Verd
ier\, Quillen\, and Dwyer-Kan that gives abstract characterizations of the
structures of homotopy theory in terms of formal cylinder and suspension
objects or mapping spaces. This talk will be about efforts to understand
the invariants of topological data analysis from an abstract perspective.
There will be many more questions than answers.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lawrence Paulson
DTSTART;VALUE=DATE-TIME:20210701T170000Z
DTEND;VALUE=DATE-TIME:20210701T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/26
DESCRIPTION:Title: Formalising Contemporary Mathematics in Simple Type Theo
ry\nby Lawrence Paulson as part of Topos Institute Colloquium\n\n\nAbs
tract\nA long-standing question in mathematics is the relevance of formali
sation to practice. Rising awareness of fallibility among mathematicians s
uggests formalisation as a remedy. But are today's proof assistants up to
the task? And what is the right formalism?\n\nA wide variety of mathematic
al topics have been formalised in simple type theory using Isabelle/HOL. T
he partition calculus was introduced by Erdös and R. Rado in 1956 as the
study of “analogues and extensions of Ramsey’s theorem”. Highly tech
nical results were obtained by Erdös-Milner\, Specker and Larson (among m
any others) for the case of ordinal partition relations\, which is concern
ed with countable ordinals and order types. Much of this material was form
alised last year (with the assistance of Džamonja and Koutsoukou-Argyraki
). \n\nGrothendieck's Schemes have also been formalised in Isabelle/HOL. T
his achievement is notable because some prominent figures had conjectured
that schemes were beyond the reach of simple type theory.\n\nSome highligh
ts of this work will be presented along with general observations about ro
le of type theory in the formalisation of mathematics.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jamie Vicary
DTSTART;VALUE=DATE-TIME:20210916T170000Z
DTEND;VALUE=DATE-TIME:20210916T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/27
DESCRIPTION:Title: Understanding free infinity-categories\nby Jamie Vic
ary as part of Topos Institute Colloquium\n\n\nAbstract\nInfinity-categori
es have a reputation for being difficult algebraic objects to define and w
ork with. In this talk I will present a new definition of free infinity-ca
tegory that demystifies them\, and makes them easy to understand from an a
lgebraic perspective. The definition is given as a sequence of inductive-r
ecursive data structures\, and we explore how this relates to Grothendieck
's original ideas on infinity-categories. No knowledge of infinity-categor
ies is required to follow this talk!\n\nThis is joint work with Christophe
r Dean\, Eric Finster\, Ioannis Markakis and David Reutter.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Valeria de Paiva
DTSTART;VALUE=DATE-TIME:20210819T170000Z
DTEND;VALUE=DATE-TIME:20210819T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/28
DESCRIPTION:Title: Categorical Explicit Substitutions\nby Valeria de Pa
iva as part of Topos Institute Colloquium\n\n\nAbstract\nThe advantages of
functional programming are well-known: programs are easier to write\, und
erstand and verify than their imperative counterparts. However\, functiona
l languages tend to be more memory intensive and these problems have hinde
red their wider use in industry. The xSLAM project tried to address these
issues by using *explicit substitutions* to construct and implement more e
fficient abstract machines\, proved correct by construction.\n\nIn this ta
lk I recap two results from the xSLAM project which haven't been sufficien
tly discussed. First\, we provided categorical models for the calculi of e
xplicit substitutions (linear and cartesian) that we are interested in. No
one else seems to have provided categorical models for explicit substitut
ions calculi\, despite the large number of explicit substitutions systems
available in the literature. Indexed categories provide models of cartesi
an calculi of explicit substitutions. However\, these structures are inher
ently non-linear and hence cannot be used to model *linear* calculi of exp
licit substitutions. Our work replaces indexed categories with pre-sheave
s\, thus providing a categorical semantics covering both the linear and ca
rtesian cases. Our models satisfy soundness and completeness\, as expected
. \n\nSecondly\, we recall a different linear-non-linear type theory\, bui
lt from Barber and Plotkin DILL ideas\, which\, like DILL\, is better for
implementations. Unlike DILL\, this type theory\, called ILT\, satisfies
an internal language theorem. Thus we describe ILT\, show categorical sema
ntics for it and sketch the proof of its internal language theorem\, thus
justifying its use in implementations. These results are examples of `(ca
tegorically) structured deep syntax'\, to borrow Hyland's characterizatio
n.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anders Mortberg
DTSTART;VALUE=DATE-TIME:20211007T150000Z
DTEND;VALUE=DATE-TIME:20211007T160000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/29
DESCRIPTION:Title: Cubical Methods in Homotopy Type Theory and Univalent Fo
undations\nby Anders Mortberg as part of Topos Institute Colloquium\n\
n\nAbstract\nOne of the aims of Homotopy Type Theory and Univalent Foundat
ions (HoTT/UF) is to provide a practical foundation for computer formaliza
tion of mathematics by building on deep connections between type theory\,
homotopy theory and (higher) category theory. Some of the key inventions o
f HoTT/UF include Voevodsky's univalence axiom relating equality and equiv
alence of types\, the internal stratification of types by the complexity o
f their equality\, as well as higher inductive types which allow synthetic
reasoning about spaces in type theory. In order to provide computational
support for these notions various cubical type theories have been invented
. In particular\, the Agda proof assistant now has a cubical mode which ma
kes it possible to work and compute directly with the concepts of HoTT/UF.
In the talk I will discuss some of the mathematical ideas which motivate
these developments\, as well as show examples of how computer mechanizatio
n of mathematics looks like in Cubical Agda. I will not assume expert know
ledge of HoTT/UF and key concepts will be introduced throughout the talk.\
n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andreas Blass
DTSTART;VALUE=DATE-TIME:20211014T170000Z
DTEND;VALUE=DATE-TIME:20211014T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/30
DESCRIPTION:Title: A topos view of axioms of choice for finite sets\nby
Andreas Blass as part of Topos Institute Colloquium\n\n\nAbstract\nTarski
proved (in set theory without choice) that if one assumes that\nall famil
ies of 2-element sets have choice functions then one can\nprove that all f
amilies of 4-element sets have choice functions.\nMostowski (1937) investi
gated similar implications\, giving\nnumber-theoretic and group-theoretic
conditions\, some necessary and\nsome sufficient for such implications. B
ut some questions remained\nunsolved\, in particular: Do choice from 3-ele
ment sets\, from 5-element\nsets\, and from 13-element sets together imply
choice from 15-element\nsets. Gauntt (1970) resolved those remaining que
stions\, using\ngroup-theoretic criteria. I plan to describe some of this
work and to\nexplain what it has to do with topos theory.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chris Kapulkin
DTSTART;VALUE=DATE-TIME:20211021T170000Z
DTEND;VALUE=DATE-TIME:20211021T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/31
DESCRIPTION:Title: Cubical setting for Discrete Homotopy Theory\nby Chr
is Kapulkin as part of Topos Institute Colloquium\n\n\nAbstract\nDiscrete
homotopy theory\, developed by H. Barcelo and collaborators\, is a homotop
y theory of (simple) graphs. Homotopy invariants of graphs have found nume
rous applications\, for instance\, in the theory of matroids\, hyperplane
arrangements\, and time series analysis. Discrete homotopy theory is also
a special instance of a homotopy theory of simplicial complexes\, develope
d by R. Atkin\, to study social and technological networks.\n\nIn the talk
\, I will introduce the main concepts and open problems of discrete homoto
py theory. I will also report on the joint work with D. Carranza on develo
ping a new foundation for discrete homotopy theory in the category of cubi
cal sets\, which offers solutions to a number of long standing open proble
ms in the field.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dorette Pronk
DTSTART;VALUE=DATE-TIME:20211028T170000Z
DTEND;VALUE=DATE-TIME:20211028T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/32
DESCRIPTION:Title: Doubly Lax Colimit of Double Categories with Application
s\nby Dorette Pronk as part of Topos Institute Colloquium\n\n\nAbstrac
t\nThus far\, lax and oplax pseudo colimits of double categories have been
considered in two flavours [2]: horizontally lax and vertically lax\, bas
ed on the notions of horizontal and vertical transformations (respectively
) between double functors. Also\, the diagrams of double categories have t
ypically been indexed by a 2-category.\n\nIn this work we introduce diagra
ms indexed by a double category\; in order to make sense of this we will m
ap into a version of the quintets of the category of double categories\, b
ecause this category itself is only enirched in double categories and is o
ften taken as a 2-category. Between the new indexing functors we introduce
a new notion of transformation\, namely doubly lax transformation. We the
n introduce a double categorical version of the Grothendieck construction
and show that it has a universal property as doubly lax colimit of the dia
gram\; i.e.\, a colimit that is lax with respect to the new transformation
s.\n\nAs applications we obtain:\n\n— a universal property as lax colimi
t for the Grothendieck construction for bicategories described in [1]\;\n\
n— a universal property for the elements construction for double categor
ies\;\n\n— a notion of fibration for double categories\, different from
the internal one described by Street and others\;\n\n— a double categori
cal generalization of the classical tom Dieck fundamental groupoid for a s
pace with an action by a topological group.\n\nThis is joint work with Mar
zieh Bayeh (University of Ottawa) and Martin Szyld (Dalhousie University).
\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kevin Buzzard
DTSTART;VALUE=DATE-TIME:20210812T170000Z
DTEND;VALUE=DATE-TIME:20210812T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/33
DESCRIPTION:Title: What is the point of Lean's maths library?\nby Kevin
Buzzard as part of Topos Institute Colloquium\n\n\nAbstract\nLean is a co
mputer proof checker developed by Microsoft Research. Over the last four y
ears I have been part of a team of mathematicians and computer scientists
who have got it into their heads that it is somehow "obviously" a good ide
a to build a formally verified library of modern mathematics in Lean. You
can think of it as a 21st century Bourbaki if you like\, although our plan
s are actually far grander than Bourbaki's. I will talk about two things:
(1) how it's going and (2) why we're doing it. No background in computer p
roof checkers will be necessary to follow the talk.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Conor McBride
DTSTART;VALUE=DATE-TIME:20210826T170000Z
DTEND;VALUE=DATE-TIME:20210826T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/34
DESCRIPTION:Title: Cats and Types: Best Friends?\nby Conor McBride as p
art of Topos Institute Colloquium\n\n\nAbstract\nIntensional Type Theory a
nd Category Theory ought to fit well together\, but the current practical
experience of representing concepts from one with the tools of the other i
s often quite strained. On the one hand\, fibrational approaches to depend
ency often seem heavy. On the other hand\, definitional equality in type s
ystems often falls way short of delivering even the simplest of coherences
. In this talk\, I shall reflect on the problems and search for opportunit
ies. What has to change to make type theoretic proof assistants a good med
ium for categorical approaches to programming and proof? I wish I knew the
answer to that question! I can at least offer a few clues. For example\,
I shall exhibit a universe of indexed inductively defined datatypes which
exhibit nontrivial presheaf structure by construction.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/34/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Evan Patterson
DTSTART;VALUE=DATE-TIME:20211202T170000Z
DTEND;VALUE=DATE-TIME:20211202T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/35
DESCRIPTION:Title: Categories of diagrams in data migration and computation
al physics\nby Evan Patterson as part of Topos Institute Colloquium\n\
n\nAbstract\nDiagrams are among the most fundamental and ubiquitous concep
ts of category theory. Less appreciated are the several notions of morphis
m between diagrams in a category. After reviewing the resulting categories
of diagrams\, this talk will explain their central role in two recent pro
jects by the author and collaborators. First\, due to their close connecti
ons with limits and colimits\, the categories of diagrams provide a natura
l syntax for defining flexible data migrations between categorical databas
es. We describe a prototype implementation of this system in Catlab.jl. In
the second part of the talk\, we explain how "Tonti diagrams\," diagramma
tic presentations of physics equations expressed in vector calculus or ext
erior calculus\, can be formalized using category-theoretic diagrams. When
combined with a suitable discretization scheme\, such as the discrete ext
erior calculus (DEC)\, the result is a diagrammatic and compositional appr
oach to building numerical simulators of physical systems.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/35/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robert Harper
DTSTART;VALUE=DATE-TIME:20211209T170000Z
DTEND;VALUE=DATE-TIME:20211209T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/36
DESCRIPTION:Title: Phase Distinctions in Type Theory\nby Robert Harper
as part of Topos Institute Colloquium\n\n\nAbstract\n(Joint work with Jon
Sterling and Yue Niu)\n\nThe informal phase distinction between compile-ti
me and run-time in programming languages is formally manifested by the dis
tinction between kinds\, which classify types\, and types\, which classify
code. The distinction underpins standard programming methodology whereby
code is first type-checked for consistency before being compiled for execu
tion. When used effectively\, types help eliminate bugs before they occur.
\n\nProgram modules\, in even the most rudimentary form\, threaten the dis
tinction\, comprising as they do both types and programs in a single unit.
Matters worsen when considerating "open" modules\, with free module varia
bles standing for its imports. To maintain the separation in their presenc
e it is necessary to limit the dependency of types\, the static parts of a
module\, to their imported types. Such restrictions are fundamental for u
sing dependent types to express modular structure\, as originally suggeste
d by MacQueen.\n\nTo address this question Moggi gave an "analytic" formul
ation of program modules in which modules are explicitly separated into th
eir static and dynamic components using tools from category theory. Recent
work by Dreyer\, Rossberg\, and Russo develops this approach fully in the
ir account of ML-like module systems. In this talk we consider instead a "
synthetic" formulation using a proposition to segregate the static from th
e dynamic\, in particular to define static equivalence to manage type shar
ing and type dependency\n\nRobert Harper is a Professor of Computer Scienc
e at Carnegie Mellon\, where he\nhas been a member of faculty since 1988.
He is past recipient of the Allen\nNewell Award for research excellence an
d the Herbert Simon Award for teaching\nexcellence. He is author of Practi
cal Foundations for Programming Languages\, a\ntextbook account of program
ming language theory. His work focuses on the\napplication of type theory
to program development\, language design\, compiler\nconstruction\, and m
echanized proof.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/36/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paolo Perrone
DTSTART;VALUE=DATE-TIME:20211118T170000Z
DTEND;VALUE=DATE-TIME:20211118T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/37
DESCRIPTION:Title: The rise of quantitative category theory\nby Paolo P
errone as part of Topos Institute Colloquium\n\n\nAbstract\nIn several dom
ains of applications\, category theory can be useful to add conceptual cla
rity and scalability to mathematical models.\nHowever\, ordinary categorie
s often fail to grasp some quantitative aspects: the total cost of a certa
in strategy\, the number of composite steps\, the discrepancy between a co
ncrete construction and its ideal model\, and so on.\n\nIn order to incorp
orate these aspects\, it is helpful to switch to a "quantitative" version
of categories: weighted categories. These are particular enriched categori
es where each arrow carries a number\, or "weight"\, as in a weighted grap
h. The composition of paths comes with a triangle inequality\, analogous t
o the one of metrics and norms\, which equips universal properties with qu
antitative bounds. Most results in category theory have a weighted analogu
e\, which often carries additional geometric or analytic significance.\nWe
ighted categories have been around since early work of Lawvere\, but only
in the last few years researchers are starting to recognize their importan
ce. More and more recent papers are using them in fields as diverse as top
ological data analysis\, geometry\, and probability theory\, some times ev
en rediscovering the concepts independently.\n\nIn this talk we are going
to see what it's like to work with weighted categories\, their relationshi
p with graphs\, and the quantitative aspects about limits and colimits. We
will also define a weighted analogue of lenses\, and use it to express li
ftings of transport plans between probability measures.\n\nRelevant litera
ture: arxiv.org/abs/2110.06591 and additional work in preparation.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/37/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Florian Rabe
DTSTART;VALUE=DATE-TIME:20210902T170000Z
DTEND;VALUE=DATE-TIME:20210902T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/38
DESCRIPTION:Title: MMT: A UniFormal Approach to Knowledge Representation\nby Florian Rabe as part of Topos Institute Colloquium\n\n\nAbstract\nUn
iFormal is the idea of representing all aspects of knowledge uniformly\, i
ncluding narration\, deduction\, computation\, and databases.\nMoreover\,
it means to abstract from the multitude of individual systems\, which not
only often focus on just one aspect but are doing so in mutually incompati
ble ways\, thus creating a universal framework of formal knowledge.\n\nMMT
is a concrete representation language to that end.\nIt systematically abs
tracts from assumptions typically inherent in the syntax and semantics of
concrete systems\, and focuses on language-independence\, modularity\, and
system interoperability.\nWhile constantly evolving in order to converge
towards UniFormal\, its design and implementation have become very mature.
\nIt is now a readily usable high-level platform for the design\, analysis
\, and implementation of formal systems.\n\nThis talk gives an overview of
the current state of MMT\, its existing successes and its future challeng
es.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/38/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jeremy Avigad
DTSTART;VALUE=DATE-TIME:20211104T180000Z
DTEND;VALUE=DATE-TIME:20211104T190000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/39
DESCRIPTION:Title: Formal mathematics\, dependent type theory\, and the Top
os Institute\nby Jeremy Avigad as part of Topos Institute Colloquium\n
\n\nAbstract\nModern logic tells us that mathematics can be formalized\, i
n principle. Computational proof assistants\, developed over the last half
century\, make it possible to do so in practice. In this talk\, I will br
iefly survey the state of the field today and discuss some of the reasons
that formalization is desirable. I will discuss one particular proof assis
tant\, Lean\, and its library\, mathlib. I will explain why dependent type
theory\, Lean's underlying logical framework\, provides an attractive pla
tform for formalization. Finally\, I will consider ways that formal mathem
atics can support and enhance the Topos Institute's missions.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/39/
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Danks
DTSTART;VALUE=DATE-TIME:20220217T170000Z
DTEND;VALUE=DATE-TIME:20220217T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/40
DESCRIPTION:Title: Ethics in AI\, not Ethics of AI\nby David Danks as p
art of Topos Institute Colloquium\n\n\nAbstract\nDiscussions of the ethica
l (and societal) impact of AI often implicitly assume that ethical issues
arise only once the AI Is deployed or used. If AI is “just math” or
“just a tool\,” then one might think that ethics is simply irrelevant
to research and development of AI systems. In contrast\, I will argue that
ethical issues arise throughout every step of AI creation\, including res
earch efforts that seem to be outside of the scope of ethics. That is\, et
hics is an intrinsic part of AI\, not something that arises only after the
fact. Throughout this argument\, I will provide examples of practical too
ls and practices to improve the ethics in one’s AI systems. These insigh
ts and examples will apply to technology development in general\, includin
g fundamental mathematical research.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/40/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bob Coecke
DTSTART;VALUE=DATE-TIME:20220224T170000Z
DTEND;VALUE=DATE-TIME:20220224T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/41
DESCRIPTION:Title: Compositional Intelligence\nby Bob Coecke as part of
Topos Institute Colloquium\n\n\nAbstract\nThis talk will be fairly high-l
evel and requires no prior technical background. We will introduce the no
tion of compositional intelligence that my Oxford-based CQ-team is trying
to achieve. \n\nIn particular\, starting from the compositional match bet
ween natural language and quantum\, which also extends to other domains [1
]\, we will argue that a new generation of AI can emerge when fully pushin
g this analogy while exploiting the completeness of categorical quantum me
chanics [2]. \n\nWe also discuss the notion of compositionality itself\,
which takes many different forms within many different contexts\, and how
the one we need goes beyond previous ones [3]. \n\n[1] Vincent Wang-Masci
anica\, BC (2021) Talking Space: inference from spatial linguistic meaning
s. https://arxiv.org/abs/2109.06554 \n\n[2] BC\, Dom Horsman\, Aleks Kiss
inger\, Quanlong Wang (2021) Kindergarden quantum mechanics graduates (...
or how I learned to stop gluing LEGO together and love the ZX-calculus).
https://arxiv.org/abs/2102.10984\n\n[3] BC (2021) Compositionality as we s
ee it\, everywhere around us. https://arxiv.org/abs/2110.05327\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/41/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maaike Zwart
DTSTART;VALUE=DATE-TIME:20220331T170000Z
DTEND;VALUE=DATE-TIME:20220331T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/43
DESCRIPTION:Title: Lessons from failing distributive laws\nby Maaike Zw
art as part of Topos Institute Colloquium\n\n\nAbstract\nComposing monads
via distributive laws is tricky business\, as too often small mistakes are
overlooked. After failing to find a distributive law for the list monad o
ver itself\, I started proving that finding such a distributive law is imp
ossible. At the same time\, Dan Marsden was studying the famous counterexa
mple by Gordon Plotkin that probability does not distribute over non-deter
minism. Together we developed an algebraic method to find and generalise s
uch counterexamples\, resulting in our no-go theorems. In this talk I will
explain the main ideas behind our method\, illustrated by a proof that 'p
lus does not distribute over times'. Then\, I will highlight some crucial
steps in our method\, which tell us which type of monads are "high risk" i
n failing to compose with other monads. Lastly (time permitting)\, I will
say a few words about my current research on combining monads with guarded
recursion.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/43/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thierry Coquand
DTSTART;VALUE=DATE-TIME:20220602T170000Z
DTEND;VALUE=DATE-TIME:20220602T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/44
DESCRIPTION:Title: Sheaf Cohomology in Univalent Type Theory\nby Thierr
y Coquand as part of Topos Institute Colloquium\n\n\nAbstract\nIn the intr
oduction of his book on Higher Topos Theory\, Jacob Lurie motivates this t
heory by the fact that it allows an elegant and general treatment of sheaf
cohomology. It was realised early on that these ideas could be expressed
in the setting of univalent foundations/homotopy type theory (cf. the blog
post of Mike Shulman on cohomology\, 24 July 2013). I will try to explain
recent insights which show that this can be done in a maybe surprisingly
direct way. Furthermore\, all this can be formulated in a constructive met
a theory\, avoiding the non effective notion of injective resolutions.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/44/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Zoé Christoff
DTSTART;VALUE=DATE-TIME:20220317T170000Z
DTEND;VALUE=DATE-TIME:20220317T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/45
DESCRIPTION:Title: The logic of social influence in networks\nby Zoé C
hristoff as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk gi
ves an introduction to the use of logical tools in understanding social in
fluence and social networks phenomena. Individuals often form their opinio
ns by interpreting the behavior of others around them\, and by reasoning a
bout how those others have formed their opinions. This leads to several we
ll-known herd phenomena\, such as informational cascades\, bystander effec
t\, pluralistic ignorance\, bubbles\, and polarization. For instance\, in
the case of informational cascades\, agents in a sequence imitate one anot
her’s choices despite having diverging private evidence\, sometimes lead
ing the whole community to make the worst possible choice. Similar cascadi
ng mechanisms are at the heart of diffusion phenomena in social networks.
\n\nI first show how an epistemic logic modeling allows to make precise th
e conditions for such cascades to form\, as well as prove their inescapabi
lity. I then turn to what logical tools can do for analysing information f
low and influence in social networks. I illustrate how extremely simplifie
d models can yield surprising new results\, for instance about stabilizati
on conditions of diffusion processes. Finally\, I discuss how logic might
help us further understand how social networks affect collective decision
making processes.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/45/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giuseppe Rosolini
DTSTART;VALUE=DATE-TIME:20220407T170000Z
DTEND;VALUE=DATE-TIME:20220407T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/46
DESCRIPTION:Title: When an elementary quotient completion is a quasitopos\nby Giuseppe Rosolini as part of Topos Institute Colloquium\n\n\nAbstra
ct\nThe elementary quotient completion of an elementary doctrine generalis
es the exact completion of a category with finite products and weak equali
sers. I intend to present a characterisation of those elementary quotient
completions which produce a quasitopos. As a corollary one gets a characte
risation of the elementary quotient completions which give an elementary t
opos. Our work is reminiscent of\, and gathers ideas\, from others: in par
ticular\, Carboni and Vitale’s characterisation of exact completions in
terms of their projective objects\, Carboni and Rosolini’s characterisat
ion of locally cartesian closed exact completions\, also in the revision b
y Emmenegger\, and Menni’s characterisation of the exact completions whi
ch are elementary toposes. This is joint work with Maria Emilia Maietti an
d Fabio Pasquali.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/46/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tai-Danae Bradley
DTSTART;VALUE=DATE-TIME:20220526T170000Z
DTEND;VALUE=DATE-TIME:20220526T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/47
DESCRIPTION:Title: Entropy as an Operad Derivation\nby Tai-Danae Bradle
y as part of Topos Institute Colloquium\n\n\nAbstract\nThis talk features
a small connection between information theory\, algebra\, and topology—n
amely\, a correspondence between Shannon entropy and derivations of the op
erad of topological simplices. We will begin with a brief review of operad
s and their representations with topological simplices and the real line a
s the main example. We then give a general definition for a derivation of
an operad in any category with values in an abelian bimodule over the oper
ad. The main result is that Shannon entropy defines a derivation of the op
erad of topological simplices\, and that for every derivation of this oper
ad there exists a point at which it is given by a constant multiple of Sha
nnon entropy. We show this is compatible with\, and relies heavily on\, a
well-known characterization of entropy given by Faddeev in 1956 and a rece
nt variation given by Leinster.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/47/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dominic Verity
DTSTART;VALUE=DATE-TIME:20220324T200000Z
DTEND;VALUE=DATE-TIME:20220324T210000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/48
DESCRIPTION:Title: Zen and the art of ∞-categories\nby Dominic Verity
as part of Topos Institute Colloquium\n\n\nAbstract\nYou may well have he
ard the rumour that ∞-category theory is “really just like category th
eory with a little homotopy theory thrown in”. Inspired by that comment\
, you might even have headed to a book on ∞-categories or to the nLab to
find out more\, only to find that things in the ∞-world are far from th
at simple.\n\nFirstly you will have discovered that there is no universal
agreement on what an ∞-category actually is. Instead\, you’ve been met
with a proliferation of ∞-categorical models\; simplicially enriched ca
tegories\, quasi-categories\, (iterated) complete Segal spaces\, complicia
l sets\, Θ-spaces and so on. Then you discover\, to your horror\, that ea
ch one of these models supports its own particular interpretations of comm
on categorical concepts\, some of which appear far more familiar than othe
rs. Finally\, you realise that the relationships between the category theo
ries developed for each model are also much less than clear.\n\nIf this we
ren’t enough to leave anyone reaching for the Aspirin bottle\, there is
more bad news to come. It quickly becomes clear that there exists quite a
large gap between the informal language used to describe ∞-categorical a
rguments\, in blog posts and wiki articles\, and the corresponding formal
arguments expressed in any particular model of ∞-categories. Most of the
se are given either as concrete constructions with simplicial (or increasi
ngly cubical) objects or as abstract model category theoretic arguments. N
ow I have no doubt that we “all” love a good simplicial argument\, but
encoding things in this way does very little to aid our categorical intui
tion.\n\nThere must be a better way!\n\nIn this talk we discuss recent dev
elopments in ∞-technology that seek to address these issues. Specificall
y\, we review the current state of the art in model agnostic ∞-category
theory [2]\, which seeks to provide a unified account of ∞-category theo
ry freed from the straight jacket of a specific model. This allows both fo
r the model independent\, synthetic development of ∞-categorical results
and for the transport of analytically derived such results from one model
to another. We shall also see how these techniques are rapidly being refr
amed in type theoretic terms\, through the development of directed type th
eory [1\,3]\, thereby promising a more natural language for the formal dev
elopment of ∞-categorical concepts and results.\n\nReferences\n\n[1] E.
Riehl\, M. Shulman\, A type theory for synthetic ∞-categories\, High. St
ruct. 1 (2017) 147224.\n\n[2] E. Riehl\, D. Verity\, Elements of ∞-categ
ory theory\, Cambridge University Press\, 2022.\n\n[3] J. Weinberger\, A s
ynthetic perspective on (∞\,1)-category theory: Fibrational and semantic
aspects\, arXiv Preprint arXiv:2202.13132. (2022).\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/48/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Glynn Winskel
DTSTART;VALUE=DATE-TIME:20220303T170000Z
DTEND;VALUE=DATE-TIME:20220303T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/50
DESCRIPTION:Title: Making concurrency functional\nby Glynn Winskel as p
art of Topos Institute Colloquium\n\n\nAbstract\nThis talk bridges between
two major paradigms in computation\, the *functional*\, at basis computat
ion from input to output\, and the *interactive*\, where computation react
s to its environment while underway. Central to any compositional theory
of interaction is the dichotomy between a system and its environment. Conc
urrent games and strategies address the dichotomy in fine detail\, very lo
cally\, in a distributed fashion\, through distinctions between Player mov
es (events of the system) and Opponent moves (those of the environment). A
functional approach has to handle the dichotomy much more ingeniously\, t
hrough its blunter distinction between input and output. This has led to
a variety of functional approaches\, specialised to particular interactive
demands. Through concurrent games we can more clearly see what separates
and connects the differing paradigms\, and show how: \n\n\n— to lift fun
ctions to strategies\; the "Scott order" intrinsic to \nconcurrent games p
lays a key role in turning functional dependency to causal dependency. \n
\n— several paradigms of functional programming and logic arise naturall
y as subcategories of concurrent games\, \nincluding stable domain theory\
; nondeterministic dataflow\; geometry of interaction\; the dialectica in
terpretation\; lenses and optics\; and \ntheir extensions to containers in
dependent lenses and optics. \n\n— to transfer enrichments of strateg
ies (such as to probabilistic\, quantum or real-number computation) to f
unctional cases.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/50/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leo McElroy
DTSTART;VALUE=DATE-TIME:20220414T170000Z
DTEND;VALUE=DATE-TIME:20220414T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/51
DESCRIPTION:Title: Making Microworlds: A Framework for Making Sense by Maki
ng Things\nby Leo McElroy as part of Topos Institute Colloquium\n\n\nA
bstract\nPeople learn best by making things they care about\, which they s
hare with others. The role of an educational technologist is to communicat
e this principle through tools provided to learners. A primary item in thi
s toolmakers’ toolkit is the microworld\, a concept developed by Seymour
Papert as a “growing place for a specific species of powerful ideas or
intellectual structures.” A microworld presents someone with a small set
of ideas in an explorable environment which helps the learner recompose t
hose ideas for their own personal expression. Following the development of
a collection of microworlds\, we will uncover the meta-structure of the
“growing place” for intellectual structures\, with the aim of identify
ing a framework for making tools\, for making sense\, by making things.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/51/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alexandra Silva
DTSTART;VALUE=DATE-TIME:20220519T170000Z
DTEND;VALUE=DATE-TIME:20220519T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/52
DESCRIPTION:Title: Learning Weighted Automata over Principal Ideal Domains<
/a>\nby Alexandra Silva as part of Topos Institute Colloquium\n\n\nAbstrac
t\nIn the first part of this talk\, we discuss active learning algorithms
for weighted automata over a semiring. We show that a variant of Angluin's
seminal L* algorithm works when the semiring is a principal ideal domain\
, but not for general semirings such as the natural numbers. In the second
part\, we present some preliminary work on active learning for probabilis
tic automata\, and in particular discuss what the setup of the problem loo
ks like and how that leads (or not) to impossibility results.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/52/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Moshe Vardi
DTSTART;VALUE=DATE-TIME:20220623T170000Z
DTEND;VALUE=DATE-TIME:20220623T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/53
DESCRIPTION:Title: Ethics Washing in AI\nby Moshe Vardi as part of Topo
s Institute Colloquium\n\n\nAbstract\nOver the past decade Artificial Inte
lligence\, in general\, and Machine Laerning\, in particular\, have made i
mpressive advancements\, in image recognition\, game playing\, natural-lan
guage understanding and more. But there were also several instances where
we saw the harm \nthat these technologies can cause when they are deployed
too hastily. A Tesla crashed on Autopilot\, killing the driver\; a self-d
riving Uber crashed\, killing a pedestrian\; and commercial face-recogniti
on systems performed terribly in audits on dark-skinned people. In respons
e to that\, there has been much recent talk of AI ethics. Many organizatio
ns produced AI-ethics guidelines and companies publicize their newly estab
lished responsible-AI teams.\n\nBut talk is cheap. "Ethics washing" — al
so called “ethics theater” — is the practice of fabricating or exagg
erating a company’s interest in equitable AI systems that work for every
one. An example is when a company promotes “AI for good” initiatives w
ith one hand\, while selling surveillance tech to governments and corporat
e customers with the other. I will argue that the ethical lens is too narr
ow. The real issue is how to deal with technology's impact on society. Tec
hnology is driving the future\, but who is doing the steering?\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/53/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nicolas Behr
DTSTART;VALUE=DATE-TIME:20220609T170000Z
DTEND;VALUE=DATE-TIME:20220609T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/54
DESCRIPTION:Title: Fundamentals of Compositional Rewriting Theory\nby N
icolas Behr as part of Topos Institute Colloquium\n\n\nAbstract\nThis pres
entation is based upon [1] (joint work with R. Harmer and J. Krivine). \n\
nCategorical rewriting theory is a research field in both computer science
and applied category theory\, with a rich history spanning over 50 years
of active developments\, starting with the pioneering work of Ehrig in the
1970s.\n\nIn this talk\, I will present recent results [1] on a novel fou
ndation for reasoning about rewriting theories via so-called compositional
rewriting double categories (crDCs). The design principles followed in th
is approach are the typical "unify and conquer" strategy of applied catego
ry theory and a particular variant of the notion of compositionality. \n\n
To wit\, crDCs permit to formulate a wide variety of categorical rewriting
semantics uniformly\, whereby the horizontal category for a given semanti
cs models the rewriting rules\, while the vertical category models matchin
gs and co-matchings of rules into objects\, and where the squares model so
-called direct derivations (i.e.\, individual rewriting steps). Even befor
e considering compositionality\, it is already noteworthy that in order fo
r crDCs to be well-defined\, strong constraints are imposed upon the horiz
ontal and vertical categories and the squares of the crDC\, which in effec
t suggest categories with adhesivity properties (e.g.\, toposses\, quasi-t
oposses\, adhesive HLR categories\,...) as natural starting points for con
structing crDCs. In this sense\, the notion of crDCs thus permits to justi
fy the by now standard approach for categorical rewriting theories develop
ed over the past 20 years as being based upon categories with adhesivity p
roperties (starting with the seminal work of Lack and Sobocinski on adhesi
ve categories) from a clear mathematical high-level perspective.\n\nCompos
itionality\, on the other hand\, is a much deeper mathematical property th
at a categorical rewriting theory may carry. This property entails the exi
stence of so-called Concurrency and Associativity Theorems. The former con
cerns being able to reason on two-step rewriting sequences via implementin
g the overall effect of the two-step rewrite via a composite rule applied
in a single rewrite step\, and vice versa. The Associativity Theorem then
implies that the operation of forming compositions of rewriting rules is\,
in a certain sense\, associative. Compositionality is a necessary and cru
cial ingredient in the stochastic mechanics and rule algebra formalism dev
eloped by Behr et al. since 2015\, and which permits to provide a mathemat
ically fully consistent and universal formalism for continuous- [2] and di
screte-time Markov Chains [3] (central to applications of rewriting to bio
- and organo-chemistry\, social network modeling\, etc.) and rule-algebrai
c combinatorics [4].\n\nA central result of [1] is then that a sufficient
set of conditions on a double category to model a *compositional* rewritin
g theory consists in requiring certain fibrational properties for the vert
ical source and target functors from squares of the double categories\, i.
e.\, that they are (residual) multi-opfibrations. I will sketch how these
fibrational properties in conjunction with the other crDC axioms yield a c
ompletely uniform proof of both the Concurrency and the Associativity Theo
rems\, and\, time permitting\, how a large variety of categorical rewritin
g semantics indeed fall under the umbrella of our novel crDC formalism. \n
\nFinally\, I will provide an overview of open questions and potential fru
itful cross-connections of crDC theory with the TIC and broader ACT commun
ities.\n\n\n[1] N. Behr\, R. Harmer and J. Krivine\, "Fundamentals of Comp
ositional Rewriting Theory"\, https://arxiv.org/abs/2204.07175 \n\n[2] N.
Behr\, J. Krivine\, J.L. Andersen\, D. Merkle (2021)\, "Rewriting theory f
or the life sciences: A unifying theory of CTMC semantics"\, https://doi.o
rg/10.1016/j.tcs.2021.07.026\n\n[3] N. Behr\, B.S. Bello\, S. Ehmes\, R.
Heckel (2021)\, "Stochastic Graph Transformation For Social Network Modeli
ng"\, https://doi.org/10.4204/EPTCS.350.3\n\n[4] N. Behr (2021)\, "On Sto
chastic Rewriting and Combinatorics via Rule-Algebraic Methods"\, http://d
x.doi.org/10.4204/EPTCS.334.2\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/54/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Martín Escardó
DTSTART;VALUE=DATE-TIME:20220428T170000Z
DTEND;VALUE=DATE-TIME:20220428T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/55
DESCRIPTION:Title: Compact totally separated types in constructive univalen
t type theory\nby Martín Escardó as part of Topos Institute Colloqui
um\n\n\nAbstract\nIf a type X is finite\, then for every map p: X → 𝟚
we can tell\, by exhaustive search\, whether p has a root (we can exhibit
x with p x = 0) or not (for every x : X we have that p x = 1). Perhaps su
rprisingly\, there are infinite types X for which this decision is constru
ctively possible. We call such types compact. It turns out that there are
plenty of infinite compact types in any 1-topos. A basic\, but perhaps sur
prising\, example is the type ℕ∞ of decreasing infinite binary sequenc
es. There are plenty more\, and the purpose of this talk is to exhibit the
m. No matter how hard we tried to avoid that\, all searchable types we cou
ld find happen to be well-ordered. But this is just as well\, because we c
an use ordinals to measure how complicated the compact types that we can w
rite down in constructive univalent type theory are. Much of the above dis
cussion can be carried out in (the internal language of) a 1-topos. But th
en some of our constructions go beyond that\, by considering the type of a
ll ordinals in a universe\, which is itself an ordinal in the next univers
e\, and requires univalence and hence moves us to the realm of ∞-toposes
. It remains to address the notion of total separatedness of a type X. Thi
s is the condition that there are plenty of maps X → 𝟚 to "separate t
he points of X" in a suitable sense. I'll rigorously define this and exhib
it plenty of compact\, totally separated\, well-ordered types in univalent
type theory. I will mention Johnstone's topological topos as an example o
f where "compact" and "totally separated" acquire their usual topological
meaning. There is an old\, non-constructive\, theorem of topology that cha
racterizes the compact countable Hausdorff spaces as the countable ordinal
s with the interval topology. In the topological topos\, assuming a non-co
nstructive meta-language to reason about it\, the searchable objects we ge
t are of this form.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/55/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christoph Benzmueller
DTSTART;VALUE=DATE-TIME:20220616T170000Z
DTEND;VALUE=DATE-TIME:20220616T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/56
DESCRIPTION:Title: Logico-pluralistic exploration of foundational theories
with computers\nby Christoph Benzmueller as part of Topos Institute Co
lloquium\n\n\nAbstract\nSymbolic knowledge representation and reasoning (K
R&R) is a key aspect of human intelligence. Among other things\, it enable
s scientists to explore new theories\, declaratively describe them\, and s
hare them with colleagues. In the natural sciences\, abstract theories oft
en arise from observations and experiments\; in other fields\, such as met
aphysics\, they may result from pure thought experiments\, possibly withou
t data from which to start (and learn from). Strong AI without explicit s
ymbolic KR&R capabilities thus seems unthinkable. But how can the explorat
ion of abstract theories\, especially fundamental theories of metaphysics
and mathematics\, including logical formalisms\, be fruitfully supported o
n computers? \n\nIn this talk\, I review recent contributions in which a l
ogico-pluralistic KR&R methodology and infrastructure\, called LogiKEy\, h
as been successfully applied to the exploration and assessment of foundati
onal theories in metaphysics and mathematics. One such exploratory study o
n the axiomatic foundations of category theory\, conducted jointly with Da
na Scott and students at FU Berlin\, will be described in some more detail
. Since LogiKEy also supports exploration and assessment of ethical and le
gal theories\, it also has applications in the areas of trusted AI and AI&
Law.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/56/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrej Bauer
DTSTART;VALUE=DATE-TIME:20220512T170000Z
DTEND;VALUE=DATE-TIME:20220512T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/57
DESCRIPTION:Title: The countable reals\nby Andrej Bauer as part of Topo
s Institute Colloquium\n\n\nAbstract\nJoint work with James E. Hanson from
the University of Maryland\, https://james-hanson.github.io.\n\nIn 1874 G
eorg Cantor published a theorem stating that every sequence of reals is av
oided by some real\, thereby showing that the reals are not countable. Can
tor's proof uses classical logic. There are constructive proofs\, although
they all rely on the axiom of countable choice. Can the real numbers be s
hown uncountable without excluded middle and without the axiom of choice?
An answer has not been found so far\, although not for lack of trying.\n\n
We show that there is a topos in which the real numbers are countable\, i.
e.\, there is an epimorphism from the object of natural numbers to the obj
ect of Dedekind reals. Therefore\, higher-order intuitionistic logic canno
t show the reals to be uncountable.\n\nThe starting point of our construct
ion is a sequence of reals\, shown to exist by Joseph S. Miller from Unive
rsity of Wisconsin–Madison\, with a strong counter-diagonalization prope
rty: if an oracle Turing machine computes a specific real number\, when gi
ven any oracle representing Miller's sequence\, then the number appears in
the sequence. One gets the idea that the reals ought to be countable in a
realizability topos built from Turing machines with oracles for Miller's
sequence. However\, we cannot just use ordinary realizability\, because al
l realizability toposes validate countable choice and consequently the unc
ountability of the reals.\n\nTo obtain a topos with countable reals\, we d
efine a variant of realizability which we call parameterized realizability
. First we define parameterized partial combinatory algebras (ppca)\, whic
h are partial combinatory algebras whose evaluation depends on a parameter
. We then define parameterized realizability toposes. In these realizers w
itness logical statements uniformly in the parameters. The motivating exam
ple is the parameterized realizability topos built from the ppca of oracle
Turing machines parameterized by oracles for Miller's sequence. In this t
opos\, Miller's sequence is the desired epimorphism from natural numbers t
o Dedekind reals.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/57/
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Terilla
DTSTART;VALUE=DATE-TIME:20220505T170000Z
DTEND;VALUE=DATE-TIME:20220505T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/58
DESCRIPTION:Title: Rethinking language\nby John Terilla as part of Topo
s Institute Colloquium\n\n\nAbstract\nLanguage is essential to being human
. Without it\, no aspect of modern life could exist. But what is languag
e exactly? How precisely does meaning emerge from sequences constructed f
rom a small collection of basic symbols or sounds? Biologists\, linguists
\, and philosophers have been debating this question---still unanswered---
for thousands of years. \n\nNow\, at a pivotal moment when intelligent ma
chines are beginning to acquire human language skills\, new insights into
the nature of language are emerging. Some old beliefs about language can
probably be cast aside and achievements in artificial intelligence are in
spiring some new ways of thinking of language.\n\nI will present an argume
nt for rethinking language and give a tour of some relevant mathematical i
deas. The talk will be prepared keeping in mind the four themes of the To
pos Institute Colloquium: ethics and societal impact of mathematics\, app
lied category theory\, foundation models\, and technology and tools.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/58/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Eduardo Dubuc
DTSTART;VALUE=DATE-TIME:20220915T170000Z
DTEND;VALUE=DATE-TIME:20220915T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/59
DESCRIPTION:Title: On localizations via homotopies\nby Eduardo Dubuc as
part of Topos Institute Colloquium\n\n\nAbstract\n(joint work with J. Gil
abert based on work by Descotte-Dubuc-Szyld).\n\nLet $\\mathcal{C}$ be a c
ategory and $\\Sigma$ be a class of morphisms. The localization of \n$\\ma
thcal{C}$ at $\\Sigma$ is a category $\\mathcal{C}[\\Sigma^{-1}]$ together
with a functor $q: \\mathcal{C} \\longrightarrow \\mathcal{C}[\\Sigma^{-1
}]$ such that $q(s)$ is an isomorphism for all $s \\in \\Sigma$\, and whic
h is initial among such functors. The 2-localization is a 2-category $\\m
athcal{C}[\\Sigma^{\\sim 1}]$ together with a functor \n$q: \\mathcal{C} \
\longrightarrow \\mathcal{C}[\\Sigma^{\\sim 1}]$ such that $q(s)$ is a equ
ivalence for all $s \\in \\Sigma$\, and which is initial among such functo
rs. In this talk I will consider the construction of such localizations by
means of cylinders and its corresponding homotopies\, which will determin
e the 2-cells of $\\mathcal{C}[\\Sigma^{\\sim 1}]$. I will examine the ca
se where $\\Sigma = \\mathcal{W}$ is the class of weak equivalences of a Q
uillen's model category\, and in particular the role of the fibrant and co
fibrant replacements. I will elaborate about functorial versus non functor
ial factorizations in this construction. \nI will recall informally but wi
th sufficient precision the necessary definitions so that the non experts
can grasp the ideas and follow the proofs.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/59/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Noam Zeilberger
DTSTART;VALUE=DATE-TIME:20220630T170000Z
DTEND;VALUE=DATE-TIME:20220630T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/60
DESCRIPTION:Title: Parsing as a lifting problem and the Chomsky-Schützenbe
rger representation theorem\nby Noam Zeilberger as part of Topos Insti
tute Colloquium\n\n\nAbstract\nJoint work with Paul-André Melliès.\n\nIn
“Functors are Type Refinement Systems” [1]\, we argued for the idea t
hat rather than being modelled merely as categories\, type systems should
be modelled as functors p : D → T from a category D whose morphisms are
typing derivations to a category T whose morphisms are the terms correspon
ding to the underlying subjects of those derivations. One advantage of thi
s fibrational point of view is that the notion of typing judgment receives
a simple mathematical status\, as a triple (R\,f\,S) consisting of two ob
jects R\, S in D and a morphism f in T such that p(R)=dom(f) and p(S)=cod(
f). The question of finding a typing derivation for a typing judgment (R\,
f\,S) then reduces to the lifting problem of finding a morphism α : R →
S such that p(α)=f. We developed this perspective in a series of papers\
, and believe that it may be usefully applied to a large variety of deduct
ive systems\, beyond type systems in the traditional sense. In this work [
2]\, we focus on derivability in context-free grammars\, a classic topic i
n formal language theory with wide applications in computer science.\n\nTh
e talk will begin by explaining how derivations in any context-free gramma
r G may be naturally encoded by a functor of operads p : Free S → W[Σ]
from a freely generated operad into a certain “operad of spliced words
”. This motivates the introduction of a more general notion of context-f
ree grammar over any category C\, defined as a finite species S equipped w
ith a color denoting the start symbol and a functor of operads p : Free S
→ W[C] into the operad of spliced arrows in C. We will see that many sta
ndard concepts and properties of context-free grammars and languages can b
e formulated within this framework\, thereby admitting simpler analysis\,
and that parsing may indeed be profitably considered from a fibrational pe
rspective\, as a lifting problem along a functor from a freely generated o
perad.\n\nThe second half of the talk will be devoted to a new proof of th
e Chomsky-Schützenberger Representation Theorem. An important ingredient
is the identification of a left adjoint C[−] : Operad → Cat to the ope
rad of spliced arrows functor W[−] : Cat → Operad. This construction b
uilds the contour category C[O] of any operad O\, whose arrows have a geom
etric interpretation as “oriented contours” of operations. A direct co
nsequence of the contour / splicing adjunction is that every finite specie
s equipped with a color induces a universal context-free grammar\, generat
ing a language of tree contour words. Finally\, we prove a generalization
of the Chomsky-Schützenberger Representation Theorem\, establishing that
any context-free language of arrows over a category C is the functorial im
age of the intersection of a C-chromatic tree contour language and a regul
ar language.\n\n[1] P.-A. Melliès and N. Zeilberger\, Functors are type r
efinement systems\, POPL 2015\n\n[2] P.-A. Melliès and N. Zeilberger\, Pa
rsing as a lifting problem and the Chomsky-Schützenberger representation
theorem\, to appear at MFPS 2022\, preliminary version available at https:
//hal.archives-ouvertes.fr/hal-03702762\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/60/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dan Koditschek
DTSTART;VALUE=DATE-TIME:20221013T170000Z
DTEND;VALUE=DATE-TIME:20221013T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/61
DESCRIPTION:Title: Working Compositions for Correct Execution of Robot Task
Specifications\nby Dan Koditschek as part of Topos Institute Colloqui
um\n\nInteractive livestream: https://topos-institute.zoom.us/j/8439252373
6\nPassword hint: the 5th Fermat prime\nView-only livestream: https://yout
u.be/mJmQVO_rp3Y\n\nAbstract\nA long tradition in robotics has deployed dy
namical primitives as empirical modules of behavior [1]. Physically ground
ed formalization of these practices offers the prospect of an expressive p
rogramming language of work for dynamically dexterous robotics whose progr
ams lead to task and motion planners with associated controllers that are
correct by design [2]. This talk will offer a brief progress report on a b
ottom-up robotics research agenda seeking to formalize the use of Lagrangi
an energy landscapes as “letters” whose hierarchical [3]\, parallel [4
] and sequential [5] compositions yield “words” of hybrid dynamical sy
stems with guaranteed behavioral properties. Attention then shifts to an e
merging architecture for top-down task and motion planning [6] that offer
s the promise of abstract\, semantic\, formal specification [7] for mobile
manipulation tasks carried out by general purpose robots [8] in learned\,
geometrically complicated environments [9].\n\nThe talk concludes with a
more speculative appraisal of the prospects for a unified programming envi
ronment allowing the expressive top-down specification of robot behavior w
ith automatic compilation into bottom-up words of work that are correct by
design. A recent categorical treatment [10] of robot hybrid dynamical sys
tems [11] encodes a well-grounded version of sequential composition [12] a
nd a weak but still practicable version of hierarchical composition [3]\,
while neglecting the consideration of cross-talk [4] in its idealization o
f parallel composition as a monoidal product. Subsequent results imbue a s
lightly restricted version of this hybrid dynamical category [10] with a v
ersion of Conley’s fundamental theorem [13] guaranteeing the existence o
f global Lyapunov functions that decompose a suitably formulated relaxatio
n of the hybrid state space into a covering by attractor basins and their
boundaries [14]. Thus equipped with generalized energy landscapes\, more
physically grounded refinements of this hybrid dynamical category may yiel
d a practicable type theory whose associated resource-aware linear logic c
lauses might be integrated into the more expressive linear temporal logic
interface to the task and motion planning architecture of [7]. Such futur
e developments would greatly advance the longer term agenda toward an empi
rically practicable theory of “programming work” [2].\n\n[1] M. H. Rai
bert\, Legged Robots That Balance. Cambridge: MIT Press\, 1986.\n\n[2] D.
E. Koditschek\, “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 hy
potheses 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 hybrid dynamical extension of averaging and its application to the an
alysis of 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. Burridge\, A. A. Rizzi\, and D. E. Koditschek\, “Toward a systems
theory for the composition of dexterous robot behaviours\,” Robot. Res.
Seventh Int. Symp. ISRR’95\, pp. 149–161.\n\n[6] V. Vasilopoulos et al
.\, “Reactive Semantic Planning in Unexplored Semantic Environments Usin
g Deep Perceptual Feedback\,” IEEE Robot. Autom. Lett.\, vol. 5\, no. 3\
, pp. 4455–4462\, Jul. 2020\, doi: 10.1109/LRA.2020.3001496.\n\n[7] V. V
asilopoulos\, Y. Kantaros\, G. Pappas\, and D. Koditschek\, “Reactive Pl
anning for Mobile Manipulation Tasks in Unexplored Semantic Environments\,
” IEEE Int. Conf. Robot. Autom. ICRA\, May 2021\, [Online]. Available: h
ttps://repository.upenn.edu/ese_papers/880\n\n[8] T. T. Topping\, V. Vasil
opoulos\, A. De\, and D. Koditschek E.\, “Composition of Templates for T
ransitional Pedipulation Behaviors\,” in Proc. Int. Symp. Rob. Res.\, 20
19\, p. https://repository.upenn.edu/ese_papers/860/. [Online]. Available:
https://repository.upenn.edu/ese_papers/860/\n\n[9] V. Vasilopoulos\, G.
Pavlakos\, K. Schmeckpeper\, K. Daniilidis\, and D. E. Koditschek\, “Rea
ctive Navigation in Partially Familiar Non-Convex Environments Using Seman
tic Perceptual Feedback\,” Rev.\, p. (under review)\, 2019.\n\n[10] J. C
ulbertson\, P. Gustafson\, D. E. Koditschek\, and P. F. Stiller\, “Forma
l composition of hybrid systems\,” Theory Appl. Categ.\, vol. 35\, no. 4
5\, pp. 1634–1682\, Oct. 2020.\n\n[11] A. M. Johnson\, S. A. Burden\, an
d D. E. Koditschek\, “A hybrid systems model for simple manipulation and
self-manipulation systems\,” Int. J. Robot. Res.\, vol. 35\, no. 11\, p
p. 1354--1392\, Sep. 2016\, doi: 10.1177/0278364916639380.\n\n[12] R. R. B
urridge\, A. A. Rizzi\, and D. E. Koditschek\, “Sequential Composition o
f 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\, and Ch
aos\, Second. Boca Raton\, FL: CRC Press\, 1999. Accessed: Jan. 29\, 2017.
[Online]. Available: http://imb-biblio.u-bourgogne.fr/Record.htm?record=3
25212414349&idlist=1\n\n[14] M. D. Kvalheim\, P. Gustafson\, and D. E. Kod
itschek\, “Conley’s Fundamental Theorem for a Class of Hybrid Systems\
,” SIAM J. Appl. Dyn. Syst.\, pp. 784–825\, Jan. 2021\, doi: 10.1137/2
0M1336576.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/61/
URL:https://topos-institute.zoom.us/j/84392523736
URL:https://youtu.be/mJmQVO_rp3Y
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrea Censi
DTSTART;VALUE=DATE-TIME:20220825T170000Z
DTEND;VALUE=DATE-TIME:20220825T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/62
DESCRIPTION:Title: Categorification of Negative Information\nby Andrea
Censi as part of Topos Institute Colloquium\n\n\nAbstract\nI will present
some very recent and in-progress work about dealing\nwith “negative info
rmation” categorically. This need arises naturally\nin applications. For
example\, in motion planning problems\, providing\nan optimal solution is
the same as giving a feasible solution (the\n“positive” information)
together with a proof of the fact that there\ncannot be feasible solutions
better than the one given (the “negative”\ninformation). We model neg
ative information by introducing the concept\nof “norphisms”\, as oppo
sed to the positive information of morphisms. A\n“nategory” is a categ
ory that has “Nom”-sets in addition to hom-sets\,\nand specifies the c
ompatibility rules between norphisms and morphisms.\nWith this setup we ca
n choose to work in “coherent” “subnategories”:\nsubcategories tha
t describe a potential instantiation of the world in\nwhich all morphisms
and norphisms are compatible. We derive the\ncomposition rules for norphis
ms in a coherent subnategory\; we show\nthat norphisms do not compose by t
hemselves\, but rather they need to\nuse morphisms as catalysts. We have t
wo distinct rules of the type\nmorphism + norphism → norphism. We then s
how that those complex rules\nfor norphism inference are actually as natur
al as the ones for\nmorphisms\, from the perspective of enriched category
theory.\n\nThis is joint work with Dr. Jonathan Lorand and Ph.D. student G
ioele Zardini.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/62/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Angeliki Koutsoukou Argyraki
DTSTART;VALUE=DATE-TIME:20221006T170000Z
DTEND;VALUE=DATE-TIME:20221006T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/63
DESCRIPTION:Title: The new era of formalised mathematics and the ALEXANDRIA
Project\nby Angeliki Koutsoukou Argyraki as part of Topos Institute C
olloquium\n\nInteractive livestream: https://topos-institute.zoom.us/j/843
92523736\nPassword hint: the 5th Fermat prime\nView-only livestream: https
://youtu.be/084UXiJvFfY\n\nAbstract\nThe formalisation of mathematics with
proof assistants has recently seen a \nconsiderable increase in activity\
, with fast-expanding\, flourishing communities attracting computer scient
ists\, mathematicians and students. I will discuss the philosophy and moti
vation behind the use of modern proof assistants to formalise mathematics\
, referring to the state of the art and potential of the area and to recen
t developments involving the formalisation of advanced\, research-level ma
thematics. I will share my experiences from my participation in the ERC pr
oject "ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician"
(https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/) at the University of
Cambridge led by Professor Lawrence C. Paulson FRS and I will give an over
view of the main contributions and achievements of the project so far.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/63/
URL:https://topos-institute.zoom.us/j/84392523736
URL:https://youtu.be/084UXiJvFfY
END:VEVENT
BEGIN:VEVENT
SUMMARY:Richard Zanibbi
DTSTART;VALUE=DATE-TIME:20221027T170000Z
DTEND;VALUE=DATE-TIME:20221027T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/65
DESCRIPTION:by Richard Zanibbi 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://researchseminars.org/talk/ToposInstituteColloquium/65/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Jaz Myers
DTSTART;VALUE=DATE-TIME:20220908T170000Z
DTEND;VALUE=DATE-TIME:20220908T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/66
DESCRIPTION:Title: A synthetic approach to orbifolds\nby David Jaz Myer
s as part of Topos Institute Colloquium\n\n\nAbstract\nOrbifolds are smoot
h spaces where the points may have finitely many internal symmetries. Thes
e spaces often arise as quotients of manifolds by the actions of discrete
groups --- that is\, in situations with discrete symmetries\, such as in c
rystallography. \n\nFormally\, the notion of orbifold has been presented i
n a number of different guises -- from Satake's V-manifolds to Moerdijk an
d Pronk's proper étale groupoids -- which do not on their face resemble t
he informal definition. The reason for this divergence between formalism a
nd intuition is that the points of spaces cannot have internal symmetries
in traditional\, set-level foundations. In this talk\, we will see a forma
l definition which closely tracks the informal idea of an orbifold.\n\nBy
working with the axioms of synthetic differential geometry in cohesive hom
otopy type theory\, we will give a synthetic definition of orbifold (subsu
ming the traditional definitions) which closely resembles the informal def
inition: an orbifold is a microlinear type where the type of identificatio
ns between any two points is properly finite. In homotopy type theory\, we
can construct these orbifolds simply by giving their type of points.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/66/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jacques Carette
DTSTART;VALUE=DATE-TIME:20220922T170000Z
DTEND;VALUE=DATE-TIME:20220922T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/67
DESCRIPTION:Title: What I learned from formalizing Category Theory in Agda<
/a>\nby Jacques Carette as part of Topos Institute Colloquium\n\n\nAbstrac
t\nAn interesting side-effect of formalizing mathematics in a theorem prov
er is that such efforts frequently leads to learning new details (*) about
a known topic. I'll discuss these "little gems" that become much more app
arent via formalization. While the focus will be mostly on items learned t
hrough formalizing Category Theory\, a few nuggets from other domains (Uni
versal Algebra\, and the theory of programming languages) will also be thr
own in.\n\n(*) These details are frequently known to select experts\, but
rarely ever recorded in print.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/67/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chad Scherrer
DTSTART;VALUE=DATE-TIME:20220901T170000Z
DTEND;VALUE=DATE-TIME:20220901T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/68
DESCRIPTION:Title: Applied Measure Theory for Composable Statistical Modeli
ng\nby Chad Scherrer as part of Topos Institute Colloquium\n\n\nAbstra
ct\nStatistics is often framed in terms of probability distributions. Dist
ributions are special cases of measures\; we find that working in these mo
re general terms leads more naturally to a composable system. For example\
, a univariate probability density function is defined relative to Lebesgu
e measure. Bayesian inference often leaves us with an unnormalized posteri
or\, which (until normalized) is not a distribution at all\, but a measure
.\n\nThe MeasureTheory.jl ecosystem takes a principled approach to design\
, identifying primitives (measures like Lebesgue and Counting measure that
cannot be described in terms of other measures)\, and a rich set of combi
nators for building new measures from existing ones. This approach gives g
ood performance and makes it easy to describe measures and related structu
res (kernels\, likelihoods\, etc) that are awkward or impossible to expres
s in other systems.\n\nAfter introducing some fundamental concepts relevan
t to the field of measure theory\, this talk will give an overview of the
MeasureTheory.jl library\, finally closing with a brief introduction to Ti
lde.jl\, a probabilistic programming language that specifically targets Me
asureTheory.jl.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/68/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Josef Urban
DTSTART;VALUE=DATE-TIME:20220707T170000Z
DTEND;VALUE=DATE-TIME:20220707T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/69
DESCRIPTION:Title: Combining learning and deduction over formal math corpor
a\nby Josef Urban as part of Topos Institute Colloquium\n\n\nAbstract\
nThe talk will give a brief overview of recent methods that combine learni
ng and deduction over large formal libraries. I will mention the "hammer"
linkups between ITPs and ATPs\, systems that learn and perform direct tac
tical guidance of ITPs\, discuss learning of premise selection over large
libraries\, and learning-based guidance of saturation-style and tableau-st
yle automated theorem provers (ATPs) trained over the large proof corpora.
I will also mention feedback loops between proving and learning in this s
etting\, and show some autoformalization and conjecturing experiments.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/69/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Johan Commelin
DTSTART;VALUE=DATE-TIME:20220929T170000Z
DTEND;VALUE=DATE-TIME:20220929T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/70
DESCRIPTION:Title: Breaking the one-mind-barrier in mathematics using forma
l verification\nby Johan Commelin as part of Topos Institute Colloquiu
m\n\nInteractive livestream: https://topos-institute.zoom.us/j/84392523736
?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime
\nView-only livestream: https://youtu.be/BJsEygxdl98\n\nAbstract\nIn this
talk I will argue that formal verification helps break the\none-mind-barri
er in mathematics. Indeed\, formal verification allows a\nteam of mathemat
icians to collaborate on a project\, without one person\nunderstanding all
parts of the project. At the same time\, it also\nallows a mathematician
to rapidly free mental RAM in order to work on a\ndifferent component of a
project. It thus also expands the\none-mind-barrier by reducing cognitive
load.\n\nI will use the Liquid Tensor Experiment as an example\, to illus
trate\nthe above two points. This project recently finished the formalizat
ion\nof the main theorem of liquid vector spaces\, following up on a\nchal
lenge by Peter Scholze.\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/70/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
URL:https://youtu.be/BJsEygxdl98
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gilles Dowek
DTSTART;VALUE=DATE-TIME:20221110T170000Z
DTEND;VALUE=DATE-TIME:20221110T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/72
DESCRIPTION:by Gilles Dowek 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://researchseminars.org/talk/ToposInstituteColloquium/72/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gordon Plotkin
DTSTART;VALUE=DATE-TIME:20221117T170000Z
DTEND;VALUE=DATE-TIME:20221117T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/73
DESCRIPTION:by Gordon Plotkin as part of Topos Institute Colloquium\n\nInt
eractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjd
VS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstra
ct: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/73/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pawel Sobocinski
DTSTART;VALUE=DATE-TIME:20221201T170000Z
DTEND;VALUE=DATE-TIME:20221201T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/74
DESCRIPTION:by Pawel Sobocinski as part of Topos Institute Colloquium\n\nI
nteractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=b
jdVS09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbst
ract: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/74/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robin Cockett
DTSTART;VALUE=DATE-TIME:20221020T170000Z
DTEND;VALUE=DATE-TIME:20221020T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/75
DESCRIPTION:by Robin Cockett as part of Topos Institute Colloquium\n\nInte
ractive livestream: https://topos-institute.zoom.us/j/84392523736?pwd=bjdV
S09wZXVscjQ0QUhTdGhvZ3pUdz09\nPassword hint: the 5th Fermat prime\nAbstrac
t: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/75/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bryce Clarke
DTSTART;VALUE=DATE-TIME:20221103T170000Z
DTEND;VALUE=DATE-TIME:20221103T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/76
DESCRIPTION:by Bryce Clarke 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://researchseminars.org/talk/ToposInstituteColloquium/76/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrei Rodin
DTSTART;VALUE=DATE-TIME:20221215T170000Z
DTEND;VALUE=DATE-TIME:20221215T180000Z
DTSTAMP;VALUE=DATE-TIME:20220929T082733Z
UID:ToposInstituteColloquium/77
DESCRIPTION:by Andrei Rodin 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://researchseminars.org/talk/ToposInstituteColloquium/77/
URL:https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhT
dGhvZ3pUdz09
END:VEVENT
END:VCALENDAR