| CARVIEW |
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.- To subscribe, send an email to dutchcats+subscribe@googlegroups.com.
- To send a message to the list, use dutchcats@googlegroups.com. (Only emails from subscribers are accepted for distribution.)
DutchCATS meeting in Utrecht, 2 May 2025
Location
We meet in KBG - Atlas (see the campus map). Registration is free, and you can register here.Programme
arrival (13:00)
-
13:15-13:45 Daniël Otten, Matching (Co)patterns with Cyclic Proofs
Abstract: 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. -
13:45-14:15 Niels van der Weide, Impredicative Encodings of Inductive and Coinductive Types
Abstract: 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. - 14:15-14:45 break
-
14:45-15:15 Kobe Wullaert, Rezk completion for topoi
Abstract: 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. -
15:15-15:45 Dario Stein, Independence Structures and Dagger Categories of Relations
Abstract: 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. - 15:45-16:15 break
-
16:15-16:45 Makoto Fujiwara, On the separation techniques of weak logical principles over intuitionistic arithmetic
Abstract: 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. -
16:45-17:15 Pim Otte, Tutte's theorem as an educational formalization project
Abstract: 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. - 18:00: Dinner at Wagamama
DutchCATS meeting in Nijmegen, 7 February 2025
Location
We meet in Room HG00.303 in the Huygens building (see the campus map). Registration is free, and you can register here.Programme
arrival (13:30)
-
13:40-14:05 Nima Rasekh, From Mathematical Foundations to (Higher) Categories
Abstract: 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. -
14:05-14:30 Lukas Mulder, The Functorial Nature of Enriched Data Types
Abstract: 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. - 14:30-14:55 break
-
14:55-15:20 Tom de Jong, Ordinal Exponentiation in Homotopy Type Theory
Abstract: 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. -
15:20-15:45 Fernando Chu, Towards a fully functorial directed type theory
Abstract: 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. - 15:45-16:10 break
-
16:10-16:35 Márk Széles, Categories of partial probabilistic computations
Abstract: 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. -
16:35-17:00 Bálint Kocsis, Complete Test Suites for Automata in Monoidal Closed Categories
Abstract: 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. - 18:00: Dinner at De Hemel
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)
-
[13:00-13:40] Umberto Tarantino, Triposes and toposes through arrow algebras slides
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.
-
[13:40-14:20] Henning Basold, Simplicial and higher coalgebras
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.
break (20 min)
-
[14:40-15:20] Henning Urbat, Operational techniques for higher-order coalgebras slides
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.
break (20 min)
-
[15:40-16:20] Ruben Turkenburg, Proving behavioural apartness slides
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.
-
[16:20-17:00] Dario Stein, Two types of *do*: functional programming with interventions and counterfactuals slides
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.
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)
-
[13:30-14:15] Matteo Acclavio, Constructive modal logic: game semantics and lambda-calculi
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.
This talk is based on joint works with Davide Catta, Federico Olimpieri and Lutz Strassburger.
Proof equivalence: https://inria.hal.science/hal-03909538
Game semantics: https://link.springer.com/chapter/10.1007/978-3-030-86059-2_25
Lambda-calculus: https://link.springer.com/chapter/10.1007/978-3-031-43513-3_19 -
[14:15-15:00] Patrick Forré, Quasi-measurable spaces - A convenient foundation of probability theory slides
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.
This talk is based on the following references:
- 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.
- P. Forré. "Quasi-Measurable Spaces". Preprint, arXiv:2109.11631, 2021.
break (30 min)
-
[15:30-16:15] Chase Ford, Monads on categories of relational structures slides
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.
-
[16:15-17:00] Lingyuan Ye, Stack representation of first-order intuitionistic theories
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.
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)
-
[13:00-13:30] Anna Schenfisch, Algebraic K-Theory of Persistence Modules, slides
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.
-
[13:30-14:00] Lingyuan Ye, Categorical Structures in Theory of Arithmetic, slides
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.
break (30 min)
-
[14:30-15:00] Jan Heemstra, Hardware Accelerated Intelligent Theorem Proving, slides
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.
-
[15:00-15:30] Wouter Fransen, Grothendieck Topologies on the Category of Finite Probability Spaces
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?
break (30 min)
-
[16:00-17:00] [Replacement programme] Jim Portegies, Workshop on Models for Synthetic Calculus, hand-out
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.
-
Valentina Castiglioni, On the Axiomatisation of Weak Bisimulation-based Congruences over CCS(canceled)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.
-
Bálint Kocsis, Normalization for simply typed lambda-calculus(canceled)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.
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
-
13:00-13:30 Dario Stein, New Topics in Markov Categories, slides
Abstract: I will discuss some new insights in categorical probability, such as copartiality, convex analysis and a sheaves of random variables -
13:30-14:00 Pedro Nora, Maximally permissive notions of bisimulation
Abstract: 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. - 14:00-14:30 Coffee break
-
14:30-15:00 Nima Rasekh, Univalent Double Categories, slides
Abstract: 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. -
15:00-15:30 Kobe Wullaert, Rezk Completions in Formal Category Theory, slides
Abstract: TBA - 15:30-16:00 Coffee break
-
16:00-16:30 Jelle Wemmenhove, slides
Abstract: 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. -
16:30-17:00 Arnoud van der Leer, slides
Abstract: 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. - 18:00: Dinner at De Hemel
DutchCATS meeting in Delft, 6 September 2023
Location
We meet in the Snijderzaal (building 36), Mekelweg 4, 2628 CD Delft.Programme
- 14:00 - 15:00 Fabian Zickgraf
- 15:00 - 15:30 Benno van den Berg
- 15:30 - 16:00 Break
- 16:00 - 16:30 Daniel Otten
- 16:30 - 17:00 Andreas Nuyts
- 17:00 - 17:30 Luc Chabassier
- 18:30 Dinner at Delfts Brouwhuis at Hippolytusbuurt 43, 2611 HM Delft (Google Maps)
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).-
11:00-12:00 Daniel Otten, Models for propositional type theory slides
Abstract: 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. - Lunch
-
13:30-14:30 Theo Winterhalter, A conservative and constructive translation from extensional type theory to weak type theory slides
Abstract: 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’splea for weaker frameworks since the translation in particular shows that ETT (and thus intensional type theory) is conservative over WTT. - Coffee break
-
15:00-16:00 Sam Speight, Higher-Dimensional Realizability for Intensional Type Theory slides
Abstract: 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". - Coffee Break
-
16:30-17:30 Discussion
- 18:30 Conference dinner at A Beautiful Mess
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)