-
Notifications
You must be signed in to change notification settings - Fork 3
Expand file tree
/
Copy pathindex.html
More file actions
1269 lines (1117 loc) · 77.7 KB
/
index.html
File metadata and controls
1269 lines (1117 loc) · 77.7 KB
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
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE HTML>
<html>
<head>
<meta http-equiv="Content-type" content="text/html;charset=UTF-8" />
<title>Dutch Categories And Types Seminar</title>
<style type="text/css">
body {
margin: 1em auto;
padding: 0em 1em;
max-width: 50em;
}
a {
text-decoration: none;
color: red;
}
a:hover {
background-color: yellow;
}
</style>
</head>
<body>
<h1>Dutch Categories And Types Seminar</h1>
The Dutch Categories And Types Seminar is an inter-university seminar on type theory, category theory, and the
interaction between these two fields.
It provides a forum for discussion, collaboration, and dissemination to researchers in type theory and category theory
working in the Netherlands.
<h2>Mailing List and Zulip</h2>
We maintain a mailing list for discussion of everything related to categories and types, and for coordination of our
meetings.
<ul>
<li>To subscribe, send an email to <a
href="mailto:dutchcats+subscribe@googlegroups.com">dutchcats+subscribe@googlegroups.com</a>.
</li>
<li> To send a message to the list, use <a href="mailto:dutchcats@googlegroups.com">dutchcats@googlegroups.com</a>.
(Only emails from subscribers are accepted for distribution.)
</li>
</ul>
We also have a <a href="https://dutchcats.zulipchat.com/">Zulip server</a>. Sign up at the <a
href="https://dutchcats.zulipchat.com/register/">signup page</a>.
<h2> DutchCATS meeting in Delft, 10 April 2026</h2>
<h3>Location</h3>
We meet in the Social Data Lab (building 28)</a>, Van Mourik Broekmanweg 6, 2628 XE Delft (<a href="https://maps.app.goo.gl/9eaHqQiQ7VKkiUyj9">Google Maps</a>).
<h3>Programme</h3>
<p style="margin-left: 40px;"><em>arrival (13:00)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary> 13:10-13:40 Nathaniel Burke: Applying Non-Linear Reductions in Normalisation by Evaluation</summary>
<div><b>Abstract:</b>
A key lemma for proving decidability of dependent typechecking is decidability of judgemental equality/conversion. One technique for establishing this is normalisation by evaluation (NbE).
In the standard presentation of NbE for dependent types, we first prove normalisation, by corollary obtain injectivity of type formers and then prove decidability of equality for normal forms. Unfortunately, this approach does not scale to type theories where we need to interleave normalisation and conversion-checking, e.g. to apply non-linear reductions such as 'n - n = 0' or the 'cast-refl' rule from Observational Type Theory.
In this talk, I will introduce NbE for dependent types and explain how we can fix this problem with non-linear reductions by taking a more relaxed definition of normal forms. I will also discuss a work-in-progress Agda mechanisation.
</div>
</details>
</li>
<li>
<details>
<summary>13:40-14:10 Tom de Jong: (Counter)examples of injective types</summary>
<div><b>Abstract:</b>
In the context of univalent foundations (a.k.a. homotopy type theory), injective types were discussed by Martín Escardó in an MSCS paper from 2021. The interest in injectivity originated in its use to construct infinite searchable types, but the topic turned out to have a rather rich theory on its own. With classical logic, the injective types are simply the nonempty types. Constructively, things are more interesting with examples and counterexamples a plenty, as I will explain in this talk.
This is joint work with Martín Escardó. A preprint (with associated Agda formalization) is available as arXiv:2601.12536.
</div>
</details>
</li>
<li>14:10-14:30 <i>break</i> </li>
<li>
<details>
<summary>14:30-15:00 Josje van der Laan: A Directed Refinement of Constructive Ordinals in Algebraic Set Theory</summary>
<div><b>Abstract:</b>
Within the framework of Algebraic Set Theory (AST), as developed by Joyal and Moerdijk, ordinals may be defined categorically as the initial ZF-algebra with an inflationary successor operation. This construction coincides with the notions of ordinal in constructive set theory (CZF) and in Homotopy Type Theory (HoTT). In addition, Joyal and Moerdijk introduce Tarski ordinals, a particular initial ZF-algebra whose successor operation is monotone. This construction provides a constructive proof of Tarski’s fixed point theorem and the resulting ordinals are directed.
In this work, we introduce and analyze a new variant of directed ordinals obtained as the initial ZF-algebra with an inflationary successor whose strict downsets are closed under binary joins. We show the existence of this initial object and study its structural properties. The resulting construction gives a directed variant of the usual constructive ordinals in Algebraic Set Theory.
</div>
</details>
</li>
<li>
<details>
<summary>15:00-15:30 Niyousha Najmaei: For Generalised Algebraic Theories, Two Sorts Are Enough</summary>
<div><b>Abstract:</b>
Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. For example, the theories of categories or Martin-L{ö}f type theories form GATs. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-L{ö}f type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT with only two sorts, and there is a section-retraction correspondence (formally, a strict coreflection) between models of the original and the reduced GAT. In particular, any model of the original GAT can be turned into a model of the reduced (two-sorted) GAT and back, and this roundtrip is the identity.
The reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won't have operations interleaved between different sorts. In a type-theoretic metatheory, the initial algebra of a GAT is called a quotient inductive-inductive type (QIIT). Our reduction provides a way to implement QIITs with sort equalities or interleaved constructors which are not allowed by Cubical Agda. An instance of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura's bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.
This is joint work with Samy Avrillon, Ambrus Kaposi, Ambroise Lafont, Johann Rosain. The preprint is available here: https://arxiv.org/abs/2601.19426
</div>
</details>
</li>
<li>15:30-16:00 <i>break</i> </li>
<li>
<details>
<summary>16:00-16:30 Niels van der Weide: A realisability model of linear dependent type theory</summary>
<div><b>Abstract:</b>
We give a realisability model of linear dependent type theory with an impredicative universe of types. To do so, we use the notion of a linear comprehension category. Such comprehension categories nicely feature each of the features of linear dependent type theory, which we encode via a Grothendieck fibration and a monoidal fibration. Specifically, we show that each linear combinatory algebra gives rise to a linear comprehension category. The model construction has been formalised in the proof assistant Rocq using the UniMath library. This talk is based on joint work with Sam Speight.
</div>
</details>
</li>
<li>
<details>
<summary>16:30-17:00 Fernando Chu: AI for formalization of category theory, an experience report </summary>
<div><b>Abstract:</b>
Recently, AI has become increasingly better at formalizing mathematics. For example, on March 2, Math Inc. announced that their AI had formalized the field-medal-winning solution to the sphere packing problem in 24 dimensions, writing 500k Lean LoC in two weeks. Nonetheless, it is widely accepted that AI's code is of very low quality, and so its relevance for building libraries of formalized mathematics remains unclear. In this talk, we argue that AI can already be used with great effectiveness to aid library contributors and maintainers. We support this claim through examples from our own experience formalizing category theory in Lean, as well as through other examples we have found in the Mathlib community.
</div>
</details>
</li>
<li>18:30 Dinner at <a href="https://www.pizzabeppe.nl/en/locations/delft/markt">Pizza Beppe</a> at Markt 9a, 2611GP Delft
(<a href="https://maps.app.goo.gl/MAR2YwkmHQH1jzAi7">Google Maps</a>)</li>
</ul>
<h2>DutchCATS meeting in Utrecht, 2 May 2025</h2>
<h3>Location</h3>
We meet in KBG - Atlas
(see the <a href="https://maps.app.goo.gl/8Fjkug5JZzYjKiyo9">campus map</a>).
Registration is free, and you can register <a href="https://forms.gle/gPGDdhzSereH93Jo7">here</a>.
<h3>Programme</h3>
<p style="margin-left: 40px;"><em>arrival (13:00)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>13:15-13:45 Daniël Otten, Matching (Co)patterns with Cyclic Proofs
</summary>
<div><b>Abstract:</b>
We show how (co)pattern matching can be seen as a cyclic proof system via the Curry-Howard correspondence: cycles correspond to recursive calls, while the soundness condition makes sure that the function terminates. In cyclic proof systems, one replaces induction axioms with circular reasoning. The advantage of these systems lies in proof search: to apply (co)induction we need to guess the right (co)induction hypothesis, whereas with cycles we can start generating the proof until our current goal matches one that we have seen before.
Often, one obtains a conservativity result: cyclic proofs do not derive more than inductive proofs. In type theory, we have similar results showing that every function defined using (co)pattern matching can already be implemented using primitive (co)induction rules. However, existing results place more restrictions on recursive calls than proof assistants do in practice. Our goal is to explain the correspondences, and we hope to use techniques from cyclic proof theory to extend the type theoretic conservativity results.
This is joint work in progress with Lide Grotenhuis.
</div>
</details>
</li>
<li>
<details>
<summary>13:45-14:15 Niels van der Weide, Impredicative Encodings of Inductive and Coinductive Types
</summary>
<div><b>Abstract:</b>
In impredicative type theory (System F, also known as λ2), it is possible to define inductive data types, such as natural numbers and lists. It is also possible to define coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the β-rules). Unfortunately, they do not yield a (co)induction principle, because the necessary uniqueness principles are missing (the η-rules). Awodey, Frey, and Speight used a extension of the Calculus of Constructions (λC) with Σ-types, identity-types, and functional extensionality to define System F style inductive types with an induction principle, by encoding them as a well-chosen subtype, making them initial algebras.
In this paper, we extend their results to coinductive data types, and we detail the example of the stream data type with the desired coinduction principle (also called bisimulation). To do that, we first define quotient types (with the desired η-rules) and we also need a stronger form of the definable existential types. We also show that we can use the original method by Awodey, Frey and Speight for general inductive types by defining W-types with an induction principle. The dual approach for streams can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.
</div>
</details>
</li>
<li>14:15-14:45 <i>break</i> </li>
<li>
<details>
<summary>14:45-15:15 Kobe Wullaert, Rezk completion for topoi
</summary>
<div><b>Abstract:</b>
Topos theory offers a powerful unifying framework across mathematics, connecting fields from logic to algebraic geometry. Topoi are rich categorical structures that inherently support a specific kind of hyperdoctrine, providing a denotational semantics for certain logics and type theories.
A pivotal result by Pitts et al. characterizes these topos-induced hyperdoctrines as triposes (Topoi Representing Indexed Partially Ordered Sets).
Conversely, the tripos-to-topos construction provides a uniform method for building a topos from any tripos, encompassing classical examples like localic and realizability toposes.
This talk explores the translation of the tripos-to-topos construction into the setting of HoTT/UF.
We observe that if the base category defining the hyperdoctrine does not satisfy univalence, the resulting topos is generally also non-univalent.
To address this, we prove that the Rezk completion, a standard way to obtain a univalent category, commutes with the structure of an elementary topos in a 2-categorical sense.
Specifically, we demonstrate that the biadjunction characterizing the Rezk completion lifts to bicategories of elementary topoi.
Our proof strategy leverages displayed technology, enabling a modular construction of Rezk completions for categories equipped with additional structure.
</div>
</details>
</li>
<li>
<details>
<summary>15:15-15:45 Dario Stein, Independence Structures and Dagger Categories of Relations
</summary>
<div><b>Abstract:</b>
For any Markov category C with conditionals there is a fruitful theory of sample spaces S(C) and probability spaces (a.k.a. couplings) P(C) over it.
In my recent LICS paper I showed that S(C) always carries an *independence structure* which allows for an abstract development of Alex Simpson-style probability sheaves, a topos where random variables are first-class objects. In upcoming work with Paolo Perrone, Matthew Di Meglio and Chris Heunen, we found that this independence structure arises purely from the †-structure on P(C), which is given by Bayesian inversion. Formally, we establish an equivalence between *epiregular independence categories* and *dagger categories with dilators* that parallels the equivalence of regular categories and tabular allegories.
</div>
</details>
</li>
<li>15:45-16:15 <i>break</i> </li>
<li>
<details>
<summary>16:15-16:45 Makoto Fujiwara, On the separation techniques of weak logical principles over intuitionistic arithmetic
</summary>
<div><b>Abstract:</b>
In these several decades, the hierarchy of weak fragments of logical principles over intuitionistic arithmetic has been studied systematically.
These principles include the law-of-excluded-middle, the double-negation-elimination and De morgan's law.
In this talk, we overview the research on the hierarchy and discuss about the separation techniques between these principles.
</div>
</details>
</li>
<li>
<details>
<summary>16:45-17:15 Pim Otte, Tutte's theorem as an educational formalization project
</summary>
<div><b>Abstract:</b>
Tutte's theorem is a core result in graph theory, which the describes conditions for existence of perfect matchings in graphs. I have formalized this theorem in Lean and it is ready for inclusion in mathlib. Additionally, I extracted a framework for educational formalization projects, based on this project that I undertook to learn more about formalization. In this talk, I will discuss some interesting elements of the formalization of Tutte's theorem, as well as this educational framework. I propose that this framework can be applied both in traditional and community-driven educational settings and that it helps to efficiently teach formalization by minimizing teacher input.
</div>
</details>
</li>
<li>18:00: Dinner at <a href="https://www.wagamama.nl/restaurants/utrecht">Wagamama</a></li>
</ul>
<h2>DutchCATS meeting in Nijmegen, 7 February 2025</h2>
<h3>Location</h3>
We meet in Room HG00.303 in the Huygens building
(see the <a href="https://www.ru.nl/over-ons/de-campus/gebouwen-en-ruimtes/huygensgebouw">campus map</a>).
Registration is free, and you can register <a href="https://forms.gle/NfAKL3UtWQyuiCHo9">here</a>.
<h3>Programme</h3>
<p style="margin-left: 40px;"><em>arrival (13:30)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>13:40-14:05 Nima Rasekh, From Mathematical Foundations to (Higher) Categories
</summary>
<div><b>Abstract:</b>
Given a particular mathematical foundation, such as a set theory, we can construct a suitable category of
sets, which we can prove to be cocomplete. This suggests a similar homotopical analogue, namely that for every
foundation, the suitably defined higher category of ``homotopy types" is also cocomplete. The aim of this talk
is to analyze the relation between foundational assumptions and this question, with (possibly) surprising
implications. No prior knowledge of higher category theory is assumed for this talk.
</div>
</details>
</li>
<li>
<details>
<summary>14:05-14:30 Lukas Mulder, The Functorial Nature of Enriched Data Types
</summary>
<div><b>Abstract:</b>
Many data types can be modeled categorically as an initial object, and are called inductive data types.
Examples of such data types are booleans, lists, trees and more generally algebraic data types and
containers/W-types.
Being an initial object means there always exists a unique homomorphism out of this object, for a notion of
homomorphism corresponding to the data type. This fact can be used to define functions on these datatypes
inductively (using the existence of a homomorphism) and to prove properties of these functions (using the
uniqueness of the homomorphism).
If we relax the notion of homomorphism slightly, we can gain more control over the inductively defined
functions. We can also generalize the idea of an initial object while still maintaining the crucial properties
of existence and uniqueness, yielding many more (generalized) inductive datatypes.
Lastly, given a (natural) transformation between two inductive data types, we see this respects the notion of
generalized homomorphism as well. This transformation also extends to the generalized inductive data types,
giving us tools to generate more data types from existing ones.
In this talk, we will go over the above theory using the natural numbers and lists as guiding examples.
</div>
</details>
</li>
<li>14:30-14:55 <i>break</i> </li>
<li>
<details>
<summary>14:55-15:20 Tom de Jong, Ordinal Exponentiation in Homotopy Type Theory
</summary>
<div><b>Abstract:</b>
While ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has
seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation
has thus far been missing.
I will present two seemingly different definitions of constructive ordinal exponentiation in the setting of
homotopy type theory. The first is abstract, uses suprema of ordinals, and is solely motivated by the expected
equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version
of a classical construction by Sierpiński based on functions with finite support.
A key result is that the two approaches are equivalent (whenever it makes sense to ask the question), and that
we can use this equivalence to prove algebraic laws and decidability properties of the exponential.
All results are formalized in the proof assistant Agda and are written up in the recent preprint
arXiv:2501.14542. This is joint work with Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu.
</div>
</details>
</li>
<li>
<details>
<summary>15:20-15:45 Fernando Chu, Towards a fully functorial directed type theory
</summary>
<div><b>Abstract:</b>
In this talk, we present our work in progress in directed type theory. The syntax and semantics follows
roughly the presentation in North (2019), with the main difference being a new context extension operation;
which semantically represents (dependent) two sided fibrations. After studying this construction , we show how
we can state a different elimination principle for the hom-type, which gives us more expressive power. This is
joint work with Paige North and Éléonore Mangel.
</div>
</details>
</li>
<li>15:45-16:10 <i>break</i> </li>
<li>
<details>
<summary>16:10-16:35 Márk Széles, Categories of partial probabilistic computations
</summary>
<div><b>Abstract:</b>
In the last few years, Markov categories have become the standard setting for categorical probability theory.
Morphisms in such Markov categories can be thought of as total probabilistic computations. However, many
operations in probability theory are inherently partial. An important example is Bayesian updating: if one is
presented with evidence incompatible with the prior belief, then the update cannot be performed. For this
reason, there is a renewed interest in categories of partial probabilistic computations, using the theory of
so-called copy-discard categories. In this talk, I will give a broad overview of this partial approach to
categorical probability theory, focusing on the abstract treatment of normalisation and disintegration of
subprobability measures.
</div>
</details>
</li>
<li>
<details>
<summary>16:35-17:00 Bálint Kocsis, Complete Test Suites for Automata in Monoidal Closed Categories
</summary>
<div><b>Abstract:</b>
Conformance testing of automata is about checking the equivalence of a known specification and a black-box
implementation. An important notion in conformance testing is that of a complete test suite, which guarantees
that if an implementation satisfying certain conditions passes all tests, then it is equivalent to the
specification.
We introduce a framework for proving completeness of test suites at the general level of automata in monoidal
closed categories. Moreover, we provide a generalization of a classical conformance testing technique, the
W-method. We demonstrate the applicability of our results by recovering the W-method for deterministic finite
automata, Moore machines, and Mealy machines, and by deriving new instances of complete test suites for
weighted automata and deterministic nominal automata.
</div>
</details>
</li>
<li>18:00: Dinner at <a href="https://restaurantdehemel.nl/">De Hemel</a></li>
</ul>
<h2>DutchCATS meeting in Leiden, 05 June 2024</h2>
<h3>Location</h3>
We meet in Room CE.0.08 in the Gorlaeus building
(see the <a href="https://www.universiteitleiden.nl/en/locations/gorlaeus-building#tab-1">campus map</a>).
You can register for the meeting
<a
href="https://docs.google.com/forms/d/e/1FAIpQLSekyJwWfErmeGrC0_UWLbTZRWl46PkDoiNZNVMzAO6QrDN3Hg/viewform?usp=sf_link">here</a>.
<h3>Programme</h3>
(click to reveal abstracts)
<p style="margin-left: 40px;"><em>arrival and coffee (available from 12:30)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>[13:00-13:40]
Umberto Tarantino, Triposes and toposes through arrow algebras <a
href="./2024-05-06/slides-tarantino.pdf">slides</a></summary>
<p style="margin-left: 25px;">
Tripos theory offers a very general and flexible framework for topos theory which unifies both localic and
realizability
toposes as instances of a common construction. However, the notion of tripos is still very high-level when
compared to both
frames and partial combinatory algebras: the main approach to a more concrete unifying notion is given by
Miquel's implicative
algebras. In this talk, I will present arrow algebras, a generalization of implicative algebras as structures
inducing triposes.
Based on the work of my Master Thesis, I will introduce appropriate categories of arrow algebras, and show how
they perfectly
factor through both the localic and the realizability examples with respect to geometric morphisms of the
associated triposes.
Time permitting, I will also present a notion of nuclei on an arrow algebra generalizing the
locale-theoretical analogue, and sketch
how they correspond to subtoposes of the induced topos.
</p>
</details>
</li>
<li>
<details>
<summary>[13:40-14:20] Henning Basold, Simplicial and higher coalgebras</summary>
<p style="margin-left: 25px;">
There is an intricate link between concurrent systems and homotopy theory that has been exploited, for
instance, in higher-dimensional
automata and their languages. An abstraction of computation is the theory of coalgebra, which provides a
general understanding of step-wise
computation, global behaviour, modal logic and many other concepts of computation and reasoning. In this talk,
I will provide first an introduction
to coalgebra in the setting of simplicial sets and how concurrent computing can be understood there. After
this, we will see that the link between
computation and homotopy theory goes very deep. This merits an abstract development of homotopy theory for
computation, for which I will sketch an
outline in the form of higher coalgebra, which I understand as coalgebra in the context of higher categories.
We will discuss the intuition and
ingredients that go into such a theory, which will bring us back to coalgebras on simplicial sets.
</p>
</details>
</li>
</ul>
<p style="margin-left: 40px;"><em>break (20 min)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>[14:40-15:20]
Henning Urbat, Operational techniques for higher-order coalgebras <a
href="./2024-05-06/slides-urbat.pdf">slides</a></summary>
<p style="margin-left: 25px;">
Higher-order coalgebras are a form of coalgebra whose type is given by a mixed variance bifunctor rather than
an endofunctor. While standard coalgebras
model automata and state-based transition systems, higher-order coalgebras provide a categorical abstraction
of operational models of higher-order
languages such as the lambda-calculus. We discuss (1) how to specify higher-order coalgebras using
higher-order GSOS laws, and (2) how to reason
about them using generalized operational techniques such as Howe's method and logical relations. This talk
surveys recent work with Sergey Goncharov,
Stefan Milius, Lutz Schröder and Stelios Tsampas presented at POPL'23, LICS'23, LICS'24.
</p>
</details>
</li>
</ul>
<p style="margin-left: 40px;"><em>break (20 min)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>[15:40-16:20]
Ruben Turkenburg, Proving behavioural apartness <a href="./2024-05-06/slides-turkenburg.pdf">slides</a>
</summary>
<p style="margin-left: 25px;">
In this talk I will be discussing notions of apartness on state-based systems. In contrast to coinductive
notions of equivalence (e.g. bisimilarity), apartness
defines which states of a system behave differently. I will start with a simple example of how we may
determine apartness on a state-based system, which will
show one of the main benefits of apartness over equivalence notions such as bisimilarity. Namely, that it may
be determined by giving a finite witness or proof.
I will go on to discuss recent work of Geuvers and Jacobs which develops a theory of proof systems for
apartness, and show that in the case of probabilistic systems,
this does not yield finite proofs in general. This will lead us to our new approach to obtaining proof systems
for apartness, yielding finite proofs for a larger variety
of state-based systems modelled as coalgebras for a certain class of functors. This talk is based on joint
work with Harsh Beohar, Clemens Kupke, and Jurriaan Rot.
</p>
</details>
</li>
<li>
<details>
<summary>[16:20-17:00]
Dario Stein, Two types of *do*: functional programming with interventions and counterfactuals <a
href="./2024-05-06/slides-stein.pdf">slides</a> </summary>
<p style="margin-left: 25px;">
Pearl's famous do-calculus is used to express causal and counterfactual reasoning in statistical models, but
it can also be naturally understood
as a transformation of probabilistic functional programs. I am going to present work-in-progress about
representing such intervenable computation in a
compositional and type-safe way. This question warrants an excursion into graded monads, locally graded
categories and double categories.
</p>
</details>
</li>
</ul>
<p style="margin-left: 40px;"><em>relocate (e.g. by bike or bus) to restaurant and dinner</em></p>
Dinner will be at <a href="https://www.waagleiden.nl/nl/"> De Waag</a> from 18:00 (at your own expense).
<h2>DutchCATS meeting in Amsterdam, 25 March 2024</h2>
<h3>Location</h3>
We meet in Room D1.112 in Science Park 904 (see the <a
href="https://www.uva.nl/over-de-uva/organisatie/faculteiten/faculteit-der-natuurwetenschappen-wiskunde-en-informatica/locatie-en-contact/routebeschrijving/routebeschrijving-fnwi.html">campus
map</a>).
You can register for the meeting <a href="https://forms.gle/aLFzAUSqS8E3Ymta7">here</a>.
<h3>Programme</h3>
(click to reveal abstracts)
<p style="margin-left: 40px;"><em>arrival and coffee (available from 13:00)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>[13:30-14:15] Matteo Acclavio, Constructive modal logic: game semantics and lambda-calculi </a>
</summary>
<p style="margin-left: 25px;">Constructive modal logics are obtained by extending intuitionistic propositional
logic with modalities. This talk will present a line of work aiming at studying the proof equivalence for the
constructive modal logic CK. In particular, I will introduce the game semantics for CK, and a new modal lambda
calculus which has been designed to recover the one-to-one correspondence between winning innocent strategies
and normal lambda-terms, akin to the correspondence observed in propositional intuitionistic logic. <br>
<br>
This talk is based on joint works with Davide Catta, Federico Olimpieri and Lutz Strassburger. <br>
<br>
Proof equivalence: https://inria.hal.science/hal-03909538 <br>
Game semantics: https://link.springer.com/chapter/10.1007/978-3-030-86059-2_25 <br>
Lambda-calculus: https://link.springer.com/chapter/10.1007/978-3-031-43513-3_19
</p>
</details>
</li>
<li>
<details>
<summary>[14:15-15:00] Patrick Forré, Quasi-measurable spaces - A convenient foundation of probability
theory <a href="./2024-25-03/slides_forre.pdf">slides</a> </summary>
<p style="margin-left: 25px;">We introduce the category of quasi-measurable spaces and endow each such space
with a set of 'well-behaved' push-forward probability measures. It turns out that these constructions produce
a strong probability monad on a quasitopos. This thus allows for a dependent type theory for higher-order
probabilistic programs. We also show that we can extend classical results like Fubini, Kolmogorov extension,
disintegration, de Finetti to this setting. We also highlight how some foundational problems in the area of
stochastic processes, probabilistic graphical models and causality are solved. <br>
<br>
This talk is based on the following references: <br>
- C. Heunen, O. Kammar, S. Staton, H. Yang. "A convenient category for higher-order probability theory". 32nd
Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1-12. IEEE, 2017. <br>
- P. Forré. "Quasi-Measurable Spaces". Preprint, arXiv:2109.11631, 2021.
</p>
</details>
</li>
</ul>
<p style="margin-left: 40px;"><em>break (30 min)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>[15:30-16:15] Chase Ford, Monads on categories of relational structures <a
href="./2024-25-03/slides_ford.pdf">slides</a> </summary>
<p style="margin-left: 25px;"> A celebrated result in category theory is the equivalence between the algebraic
theories of Lawvere, the equational
theories of universal algebra, and finitary monads on the category of sets. The aim of this talk is to discuss
a generic
framework of universal relational algebra in categories of relational structures given by a finitary
relational signature
and (potentially infinitary) Horn theories, generalizing the classical notion of equational theory. Instances
include the
category of posets and the category of 1-bounded metric spaces. We will sketch the theory-to-monad part of a
correspondence between the ensuing notion of relational algebraic theory and enriched accessible monads on the
given base category. The content of this talk is based on joint work with Stefan Milius and Lutz Schröder.</p>
</details>
</li>
<li>
<details>
<summary>[16:15-17:00] Lingyuan Ye, Stack representation of first-order intuitionistic theories</summary>
<p style="margin-left: 25px;">There is a classical result of Pitts that propositional intuitionistic logic
eliminates second order propositional quantifiers. Later, Ghilardi and Zawadowski worked out a semantic proof
of this by developing a sheaf representation of finitely presented Heyting algebras. The basic idea is to
represent a Heyting algebra via its collection of models on finite Kripke frames, expressed in a suitable
categorical and sheaf-theoretic language. Their representation allows them to show the left exact syntactic
category of the theory of Heyting algebras is in fact itself a Heyting category, which has many logical
consequences. In this talk, I will briefly recall these classical result and show the possibility of extending
these developments to a suitable class of first-order intuitionistic theories. In particular, I will explain
how to construct higher sheaf representation of first-order intuitionistic theories, and discuss some possible
outcomes.</p>
</details>
</li>
</ul>
<p style="margin-left: 40px;"><em>walk to restaurant and dinner</em></p>
Dinner will be at <a href="https://www.cafe-restaurantpolder.nl">De Polder</a> (at your own expense)
<h2>DutchCATS meeting in Eindhoven, 2 February 2024</h2>
<h3>Time and location</h3>
We meet in lecture room MF13 (5th floor) at the MetaForum between 13:00 and 17:00.
<iframe
src="https://www.google.com/maps/embed?pb=!1m14!1m8!1m3!1d4973.233487484942!2d5.487086!3d51.446832!3m2!1i1024!2i768!4f13.1!3m3!1m2!1s0x47c6d8e04bc52af9%3A0x20fe44840cbbb233!2sMetaForum!5e0!3m2!1snl!2snl!4v1703192959341!5m2!1snl!2snl"
width="600" height="450" style="border:0;" allowfullscreen="" loading="lazy"
referrerpolicy="no-referrer-when-downgrade"></iframe>
<h3>Registration</h3>
You can register for the meeting by filling out <a
href="https://forms.office.com/Pages/ResponsePage.aspx?id=R_J9zM5gD0qddXBM9g78ZJgiwXyBFW1CvgmTN3L4g_pUMUZHSThNT1M4QVExWlhNMjZGWFBJUEdVVy4u">this
form</a>.
<h3>Programme</h3>
(click to reveal abstracts)
<p style="margin-left: 40px;"><em>arrival and coffee (available from 12:30)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>[13:00-13:30] Anna Schenfisch, Algebraic K-Theory of Persistence Modules, <a
href="./2024-02-02/AnnaSchenfisch.pdf">slides</a></summary>
<p style="margin-left: 25px;">Persistence modules are usually introduced to students through topological data
analysis, since they are the main tool used to record information about a filtered space. However, it is also
natural to define them from a purely algebraic viewpoint, for example, as functors from combinatorial entrance
path categories or as cosheaves over some parameter space. From any of these algebraic definitions, we can
then discuss the algebraic K-theory of persistence modules. We will find and interpret the K-theory of a
particular class of persistence modules, as well as discuss how this result might be extended more generally.
The intention of this talk is to leave listeners with a greater appreciation for persistence modules,
algebraic K-theory, and the interesting content at the intersection of these ideas.</p>
</details>
</li>
<li>
<details>
<summary>[13:30-14:00] Lingyuan Ye, Categorical Structures in Theory of Arithmetic, <a
href="./2024-02-02/LingyuanYe.pdf">slides</a></summary>
<p style="margin-left: 25px;">In this talk, we provide a categorical analysis of the arithmetic theory 𝐼Σ1. We
will provide a categorical proof of the classical result that the provably total recursive functions in 𝐼Σ1
are exactly the primitive recursive functions. Our strategy is to first construct a coherent theory of
arithmetic 𝕋, and prove that 𝕋 presents the initial coherent category equipped with a parametrised natural
number object. This allows us to derive the provably total functions in 𝕋 are exactly the primitive recursive
ones, and establish some other constructive properties about 𝕋. We also show that 𝕋 is exactly the
Π2-fragment of 𝐼Σ1, and conclude they have the same class of provably total recursive functions.</p>
</details>
</li>
</ul>
<p style="margin-left: 40px;"><em>break (30 min)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>[14:30-15:00] Jan Heemstra, Hardware Accelerated Intelligent Theorem Proving, <a
href="./2024-02-02/JanHeemstra.pdf">slides</a></summary>
<p style="margin-left: 25px;">We present a connection-based tableaux theorem prover that performs inferences
entirely on the GPU. Benchmarks on the m40 dataset show it performs worse than other provers in terms of
proving power. In terms of inferences per second, however, it is on par with or even surpassing
state-of-the-art provers on similarly priced and dated hardware, despite it lacking various important
optimizations that are present in the other provers. On top of this prover, we designed and implemented a
heuristic neural network-based system that avoids evaluations during the computation of inferences, and
instead pre-computes the results of these evaluations.</p>
</details>
</li>
<li>
<details>
<summary>[15:00-15:30] Wouter Fransen, Grothendieck Topologies on the Category of Finite Probability Spaces
</summary>
<p style="margin-left: 25px;">In this talk, I will present the results from my Bachelor project. The goal of
this project was to get a better understanding of category-theoretic concepts like Grothendieck topologies and
sheaves, by looking at their incarnations for a concrete example: the category Prob of finite probability
spaces. Our main question was, can we find a “non-trivial” Grothendieck topology on Prob? And if so, are they
subcanonical?</p>
</details>
</li>
</ul>
<p style="margin-left: 40px;"><em>break (30 min)</em></p>
<ul style="list-style-type: none;">
<li>
<details>
<summary>[16:00-17:00] [Replacement programme] Jim Portegies, Workshop on Models for Synthetic Calculus, <a
href="./2024-02-02/Handout workshop Models for Synthetic Calculus.pdf">hand-out</a></summary>
<p style="margin-left: 25px;">The hand-out serves as a short introduction to Synthetic Calculus (a.k.a.
Synthetic Differential Geometry) by means of looking at the model of C^∞-rings. The workshop was originally
developed for our colleagues from scientific computing, applied analysis, and applied differential geometry.
Since they have little to no experience with category theory or topos theory, the hand-out does not rely on
category-theoretical concepts, but we do try to connect with these. We chose to introduce Synthetic Calculus
via a model since this allows one's thinking to remain wholly classical (to the comfort of our colleagues),
and it avoids unproductive discusssions of a philosophical nature.</p>
</details>
</li>
<li>
<details>
<summary><s>Valentina Castiglioni, On the Axiomatisation of Weak Bisimulation-based Congruences over CCS</s>
(canceled)</summary>
<p style="margin-left: 25px;">In this talk we will discuss some of our achievements on the equational theory of
(the restriction, relabelling, and recursion free fragment of) CCS modulo four classic bisimulation-based
notions of equivalence that abstract from internal computational steps in process behaviour, i.e., the rooted
versions of branching, $\eta$, delay, and weak bisimilarities.</p>
</details>
</li>
<li>
<details>
<summary><s>Bálint Kocsis, Normalization for simply typed lambda-calculus</s> (canceled)</summary>
<p style="margin-left: 25px;">I will present part of the work I have done for my master's thesis. In my thesis,
I prove normalization for the simply typed lambda-calculus in different ways and compare the proofs in detail.
My talk will touch upon two methods: normalization by evaluation and categorical gluing. The aim of the talk
is to show how category theory is a useful tool to study metatheoretic properties of type systems. In
particular, I will illustrate through the example of normalization how the categorification of already
established results can extend the theory and make it applicable to a wider range of problems.</p>
</details>
</li>
</ul>
<p style="margin-left: 40px;"><em>walk to restaurant and dinner</em></p>
Dinner at restaurant Bommel at 18:00 (at own expense).
<iframe
src="https://www.google.com/maps/embed?pb=!1m18!1m12!1m3!1d2487.157665345947!2d5.472489976314017!3d51.436898315851785!2m3!1f0!2f0!3f0!3m2!1i1024!2i768!4f13.1!3m3!1m2!1s0x47c6d9045c49de15%3A0x6a4cd2da13ae85dd!2sEetcaf%C3%A9%20Bommel!5e0!3m2!1snl!2snl!4v1706809539566!5m2!1snl!2snl"
width="600" height="450" style="border:0;" allowfullscreen="" loading="lazy"
referrerpolicy="no-referrer-when-downgrade"></iframe>
<h2>DutchCATs meeting in Nijmegen, 3 November 2023</h2>
<h3>Location</h3>
We meet in HG00.308 in the <a
href="https://www.ru.nl/over-ons/de-campus/gebouwen-en-ruimtes/huygensgebouw">Huygensgebouw</a> between 13:00 and
17:00.
You can register for the meeting <a href="https://forms.gle/Phhrru5KRpHPxKwL8">here</a>.
<h3>Programme</h3>
<div class="container">
<ul style="list-style-type: none">
<li>
<details>
<summary>13:00-13:30 Dario Stein, New Topics in Markov Categories, <a href="./2023-11-03/dario.pdf">slides</a>
</summary>
<div><b>Abstract:</b> I will discuss some new insights in categorical probability, such as copartiality,
convex analysis and a sheaves of random variables
</div>
</details>
</li>
<li>
<details>
<summary>13:30-14:00 Pedro Nora, Maximally permissive notions of bisimulation
</summary>
<div><b>Abstract:</b> In this talk we will show that Set-valued functors that preserve inverse images admit a
maximally permissive notion of bisimulation induced by a normal lax extension.
</div>
</details>
</li>
<li>14:00-14:30 Coffee break </li>
<li>
<details>
<summary>14:30-15:00 Nima Rasekh, Univalent Double Categories, <a href="./2023-11-03/nima.pdf">slides</a>
</summary>
<div><b>Abstract:</b> The aim of this talk is to discuss possible formalizations of the notion of double
category in Coq UniMath and various theoretical challenges one encounters in this situation. This is joint
work with Benedikt Ahrens, Paige North and Niels van der Weide.
</div>
</li>
<li>
<details>
<summary>15:00-15:30 Kobe Wullaert, Rezk Completions in Formal Category Theory, <a
href="./2023-11-03/kobe.pdf">slides</a>
</summary>
<div><b>Abstract:</b> TBA
</div>
</details>
</li>
<li>15:30-16:00 Coffee break </li>
<li>
<details>
<summary>16:00-16:30 Jelle Wemmenhove, <a href="./2023-11-03/jelle.pdf">slides</a>
</summary>
<div><b>Abstract:</b> At the TU/e, we have been using a customized version of the Coq proof assistant to help
teach students how to write mathematical proofs. The software is called Waterproof, it consists of a custom
proof language and a custom editor. The proof language provides tactics for writing Coq proofs that more
closely resemble the style of regular math proofs. For example, the custom tactic notations take the form of
full English sentences, and the focus is placed on types, which carry the relevant mathematical information,
instead of on terms. The custom editor allows for the use of mixed documents which contain both
human-readable text and verifiable mathematics. It contain some quality-of-life features, like
autocompletion for typing mathematical symbols and tactics, as well as features specifically designed for
use in education, like the ability to limit student input to certain parts of a document. We will discuss
Waterproof, its aims and its features, as well as how the software is used in the Analysis 1 course at the
TU/e, and some limitations that we face with the creation of mathematical libraries that are accessible to
first-year undergraduate students.
</div>
</details>
</li>
<li>
<details>
<summary>16:30-17:00 Arnoud van der Leer, <a href="./2023-11-03/arnoud.pdf">slides</a>
</summary>
<div><b>Abstract:</b> My talk will be about the work I have been doing for my master's thesis. For this
thesis, I am studying the 2013 paper "Classical lambda calculus in modern dress" by Martin Hyland, and
formalizing a part of it. I will (probably) outline the contents of the paper, and discuss some of the
challenges that arise in formalizing it.
</div>
</details>
</li>
<li>18:00: Dinner at <a href="https://restaurantdehemel.nl/">De Hemel</a></li>
</ul>
<h2>DutchCATS meeting in Delft, 6 September 2023</h2>
<h3>Location</h3>
We meet in the Snijderzaal (building 36)</a>, Mekelweg 4, 2628 CD Delft.
<h3>Programme</h3>
<ul>
<li>14:00 - 15:00 Fabian Zickgraf</li>
<li>15:00 - 15:30 Benno van den Berg</li>
<li>15:30 - 16:00 Break</li>
<li>16:00 - 16:30 Daniel Otten</li>
<li>16:30 - 17:00 Andreas Nuyts</li>
<li>17:00 - 17:30 Luc Chabassier</li>
<li>18:30 Dinner at <a href="https://delftsbrouwhuis.nl/en/home-en/">Delfts Brouwhuis</a> at Hippolytusbuurt 43,
2611 HM Delft (<a href="https://goo.gl/maps/sZHpkomBpE2j1aVz6">Google Maps</a>)</li>
</ul>
<h2>Strength of Weak Type Theory, Amsterdam, 11 and 12 May 2023 </h2>
On Thursday 11 and Friday 12 May we will organise a workshop on weak type theories.
<h3>Programme</h3>
<h4>Thursday 11 May</h4>
Location: room B0.208 in SP 904 on the Science Park, Amsterdam (see the <a
href="https://www.uva.nl/over-de-uva/organisatie/faculteiten/faculteit-der-natuurwetenschappen-wiskunde-en-informatica/locatie-en-contact/routebeschrijving/routebeschrijving-fnwi.html">campus
map</a>).
<div class="container">
<ul style="list-style-type: none">
<li>
<details>
<summary>11:00-12:00 Daniel Otten, Models for propositional type theory <a
href="./Weak_type_theories/slides_otten.pdf">slides</a>
</summary>
<div><b>Abstract:</b> As the first talk of the workshop, we start by explaining and motivating
propositional/weak/objective type theory (PTT), which is a type theory without any reduction rules. We
compare two different categorical notions that aim to model PTT: compression categories with propositional
identity types, and path categories. Although comprehension categories are well-studied, demonstrating
that a category has the required structure for PTT can be difficult. Path categories simplify the
requirements by taking inspiration from abstract homotopy theory. In this talk we will show an equivalence
between these two notions, building upon the work of the invited speakers, and highlighting how their
research connects.
</div>
</details>
</li>
<li> Lunch</li>
<li>
<details>
<summary>13:30-14:30 Theo Winterhalter, A conservative and constructive translation from extensional type
theory to weak type theory <a href="./Weak_type_theories/slides_winterhalter.pdf">slides</a> </summary>
<div><b>Abstract:</b> I will present work conducted a few years ago with Simon Boulier on translating ETT to
WTT, which we formalised in the Coq proof assistant. This translation starts a typing derivation
potentially using equality reflection and produces a proof certificate that can be trivially checked to be
correct. This in a sense echoes De Bruijn’s <it></it>plea for weaker frameworks</it> since the translation
in particular shows that ETT (and thus intensional type theory) is conservative over WTT.</div>
</details>
</li>
<li>
Coffee break </li>
<li>
<details>
<summary>15:00-16:00 Sam Speight, Higher-Dimensional Realizability for Intensional Type Theory <a
href="./Weak_type_theories/slides_speight.pdf">slides</a> </summary>
<div><b>Abstract:</b> I will describe recent work on higher-dimensional realizability models of intensional
type theory. The notion of model that we employ is that given by path categories. The models are based on
groupoids, and realizers themselves carry higher-dimensional structure, so that a realizer for an
identification (isomorphism) is a "path".</div>
</details>
</li>
<li>Coffee Break</li>
<li>
<details>
<summary>16:30-17:30 Discussion</summary>
</details>
</li>
<li>18:30 Conference dinner at <a href="https://abeautifulmess.nl/en/home">A Beautiful Mess</a></li>
</ul>
<h4>Friday 12 May</h4>
Location: room L1.12 (morning) and room L1.17 (afternoon) in Lab 42 on the Science Park, Amsterdam (see the <a
href="https://www.uva.nl/over-de-uva/organisatie/faculteiten/faculteit-der-natuurwetenschappen-wiskunde-en-informatica/locatie-en-contact/routebeschrijving/routebeschrijving-fnwi.html">campus
map</a>).
<div class="container">
<ul style="list-style-type: none">
<li>
<details>
<summary>10:00-11:00 Matteo Spadetto, Weak type theories: A conservativity result for homotopy elementary
types <a href="./Weak_type_theories/slides_spadetto.pdf">slides</a>
</summary>
<div><b>Abstract:</b> In this talk, we consider a dependent type theory that includes propositional
identity types, propositional dependent sum types, and propositional dependent product types: in other
words, the intensional identities, the dependent sums, and the dependent products of our theory satisfy
the usual Martin-Löf computation rules, but only in propositional form (see [3, 4, 5]). We will refer to
such a theory as a weak type theory (or a propositional type theory). In a recent paper [6] the authors
conjecture that such a theory is sufficient for performing all of constructive mathematics and
formalising most of the HoTT book. <br>
The aim of this talk is to address this question, by identifying a particular family of type-judgements,
called h-elementary, of a weak type theory such that the corresponding extensional type theory is
conservative over it relative to the family of h-elementary types. Our main result informally asserts
that, for judgements essentially concerning h-sets, despite the non-negligible weakening of the weak
type theories with respect to the extensional ones, reasoning with the latter or the former is
equivalent. <br>
Our argument is fully presented in [7]. It is obtained by adapting a proof strategy introduced in [2]
and exploits the notion of category with attributes [1] to phrase the semantics of theories of dependent
type. <br>
[1] 1991. Moggi. A category-theoretic account of program modules. <br>
[2] 1995. Hofmann. Conservativity of equality reflection over intensional type theory. <br>
[3] 2013. Coquand, Danielsson. Isomorphism is equality. <br>
[4] 2018. van den Berg. Path categories and propositional identity types. <br>
[5] 2020. Bocquet. Coherence of strict equalities in dependent type theories. <br>
[6] 2021. van den Berg, den Besten. Quadratic type checking for objective type theory. <br>
[7] 2023. Spadetto. A conservativity result for homotopy elementary types in dependent type theory. <br>
</div>
</details>
</li>
<li>Coffee break</li>
<li>
<details>
<summary>11:30-12:30 Benno van den Berg, Towards homotopy canonicity for propositional type theory <a
href="./Weak_type_theories/slides_van_den_berg.pdf">slides</a> </summary>
<div><b>Abstract:</b> At TYPES 2019 Christian Sattler presented joint work with Chris Kapulkin showing
that ordinary homotopy type theory satisfies homotopy canonicity. I will explain why I believe their
method should work for propositional type theory as well. Indeed, for propositional type theory homotopy
canonicity is arguably more natural, because it is the only type of canonicity that can be expected.
</div>
</details>
</li>
<li>Lunch </li>
<li>
<details>
<summary>14:00-15:00 Rafael Bocquet, Towards coherence theorems for equational extensions of type theories
<a href="./Weak_type_theories/slides_bocquet.pdf">slides</a>
</summary>
<div><b>Abstract:</b> The conservativity of Extensional Type Theory (ETT) over Intensional
Type Theory (ITT) was proven by Martin Hofmann. The proof relies on
the presence of the Uniqueness of Identity Proofs (UIP) principle in
ITT. <br>
In this talk, I will present my progress towards generalization of
these results to type theories without UIP, such as variants of HoTT.</div>
</details>
</li>
<li>Coffee Break</li>
<li>
<details>
<summary>15:30-17:30 Discussion</summary>
</details>
</li>
</ul>
<h3>Registration</h3>
Registration is free of charge, but mandatory. Please register via this <a
href="https://forms.gle/fV8VPP31kJzuTUpm7">Google Form</a>.
<h2>DutchCATS meeting in Utrecht, 20 March 2023</h2>
<h3>Location <span style="color:#FF0000" ;>(Please note: location has changed due to local transport
strikes)</span></h3>
<p>Living Lab Digital Humanities, room 0.32, University Library City Centre, Drift 27 in the city center of
Utrecht (see <a
href="https://www.uu.nl/en/university-library/practical-information/locations/university-library-city-centre">this
page</a>)</p>
<p><s>KRUYT - O126 in the Science Park in Utrecht (see <a href="https://www.uu.nl/en/hugo-r-kruyt-building">this
page</a>)</s></p>
<h3>Program</h3>
<div class="container">
<ul>
<li>
<details>
<summary>14:00-14:50 Peter LeFanu Lumsdaine, The hierarchy of iterative sets in type theory
</summary>
<div>In ZF(C) and similar material set-theoretic foundations, the cumulative hierarchy of iterative sets
provides the arena in which all mathematics takes place. In other foundations, its place is less
central; but it still exists, as a rich and useful structure.
<br>
In this (mainly expository) talk, I will survey several treatments of the cumulative hierarchy and
variants in type theory and related settings, including:
<br>
<ul>
<li> Aczel/Leversha’s type of iterative sets </li>
<li> Gylterud’s refinements of this in the HoTT setting (https://arxiv.org/abs/1612.05468) </li>
<li> Moerdijk and Joyal’s “Algebraic set theory” characterisation of the cumulative hierarchy </li>
<li> the HoTT book’s presentation of the cumulative hierarchy as a higher inductive type</li>
<li> Palmgren’s applications of to modelling type theory (https://arxiv.org/abs/1909.01414)</li>
</ul>
</div>
</details>
</li>
<li>Coffee Break</li>
<li>
<details>
<summary>15:30-16:00 Morgan Rogers, Recovering topological endomorphism monoids (and automorphism
groups) with classifying toposes</summary>
<div>In my thesis, I examined toposes of actions of topological monoids on sets. In this talk, I will
show how that work fits into the setting of classifying toposes, and describe some work in progress on
extracting generalizations of classic model theory results from this construction.</div>
</details>
</li>
<li>
<details>
<summary>16:10-16:40 Tom de Jong, Epimorphisms and acyclic types</summary>
<div>It is well known that the epimorphisms in the category of sets are
exactly the surjections. But what are the epimorphisms of types?
Thinking of types as spaces, and following literature in algebraic
topology, we characterise epimorphisms of types in homotopy type theory
(HoTT) as so-called acyclic maps. An acyclic map is a map whose fibres
are acyclic types, and a type is acyclic if its suspension is contractible.
We also consider a weaker notion: a type is k-acyclic (for k ≥ -2) if
its suspension is k-connected. We show, for example, that the
classifying type of a group G is 2-acyclic if and only if the group G is
perfect, i.e. its abelianisation is trivial.