-
Notifications
You must be signed in to change notification settings - Fork 2
/
preliminary.html
507 lines (430 loc) · 21.1 KB
/
preliminary.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML>
<HEAD>
<TITLE>Workshop on Polynomial Functors</TITLE>
<LINK REL="stylesheet" HREF="pfunk.css" TYPE="text/css">
</HEAD>
<BODY>
<script language="JavaScript" type="text/JavaScript">
<!--
function swaptabs (showthis,hidethis) {
var style2 = document.getElementById(showthis).style;style2.display = "block";
var style3 = document.getElementById(hidethis).style;style3.display = "none";
}
//-->
</script>
<TABLE CLASS="frontpagetable" CELLSPACING="0" WIDTH="100%">
<TR>
<TD>
<IMG ALIGN="left" width="330" SRC="frame.png" ALT="Photo">
<!-- <figcaption>What is this picture anyway?</figcaption>-->
</TD>
<TD WIDTH="400">
<H1>2022 Workshop on Polynomial Functors</H1>
At the <A HREF="http://topos.institute">Topos Institute</A> and
online via Zoom<BR>
2022 March 14–18 (UTC)
</TD>
</TR>
</TABLE>
<HR>
<P>
Participants will learn background material and hear the latest progress on polynomial functors. The main topic is the notion of polynomial functors in locally cartesian closed categories, as employed in logic and type theory (the theme of last year's workshop). However we also include a tutorial and talks on the notion of polynomial functors in the sense of Eilenberg and Mac Lane, hoping to uncover connections between these two notions.
<P>
This is the second workshop in a series. The <A
HREF="2021/index.html">first Workshop on
Polynomial Functors</A> was held in March 2021.
<H3>Organizers</H3>
<A HREF="http://mat.uab.cat/~kock/">Joachim Kock</A> and
<A HREF="http://dspivak.net">David Spivak</A>
<BR>
<H3>Speakers</H3>
<TABLE class="speakerstable">
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://www.andrew.cmu.edu/user/awodey/">Steve Awodey x2</A>:</TD>
<TD class="topic">
<div id="awodeylog" style="DISPLAY: block">
<a href="javascript:swaptabs('awodeyexp','awodeylog');">
► <EM>Tutorial: Polynomial functors and type theory</EM> </a> </div>
<div id="awodeyexp" style="DISPLAY: none">
<a href="javascript:swaptabs('awodeylog','awodeyexp');">
▼ <EM>Tutorial: Polynomial functors and type theory</EM> </a>
<!--
| <br>
| <a href="">Awodey's notes or slides</a>
-->
<br>Abstract: This 2-lecture tutorial will explain the connection between dependent type theory and polynomial functors first explored in [1].
The first lecture presents the basic notion of a "natural model" of type theory, a functorial reformulation of the concept of a "category with families”, capturing the syntax of dependent type theory. We show how the usual type theoretic rules of dependent sums and products correspond to the structure of a polynomial monad on the associated natural model, and an algebra for that monad. In part 2 we show what it means to add identity types and universes to the type theory, consider the relation between natural models and Joyal's “tribes”, and state some open problems.<br>
[1] S. Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science 28(2), pp. 241–286 (2018)
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://science.ucalgary.ca/mathematics-statistics/contacts/kristine-bauer">Kristine Bauer</A>:</TD>
<TD class="topic">
<div id="bauerlog" style="DISPLAY: block">
<a href="javascript:swaptabs('bauerexp','bauerlog');">
► <EM>Categorical differentiation and Goodwillie polynomial functors</EM> </a> </div>
<div id="bauerexp" style="DISPLAY: none">
<a href="javascript:swaptabs('bauerlog','bauerexp');">
▼ <EM>Categorical differentiation and Goodwillie polynomial functors</EM> </a>
<!--
| <br>
| <a href="">Bauer's notes or slides</a>
-->
<br>Abstract: The Eilenberg-Maclane notion of polynomial functors was used by Goodwillie to construct a tower of approximations of a homotopy functor similar to the way in which the Taylor Series provides approximations to functions of real variables. In this talk, I will explain the construction of the functor calculus tower and address the analogy with the Taylor Series by explaining how the derivative of a functor in the sense of Goodwillie is a categorical derivative.
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="">Clemens Berger</A>:</TD>
<TD class="topic">
<div id="bergerlog" style="DISPLAY: block">
<a href="javascript:swaptabs('bergerexp','bergerlog');">
► <EM>TBA</EM> </a> </div>
<div id="bergerexp" style="DISPLAY: none">
<a href="javascript:swaptabs('bergerlog','bergerexp');">
▼ <EM>TBA</EM> </a>
<!--
| <br>
| <a href="">Berger's notes or slides</a>
-->
<br>Abstract:
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://www.irif.fr/~curien/">Pierre-Louis Curien</A>:</TD>
<TD class="topic">
<div id="curienlog" style="DISPLAY: block">
<a href="javascript:swaptabs('curienexp','curienlog');">
► <EM>Opetopes, opetopic sets and polygraphs</EM> </a> </div>
<div id="curienexp" style="DISPLAY: none">
<a href="javascript:swaptabs('curienlog','curienexp');">
▼ <EM>Opetopes, opetopic sets and polygraphs</EM> </a>
<!--
| <br>
| <a href="">Curien's notes or slides</a>
-->
<br>Abstract: Opetopes are algebraic tree-like descriptions of shapes corresponding to compositions and coherences in higher dimensions. They were introduced by Baez and Dolan. They were later recast in the language of polynomial functors by Kock, Joyal, Batanin, and Mascari, and subsequently in a type-theoretic language by Curien, Ho Thanh and Mimram. On the other hand, polygraphs (also known as computads) are presentations of strict n- or ω-categories all the strict finite truncations of which are free in all dimensions. We will introduce both opetopes and polygraphs, and present a new, elementary, proof of the isomorphism between many-to-one polygraphs on one hand, and opetopic sets (i.e. presheaves on the category of opetopes) on the other hand. This result had been proved quite indirectly by Harnik, Makkai, and Zawadowski in 2008. A more direct proof was given by Ho Tanh in his PhD thesis (2019), with a reference to some results of Simon Henry. The new proof is entirely self-contained, and, more importantly, unveils invariants of the polygraphic syntax.
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://eldenelmanto.com">Elden Elmanto</A>:</TD>
<TD class="topic">
<div id="elmantolog" style="DISPLAY: block">
<a href="javascript:swaptabs('elmantoexp','elmantolog');">
► <EM>Bispans in algebraic geometry</EM> </a> </div>
<div id="elmantoexp" style="DISPLAY: none">
<a href="javascript:swaptabs('elmantolog','elmantoexp');">
▼ <EM>Bispans in algebraic geometry</EM> </a>
<!--
| <br>
| <a href="">Elmanto's notes or slides</a>
-->
<br>Abstract:
The category of bispans is to the category of commutative rings, as the category of spans is to the category of abelian groups. If one believes this, then it is not a stretch that various forms and ideas of algebraic geometry arise from and interact with the category of bispans. I will survey recent work around this idea. Original results presented are with Rune Haugseng, but other results include those of Bachmann-Hoyois and Barwick-Glasman-Mathew-Nikolaus.
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://www.cl.cam.ac.uk/~mpf23/">Marcelo Fiore</A>:</TD>
<TD class="topic">
<div id="fiorelog" style="DISPLAY: block">
<a href="javascript:swaptabs('fioreexp','fiorelog');">
► <EM>TBA</EM> </a> </div>
<div id="fioreexp" style="DISPLAY: none">
<a href="javascript:swaptabs('fiorelog','fioreexp');">
▼ <EM>TBA</EM> </a>
<!--
| <br>
| <a href="">Fiore's slides</a>
-->
<br>
Abstract:
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="http://www1.maths.leeds.ac.uk/~pmtng/">Nicola Gambino</A>:</TD>
<TD class="topic">
<div id="gambinolog" style="DISPLAY: block">
<a href="javascript:swaptabs('gambinoexp','gambinolog');">
► <EM>The matrix product of coloured symmetric sequences</EM> </a> </div>
<div id="gambinoexp" style="DISPLAY: none">
<a href="javascript:swaptabs('gambinolog','gambinoexp');">
▼ <EM>The matrix product of coloured symmetric sequences</EM> </a>
<!--
| <br>
| <a href="">Gambino's notes or slides</a>
-->
<br>Abstract: In 2008, Maia and Méndez defined the operation of
arithmetic product of species of structures, extending the calculus of
species of structures introduced by Joyal. In 2014, Dwyer and Hess
rediscovered independently this operation in the context of symmetric
sequences (as part of their work on Boardman-Vogt tensor product of bimodules)
and named it matrix multiplication.
In this talk, based on joint work in progress with Richard Garner and
Christina Vasilakopoulou, we extend the matrix multiplication from symmetric
sequences to coloured symmetric sequences and show that it determines an
oplax monoidal structure on the the bicategory of coloured symmetric sequences.
In order to do this, we establish general results on lifting monoidal
structures to Kleisli double categories. This approach allows us to
attack and solve the difficult problem of verifying the coherence conditions
for a monoidal bicategory in an efficient way.
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://www.union.edu/mathematics/faculty-staff/brenda-johnson">Brenda Johnson</A>:</TD>
<TD class="topic">
<div id="johnsonlog" style="DISPLAY: block">
<a href="javascript:swaptabs('johnsonexp','johnsonlog');">
► <EM>From polynomial functors to functor calculi</EM> </a> </div>
<div id="johnsonexp" style="DISPLAY: none">
<a href="javascript:swaptabs('johnsonlog','johnsonexp');">
▼ <EM>From polynomial functors to functor calculi</EM> </a>
<!--
| <br>
| <a href="">Johnson's notes or slides</a>
-->
<br>Abstract: The calculus of homotopy functors, developed by Tom Goodwillie,
provides a means of constructing a Taylor-series-like tower of functors for a
suitably nice functor of topological spaces. Use of this "Taylor tower" has led to
significant results in homotopy theory and K-theory. Inspired by Goodwillie's
construction, Kristine Bauer, Randy McCarthy and I developed an analogous functor
calculus, the discrete calculus, based on the polynomial functors of Eilenberg and Mac Lane. In this talk, I will provide an introduction to these functor calculi, and discuss recent work with Kathryn Hess that sets up a general framework for constructing functor calculi.
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://users.ox.ac.uk/~univ4449/">Sean Moss</A>:</TD>
<TD class="topic">
<div id="mosslog" style="DISPLAY: block">
<a href="javascript:swaptabs('mossexp','mosslog');">
► <EM>TBA</EM> </a> </div>
<div id="mossexp" style="DISPLAY: none">
<a href="javascript:swaptabs('mosslog','mossexp');">
▼ <EM>TBA</EM> </a>
<!--
| <br>
| <a href="">Moss's notes or slides</a>
-->
<br>Abstract:
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://fredriknf.com/">Fredrik Nordvall Forsberg</A>:</TD>
<TD class="topic">
<div id="nordvalllog" style="DISPLAY: block">
<a href="javascript:swaptabs('nordvallexp','nordvalllog');">
► <EM>TBA</EM> </a> </div>
<div id="nordvallexp" style="DISPLAY: none">
<a href="javascript:swaptabs('nordvalllog','nordvallexp');">
▼ <EM>TBA</EM> </a>
<BR>Abstract:
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="http://vcvpaiva.github.io">Valéria de Paiva</A>:</TD>
<TD class="topic">
<div id="paivalog" style="DISPLAY: block">
<a href="javascript:swaptabs('paivaexp','paivalog');">
► <EM>Dialectica logical principles</EM> </a> </div>
<div id="paivaexp" style="DISPLAY: none">
<a href="javascript:swaptabs('paivalog','paivaexp');">
▼ <EM>Dialectica logical principles</EM> </a>
<!--
| <br>
| <a href="">de Paiva's notes or slides</a>
-->
<br>Abstract: (joint work with D. Trotta and M. Spadetto)
Godel introduced the Dialectica interpretation to prove the consistency of intuitionistic arithmetic. Over the years the interpretation has been generalized by several people from a categorical perspective, leading up to the notion of Dialectica category (de Paiva 1989) or, more recently, to the notion of a Dialectica fibration (Trotta, Spadetto and de Paiva 2021). The crucial point of the interpretation is that it validates two logical principles, usually not acceptable from a constructive point of view, namely a variant of the principle of independence of premises (IP) and a variant of Markov’s principle (MP).<br><br>
This talk provides a categorical explanation of the validity of (IP) and (MP) in the Dialectica interpretation using the language of Lawvere’s doctrines. Our main tools are the existential (and universal) completions of a category discussed by Trotta and Maietti. These completions are used to define a proof-irrelevant categorification of the Dialectica interpretation in terms of Godel doctrines. We show that the categorical notions of existential-free elements and universal-free elements provide a categorical presentation of quantifier-free formulas and are the key ingredients to validate the logical principles (IP) and (MP) underlying Godel’s Dialectica interpretation.
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="">Exequiel Rivas</A>:</TD>
<TD class="topic">
<div id="rivaslog" style="DISPLAY: block">
<a href="javascript:swaptabs('rivasexp','rivaslog');">
► <EM>Procontainers: a proposal from computational effects</EM> </a> </div>
<div id="rivasexp" style="DISPLAY: none">
<a href="javascript:swaptabs('rivaslog','rivasexp');">
▼ <EM>Procontainers: a proposal from computational effects</EM> </a>
<!--
| <br>
| <a href="">Rivas's notes or slides</a>
-->
<br>Abstract:
Computational effects such as monads (Moggi 1989) and idioms (McBride &
Paterson 2008) are interpreted by functors in the semantics of
programming languages, which in many interesting cases fall under the
sphere of containers (or polynomial functors).
Arrows (Hughes 2000) are a third connected class of computational
effects, but their interpretation is in terms of profunctors rather than
functors, which are outside the scope of (polynomial) functors.
In this talk, we will explore a proposal for a notion of "procontainer"
for capturing a class of profunctors that allows us to reflect some
results from the theory of computational effects relating monads, idioms
and arrows.
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://math.cornell.edu/brandon-shapiro">Brandon Shapiro</A>:</TD>
<TD class="topic">
<div id="shapirolog" style="DISPLAY: block">
<a href="javascript:swaptabs('shapiroexp','shapirolog');">
► <EM>Polynomial representations of pra functors between presheaf categories</EM> </a> </div>
<div id="shapiroexp" style="DISPLAY: none">
<a href="javascript:swaptabs('shapirolog','shapiroexp');">
▼ <EM>Polynomial representations of pra functors between presheaf categories
</EM> </a>
<!--
| <br>
| <a href="">Shapiro's notes or slides</a>
-->
<br>Abstract:
For any functor $f : C \to D$, there is a restriction functor $f^* : \hat D \to \hat C$ between their presheaf categories with left and right adjoints $f_!,f_*$. Composites of these three types of functors have the form $f_! g_* h^*$ for some non-unique functors $f,g,h$ which form a polynomial in the category $Cat$, and when $h$ is a discrete fibration this composite is a parametric right adjoint (aka pra aka familially representable) functor. I will describe when two different polynomials in $Cat$ induce the same pra functor, give a canonical choice of polynomial ``representation'' for a given pra functor, and discuss connections between these representations and higher category theories.
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="http://dspivak.net/">David Spivak</A>:</TD>
<TD class="topic">
<div id="spivaklog" style="DISPLAY: block">
<a href="javascript:swaptabs('spivakexp','spivaklog');">
► <EM>Functorial aggregation</EM> </a> </div>
<div id="spivakexp" style="DISPLAY: none">
<a href="javascript:swaptabs('spivaklog','spivakexp');">
▼ <EM>Functorial aggregation</EM> </a>
<!--
| <br>
| <a href="">Spivak's slides</a>
-->
<br>
Abstract: In this talk I'll explain how various universal operations in the the polynomial ecosystem combine to solve an applied problem: database aggregation. In particular, we will see that the category of comonoids and bicomodules in Poly has a coclosure operation as well as a local monoidal closed structure. Using these, we'll see how the seemingly atomic operation of <i>transposing a span</i>, or <i>taking the opposite of a category</i>, is actually a composite of two more primitive universal operations: a local dual and an adjoint. The ability of the polynomial ecosystem to so articulately carve nature at it's joints seems to be necessary for defining the deceptively simple idea of database aggregation, which can be roughly understood as "integrating along compact fibers".
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://www.cl.cam.ac.uk/~ds709/">Dima Szamozvancev</A>:</TD>
<TD class="topic">
<div id="szamozvancevlog" style="DISPLAY: block">
<a href="javascript:swaptabs('szamozvancevexp','szamozvancevlog');">
► <EM>TBA</EM> </a> </div>
<div id="szamozvancevexp" style="DISPLAY: none">
<a href="javascript:swaptabs('szamozvancevlog','szamozvancevexp');">
▼ <EM>TBA</EM> </a>
<!--
| <br>
| <a href="">Szamozvancev's notes or slides</a>
-->
<br>Abstract:
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://www.paultaylor.eu">Paul Taylor</A>:</TD>
<TD class="topic">
<div id="taylorlog" style="DISPLAY: block">
<a href="javascript:swaptabs('taylorexp','taylorlog');">
► <EM>TBA</EM> </a> </div>
<div id="taylorexp" style="DISPLAY: none">
<a href="javascript:swaptabs('taylorlog','taylorexp');">
▼ <EM>TBA</EM> </a>
<!--
| <br>
| <a href="">Taylor's notes or slides</a>
-->
<br>Abstract:
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://topologicalmusings.wordpress.com">Todd Trimble</A>:</TD>
<TD class="topic">
<div id="trimblelog" style="DISPLAY: block">
<a href="javascript:swaptabs('trimbleexp','trimblelog');">
► <EM>TBA</EM> </a> </div>
<div id="trimbleexp" style="DISPLAY: none">
<a href="javascript:swaptabs('trimblelog','trimbleexp');">
▼ <EM>TBA</EM> </a>
<!--
| <br>
| <a href="">Trimble's notes or slides</a>
-->
<br>Abstract:
</div>
</TD>
</TR>
<TR>
<TD class="time" style="width: 240">●
<A HREF="https://irma.math.unistra.fr/~vespa/">Christine Vespa x3</A>:</TD>
<TD class="topic">
<div id="vespalog" style="DISPLAY: block">
<a href="javascript:swaptabs('vespaexp','vespalog');">
► <EM>Tutorial: Eilenberg-Mac Lane polynomial functors</EM> </a> </div>
<div id="vespaexp" style="DISPLAY: none">
<a href="javascript:swaptabs('vespalog','vespaexp');">
▼ <EM>Tutorial: Eilenberg-Mac Lane polynomial functors</EM> </a>
<!--
| <br>
| <a href="">Vespa's notes or slides</a>
-->
<br>Abstract: This 3-lecture tutorial is an introduction to the notion of polynomial functors, introduced by Eilenberg and Mac Lane in 1954 as a generalization of additive functors. This notion applies directly to functors from a monoidal category, in which the unit is a zero object, to an abelian category. In these lectures, I will introduce equivalent definitions of polynomial functors and give several examples. After that, I will present some structure results and an overview of applications and other developments.
</div>
</TD>
</TR>
</TABLE>
<H3>Participation</H3>
<P>
Anyone interested in participating is welcome; an <a href="https://docs.google.com/forms/d/e/1FAIpQLSc5oT7hD2l78ktp5w65gpvJLHU13rH95qdYONx_s_wBVtug8Q/viewform?usp=sf_link">online registration form</a>
is now available.
A zoom link will be sent out to registered participants
a few hours before the workshop.
</P>
For other questions, please contact <A
HREF="mailto:[email protected]">David Spivak</A> or <A
HREF="mailto:[email protected]">Joachim Kock</A>.
<H3>Program</H3>
Each talk will consist of a 50-minute presentation, followed by 10 minutes for questions and coffee break.
Presentations will
take place March 14–18 in the following 4-hour window:
<p>
14:00–18:00 UTC
<P>
Japan 23:00–03:00 (+1);
Central Europe 15:00–19:00;
UK 14:00–18:00;
US East Coast 10:00–14:00;
US West Coast 07:00–11:00.
<P>
<HR>
<SMALL>
Last update: 2022-02-14.
</SMALL>
</BODY>
</HTML>