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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
UID:ToposInstituteColloquium/35
DESCRIPTION:Title: [Title TBA]\nby Evan Patterson as part of Topos Inst
itute Colloquium\n\nInteractive livestream: https://topos-institute.zoom.u
s/j/5344862882\nPassword hint: The 5th Fermat prime\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/35/
URL:https://topos-institute.zoom.us/j/5344862882
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robert Harper
DTSTART;VALUE=DATE-TIME:20211209T170000Z
DTEND;VALUE=DATE-TIME:20211209T180000Z
DTSTAMP;VALUE=DATE-TIME:20211128T085541Z
UID:ToposInstituteColloquium/36
DESCRIPTION:Title: [Title TBA]\nby Robert Harper as part of Topos Insti
tute Colloquium\n\nInteractive livestream: https://topos-institute.zoom.us
/j/5344862882\nPassword hint: The 5th Fermat prime\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/36/
URL:https://topos-institute.zoom.us/j/5344862882
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paolo Perrone
DTSTART;VALUE=DATE-TIME:20211118T170000Z
DTEND;VALUE=DATE-TIME:20211118T180000Z
DTSTAMP;VALUE=DATE-TIME:20211128T085541Z
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:20211128T085541Z
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:20211128T085541Z
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
END:VCALENDAR