Categories and Types Seminar (CATS)
This is the website of the Categories and Types Seminar at the Institute for Logic, Language and Computation (ILLC) of the University of Amsterdam. The idea behind the seminar is that the talks will be given by and for master and PhD students interested in category and type theory, and in that way to provide a forum and meeting place for students interested in these topics.
The seminar is held online via Zoom. To receive the Zoom link, please subscribe to the CATS seminar mailing list by sending an email to Anton at agolov[at]science.ru.nl with the subject "CATS seminar".
| Speaker | Martin Karlsson |
|---|---|
| Date | Thursday January 7 at 17:00 - 18:00 |
| Abstract | We define two-player perfect information games characterizing classical and intuitionistic first-order validity. In short we enrich the language of first-order logic with two force markers denoting assertion and challenge. A two-player game is then a tree of states representing each players assertions and challenges and whose turn it is to move. A winning strategy for a player is a subtree of a game fulfilling some conditions. In particular we examine one of the players (the proponents) winning strategies for which we define several operations such as parallel, contraction, application, and composition. Using these operations we then establish a correspondence of strategies with derivations in the sequent calculus. The constructive treatment of strategies gives them a computational interpretation. The techniques developed may also be of use for many similar game-semantics. To bring this to bear we seek to formalize the semantics in cubical Agda. |
| Speaker | Robert Passmann |
|---|---|
| Date | Thursday December 10 at 17:00 - 18:00 |
| Abstract | In an appendix to Troelstra's 344, Howard studies certain converse extensionality principles (CE_n) as the Dialectica interpretation of extensionality. He shows that there are model’s of Gödel’s T that does not have a witness for CE_0, and that there are models of Zermelo-Fraenkel set theory (without choice) in which CE_1 is false. Despite these negative results, we show that there is a computational interpretation of CE_0 and CE_1. Moreover, we show that CE_0 and CE_1 do not imply Markov's principle. This is joint work with Benno van den Berg. |
| Speaker | Leo Lobski |
|---|---|
| Date | Thursday November 26 at 18:00 - 19:00 |
| Abstract | One of the most striking features of quantum mechanics is its notion of a measurement: in general, an individual measurement of a system gives information about a proper subset of all the physical properties that could be observed in theory (and not of the entire system). In this way, epistemology (that which can be observed by measuring) gets decoupled from ontology (the whole system that is supposedly out there). A natural question then arises: are all the measurements collectively sufficient (in theory) to fully determine the whole system? In order to maintain an objective notion of the physical reality, one would hope the answer to this question to be affirmative. In this talk, I will formulate this question as (conjectured) essential injectivity of the 'partitions of unity functor' from the category of effect algebras to the category of posets. After this, setting aside the physical motivation, I will provide mathematical evidence towards the truth of the conjecture by discussing two special cases in which the conjecture is known to be true: Boolean algebras and finite MV-algebras. The talk is based on my MSc thesis. |
| Speaker | Niels van der Weide |
|---|---|
| Date | Thursday November 12 at 17:00 - 18:00 |
| Abstract | Universal algebra is the study of algebraic structures such as monoids and groups. In the context of homotopy type theory (HoTT), such structures are implemented using types which are sets (i.e. types in which all proofs of identity are equal). However, types do not have to be sets in HoTT, so we would like to extend this study to a more general case. As a step towards that goal, we look at universal algebra for 1-types (types of which each identity type is a set). The main goal of this talk is to show the existence of free algebras, and in particular, the existence of a certain class of higher inductive types. |
| Speaker | Daniel Figueroa |
|---|---|
| Date | Thursday October 29 at 16:00 - 17:00 |
| Abstract | Continuous logic is a modification of first-order logic with ‘continuous’ versions of structures and predicates, and is especially suited for the analysis of metric structures. Although it has become an established topic in the past decade, it has not been examined deeply from the point of categorical logic. In this talk, I will present some new results in this direction. I will introduce the notions of hyperdoctrines, categories of metric spaces and categories of partial equivalence relations and show a surprising connection that exists between these concepts. This connection leads to a natural notion of ordering of predicates in continuous logic, which will allow us to relate interpretations in continuous logic to familiar interpretation of objects and subobjects in a category. We also obtain a version of soundness for continuous logic. I explain how to extend this relation to subobjects in a topos, and give some implications of these results for continuous logic and suggestions for possible future work. |
| Speaker | Dominik Wehr |
|---|---|
| Date | Thursday October 15 at 16:00 - 17:00 |
| Abstract | We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanized in the Coq proof assistant. As completeness with respect to standard model-theoretic semantics is not readily constructive, we analyze the assumptions necessary for particular syntax fragments and discuss non-standard semantics admitting assumption-free completeness. For this, we make use of synthetic computability theory which works in terms of the notion of computation embodied by the ambient type theory. |
The seminar is currently organized by Benno van den Berg, Anton Golov, and Taichi Uemura. If you're interested in giving a talk at the seminar or have any questions regarding the seminar please contact Benno at B.vandenBerg3[at]uva.nl.
To receive further announcements, please subscribe to the CATS seminar mailing list by sending an email to Anton at agolov[at]science.ru.nl with the subject "CATS seminar". In case you no longer wish to subscribe to the mailing list send an email to Anton with the subject "CATS seminar unsubscribe".