Dutch Categories And Types Seminar

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.

Mailing List and Zulip

We maintain a mailing list for discussion of everything related to categories and types, and for coordination of our meetings. We also have a Zulip server. Sign up at the signup page.

DutchCATS meeting in Leiden, 05 June 2024

Location

We meet in Room CE.0.08 in the Gorlaeus building (see the campus map). You can register for the meeting here.

Programme

(click to reveal abstracts)

arrival and coffee (available from 12:30)

break (20 min)

break (20 min)

relocate (e.g. by bike or bus) to restaurant and dinner

Dinner will be at De Waag from 18:00 (at your own expense).

DutchCATS meeting in Amsterdam, 25 March 2024

Location

We meet in Room D1.112 in Science Park 904 (see the campus map). You can register for the meeting here.

Programme

(click to reveal abstracts)

arrival and coffee (available from 13:00)

break (30 min)

walk to restaurant and dinner

Dinner will be at De Polder (at your own expense)

DutchCATS meeting in Eindhoven, 2 February 2024

Time and location

We meet in lecture room MF13 (5th floor) at the MetaForum between 13:00 and 17:00.

Registration

You can register for the meeting by filling out this form.

Programme

(click to reveal abstracts)

arrival and coffee (available from 12:30)

break (30 min)

break (30 min)

walk to restaurant and dinner

Dinner at restaurant Bommel at 18:00 (at own expense).

DutchCATs meeting in Nijmegen, 3 November 2023

Location

We meet in HG00.308 in the Huygensgebouw between 13:00 and 17:00. You can register for the meeting here.

Programme

DutchCATS meeting in Delft, 6 September 2023

Location

We meet in the Snijderzaal (building 36), Mekelweg 4, 2628 CD Delft.

Programme

Strength of Weak Type Theory, Amsterdam, 11 and 12 May 2023

On Thursday 11 and Friday 12 May we will organise a workshop on weak type theories.

Programme

Thursday 11 May

Location: room B0.208 in SP 904 on the Science Park, Amsterdam (see the campus map).

Friday 12 May

Location: room L1.12 (morning) and room L1.17 (afternoon) in Lab 42 on the Science Park, Amsterdam (see the campus map).
  • 10:00-11:00 Matteo Spadetto, Weak type theories: A conservativity result for homotopy elementary types slides
    Abstract: 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.
    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.
    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.
    [1] 1991. Moggi. A category-theoretic account of program modules.
    [2] 1995. Hofmann. Conservativity of equality reflection over intensional type theory.
    [3] 2013. Coquand, Danielsson. Isomorphism is equality.
    [4] 2018. van den Berg. Path categories and propositional identity types.
    [5] 2020. Bocquet. Coherence of strict equalities in dependent type theories.
    [6] 2021. van den Berg, den Besten. Quadratic type checking for objective type theory.
    [7] 2023. Spadetto. A conservativity result for homotopy elementary types in dependent type theory.
  • Coffee break
  • 11:30-12:30 Benno van den Berg, Towards homotopy canonicity for propositional type theory slides
    Abstract: 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.
  • Lunch
  • 14:00-15:00 Rafael Bocquet, Towards coherence theorems for equational extensions of type theories slides
    Abstract: 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.
    In this talk, I will present my progress towards generalization of these results to type theories without UIP, such as variants of HoTT.
  • Coffee Break
  • 15:30-17:30 Discussion

Registration

Registration is free of charge, but mandatory. Please register via this Google Form.

DutchCATS meeting in Utrecht, 20 March 2023

Location (Please note: location has changed due to local transport strikes)

Living Lab Digital Humanities, room 0.32, University Library City Centre, Drift 27 in the city center of Utrecht (see this page)

KRUYT - O126 in the Science Park in Utrecht (see this page)

Program

  • 14:00-14:50 Peter LeFanu Lumsdaine, The hierarchy of iterative sets in type theory
    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.
    In this (mainly expository) talk, I will survey several treatments of the cumulative hierarchy and variants in type theory and related settings, including:
    • Aczel/Leversha’s type of iterative sets
    • Gylterud’s refinements of this in the HoTT setting (https://arxiv.org/abs/1612.05468)
    • Moerdijk and Joyal’s “Algebraic set theory” characterisation of the cumulative hierarchy
    • the HoTT book’s presentation of the cumulative hierarchy as a higher inductive type
    • Palmgren’s applications of to modelling type theory (https://arxiv.org/abs/1909.01414)
  • Coffee Break
  • 15:30-16:00 Morgan Rogers, Recovering topological endomorphism monoids (and automorphism groups) with classifying toposes
    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.
  • 16:10-16:40 Tom de Jong, Epimorphisms and acyclic types
    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. Finally, we comment on the relations between acyclic and connected maps, sketch directions for future research, and describe how the Higman group, a well-known example in combinatorial group theory, allows us to construct a nontrivial acyclic type. This is joint work with Ulrik Buchholtz and Egbert Rijke.
  • Coffee Break
  • 17:20-17:50 Thomas Lamiaux, Introduction and comparison of different approaches to Initial Semantics
    Initial Semantics is a categorical framework enabling to abstractly represent and manipulate syntax with binder e.g. lambda calculus, with an appropriate notion of substitution and recursion. This is of important as substitution is famously hard to account properly in a formal setting. In this talk, we will first consider different approaches that exist in the literature, before giving some elements on how the different approaches relates and can be seen as instances of a unified framework.
  • 19:00 Dinner at Krishna Vilas Utrecht

DutchCATS meeting in Amsterdam, 16 January 2023

Location

We meet in the Science Park, Amsterdam, in Building 904, Room A1.06 (see the campus map).

Program

  • 14:00 - 15:00 Sina Hazratpour, A 2-categorical proof of Frobenius for fibrations defined from a generic point slides
  • 15:00 - 16:00 Freek Geerligs, Symmetric effective Kan complexes with pictures slides
  • 16:00 - 16:30 Break
  • 16:30 - 17:30 Daniel Otten, Conservativity of the Calculus of Constructions over Higher-order Heyting Arithmetic slides
  • 18:00 Dinner at the Polder

DutchCATS meeting in Delft, 24 November 2022

Location

We meet in the Social Data Lab (SDL), on the ground floor of Electric Engineering, Mathematics & Computer Science (EEMCS), Van Mourik Broekmanweg 6, 2628 XE Delft. The SDL is right next to the entrance; the receptionists can point you to the SDL as well.

Program

  • 14:00 - 14:25 Niels van der Weide (slides)
  • 14:30 - 14:55 Kobe Wullaert (slides)
  • 15:00 - 15:25 Lingyuan Ye (slides)
  • 15:30 - 16:00 Break
  • 16:00 - 16:25 Thea Li (slides)
  • 16:30 - 17:00 Jeremy Kirn (slides)
  • 18:00 Dinner at De Gist

Informal workshop on Algebraic Weak Factorisation Systems, 2 May 2022

Program

  • 10:00-11:00: John Bourke (Masaryk University, Brno), An orthogonal approach to algebraic weak factorisation systems
  • 11:15-12:15: Wijnand van Woerkom (Utrecht University), The Frobenius property for algebraic weak factorisation systems (recording)
  • 13:15-14:15: Nicola Gambino (University of Leeds), The effective model structure on simplicial objects slides
  • 14:30-15:30: Benno van den Berg (University of Amsterdam), Effective Kan fibrations in simplicial sets (recording)
  • 16:00-17:00: Paige North (University of Pennsylvania), Two-sided and other generalizations of weak factorization systems (slides, recording)
  • 17:30-23:59: Dinner

Abstracts

Abstracts can be found here.

Location

The meeting is going to take place in the Science Park, Amsterdam, in Building 904, Room A1.04 (see the campus map).

Fourth Meeting: Zoom, 8 April 2022

Norihiro Yamada: Curry-Howard Isomorphisms without Commuting Conversions
  • Start: 16:00 Amsterdam time
  • Recording of the talk available on YouTube
  • Join at Zoom Meeting
  • Abstract In this talk, I present three term calculi in a uniform format that respectively embody classical, intuitionistic and linear logics. These term calculi are equipped with reductions that satisfy subject reduction, confluence and strong normalisation. An advantage of the term calculi is their simplicity: They dispense with the tangled (commuting) conversions in existing term calculi, where conversions are one of the fundamental problems in proof theory. This simplicity also means the abstraction of my approach that discards the inessential syntactic details. By formulating the computations for the three logics in this abstract level, the present work deepens the computational analyses of the logics.

Third Meeting: Zoom, 4 March 2022

Andrew Swan: Definable and non definable notions of structure
  • Start: 16:00 Amsterdam time
  • Recording of the talk available on YouTube
  • Join at Zoom Meeting ID: 832 9706 1847
  • Abstract Naïve category theory often makes implicit reference to sets, and thereby to a particular formulation of set theory. For example, we talk about the hom sets of locally small categories, small limits and colimits or the solution set condition of the adjoint functor theorem. Although almost all of homotopical algebra can be carried out in a purely algebraic way, we still see references to sets when we give explicit definitions of weak factorisation systems as cofibrantly generated by a set or small category of morphisms. We can break this dependence on sets using Grothendieck fibrations, where we replace the category of sets with a base category of our choice to serve as a foundation. The base category can be sets, but could also be a model of a particular choice of set theory or more generally an elementary topos, or even more generally a locally cartesian closed category or the category of small categories. If we have an external property of objects of the fibration that we are studying, it is natural to ask when we can talk about it in the internal language of our base. As a minimal condition we expect that such properties are stable under reindexing, but it turns out this is not strong enough. We can think of an object in the total category of a fibration intuitively as an "indexing object" I in the base together with a family of objects indexed by I, say (X_i)_I. What we need is a subobject of I in the base that tells us which objects X_i have the property we are interested in. This idea is captured remarkably well by Bénabou's notion of *definability*. For example, in many examples of Grothendieck fibrations the subterminal objects are stable under reindexing, but definability requires something more. An example where they are definable are codomain fibrations on Heyting categories: we can use the equality and universal quantifiers of the internal language to state what it means for any two elements of a type to be equal, which turns out to witness the definability of subterminal objects in the fibration.
    However, Bénabou's definition applies only to properties of objects and not to structure. For structure we can use a new definition introduced by Shulman under the name *locally representable*. I'll give a reformulation of Shulman's definition making it clear that it can be seen as a generalisation of Bénabou's in the same spirit, encompassing not just definability, but also Johnstone's earlier generalisation of comprehensivity. Just as we considered stability under reindexing as a minimal requirement for properties, we first consider *notions of fibred structure* or just *notions of structure* on a fibration. We think of this as a kind of structure which is defined externally to the fibration, but stable under reindexing. Reindexing stable classes are a special case, which we refer to as *full* notions of structure, but so are Johnstone's comprehension schemes and any time we have a (co)monad over a fibration, the category of (co)algebras is another example.
    I am particularly interested in the case of algebraic weak factorisation systems (awfs), which are notions of structure on codomain fibrations with the property of being monadic, and equipped with certain extra structure. I give a sufficient criterion for awfs's to be definable, as cofibrantly generated by a family of maps with tiny codomain. This uses a general definition of tiny in a fibration, that can be applied to codomain fibrations to obtain a result similar to that of Licata, Orton, Pitts and Spitters, or can be applied to set or category indexed families to obtain a different looking result referring to maps that are tiny in an external sense that can be phrased using hom set functors.
    I will also list some examples of non definable notions of structure based on Kan fibrations, which are widely used in homotopical algebra and can be defined in any topos with interval object. A large class of weak factorisation systems cannot be definable as full notions of structure unless the axiom of choice holds. In some interesting special cases the awfs of Kan fibrations can be shown to be non-locally representable using logical properties of the interval object, even in classical logic with the axiom of choice. In simplicial sets this can be done using the fact that the interval has a linear order (in a certain sense the interval object of simplicial sets is the "generic" linear order with endpoints) and can be done in BCH cubical sets using the fact that the interval has "separable diagonal."

Second Meeting: Zoom, 4 February 2022

Julia Ramos Gonzalez: Exponentiable Grothendieck abelian categories and algebraic geometry
  • Start: 16:00 Amsterdam time
  • Recording of the talk available on YouTube
  • Join at Zoom Meeting ID: 838 6419 3991
  • Abstract Grothendieck abelian categories can be seen, on one hand, as the Ab-enriched topoi, and on the other hand, as the (categorical counterpart of) noncommutative schemes. In particular, the 2-category Grt♭ of Grothendieck abelian categories with left exact left adjoint additive functors, which is nothing but the Ab-enriched counterpart of the 2-category of topoi and geometric morphisms, is a natural environment in order to study noncommutative flat algebraic geometry. In this talk we show that the Bird-Kelly tensor product of (enriched) locally presentable categories endows Grt♭ with a monoidal structure, which is a linear counterpart of the product of topoi and at the same time can be considered as a noncommutative parallel of the product of schemes with flat morphisms between them. Moreover, in an effort to shed some light on the exponentiability of schemes, we study the exponentiable objects in Grt♭. More concretely, we provide a characterization of the exponentiable objects in Grt♭ by following a linear parallel to Johnstone and Joyal’s characterization of exponentiable topoi.
    The content of this talk is joint work with Ivan Di Liberti.

Inaugural Meeting: Amsterdam, 27 October 2021

Program

  • 13:00-14:00: Niels van der Weide (Radboud University), The correspondence between LCCCs and dependent type theories from a univalent perspective (slides)
  • 14:30-15:00: Jaap van Oosten (Utrecht University), Games and Lawvere-Tierney topologies
  • 15:00-15:30: Daniël Otten (University Amsterdam), M-types and bisimulation (slides)
  • 16:00-17:00: Jesper Cockx (TU Delft), The Quest for Confluence (slides)
  • 17:30-23:59: Dinner

Registration

Registration is free of charge, but mandatory. Please register via this Google Form.

Location

The meeting is going to take place in the Science Park, Amsterdam, in Building 904, Room B0.209 (see the campus map).

Organizers

  • Benedikt Ahrens, B.P.Ahrens@tudelft.nl (TU Delft)
  • Benno van den Berg, bennovdberg@gmail.com (Universiteit van Amsterdam)