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 | Jetze Zoethout |
|---|---|
| Date | Tuesday May 25 at 16:00 |
| Abstract | The Effective Topos, introduced by Martin Hyland, is a topos where the internal logic is governed by recursive function application. For example, first-order arithmetic coincides with Kleene realizability, and the endofunctions on the NNO are precisely the total recursive functions. Similar toposes may be constructed on the basis of other notions of computability. Such notions of computability are formalized as partial combinatory algebras, and each such a partial combinatory algebra gives rise to a corresponding realizability topos. In this talk, we will explore how constructions in category theory correspond to constructions in computability theory, and vice versa. In one direction, we will see how slicing of categories can be reconstructed at the level of partial combinatory algebras. In the other direction, we will explain how computability relative to an oracle can be analyzed using category theory. |
| Speaker | Norihiro Yamada |
|---|---|
| Date | Tuesday May 11 at 16:00 |
| Abstract | Game semantics is a particular class of mathematical semantics of logic and computation, which interprets types and terms by games and strategies, respectively. By its distinctive intensionality, it has been a highly powerful tool for the study of type theories, and recently extended to a mathematical foundation of intensional aspects of logic and computation such as normalisation, algorithms and higher-order computability. One of the most challenging problems in game semantics is to interpret dependent types. In fact, there has been no established solution for this problem for more than 25 years. Another, related problem is that existing game semantics does not have all finite limits. In this talk, I sketch my game semantics of dependent types and show that it has all finite limits. Rather than the technical details, I focus on: 1. Why game semantics is useful for category theory and type theory; 2. Why game semantics of dependent types is difficult; 3. Main idea for the solution; 4. Ongoing and future work. |
| Speaker | Théo Winterhalter |
|---|---|
| Date | Thursday April 29 at 17:00 |
| Abstract | In this talk I will present joint work with Simon Boulier regarding a notion of dependent type theory which we called *weak type theory*, where conversion is completely removed. Instead computation rules like beta-reduction are explicit equalities (as in, inhabitants of an equality/identity type). This type theory echoes De Bruijn’s *plea for weaker frameworks* by having proof as self-evident objects as they do not require potentially enormous computing power to be checked. Nevertheless, we argue that this theory is still as (logically) powerful as its intentional counterpart (*i.e. *with regular conversion) and even as its extensional counterpart (with reflection of equality). We do so by means of a program translation from extensional type theory to weak type theory. |
| Speaker | Rafael Bocquet |
|---|---|
| Date | Tuesday April 13 at 16:00 |
| Abstract | Hofmann's conservativity theorem states that Extensional Type Theory is a conservative extension of Intensional Type Theory: when working internally to Intensional Type Theory, it is possible to pretend that every internal equality holds strictly. This relies on the presence of the Uniqueness of Identity Proofs (UIP) principle in Intensional Type Theory. We would like to establish generalizations of this conservativity theorem to type theories without UIP, such as variants of Homotopy Type Theory. In this talk I will show how to reduce the conservativity of extensions of type theories by additional strict equalities to acyclicity conditions, which I believe to be provable by normalization. This reduction is similar to the equivalence of different statements of Mac Lane's coherence theorem for monoidal categories. The main new tool is a type-theoretic definition of higher models of type theory. A preprint is available on the arXiv: https://arxiv.org/abs/2010.14166 |
| Speaker | Henrik Forssell |
|---|---|
| Date | Tuesday March 30 at 16:00 |
| Abstract | The standard completeness theorems for classical and intuitionistic first-order logic famously fail in a constructive metatheory: classical first-order logic can not be shown to be complete with respect to Tarski models, and intuitionistic logic can not be shown to be complete with respect to Kripke models. Certain weaker fragments, however, can be shown to be complete, and that without restrictions such as enumerability of theories or even decidability of equality for non-logical symbols. We explore a construction for proving this for regular logic and point out some related connections between reflectivity principles for models of regular theories and choice principles in the ambient set theory. We then show how we can use the completeness for regular logic to obtain Kripke and Beth “style” completeness results for first-order logic. This is joint work with Christian Espìndola and Peter L. Lumsdaine. |
| Speaker | Tom de Jong |
|---|---|
| Date | Tuesday March 16 at 16:00 |
| Abstract | Univalent Foundations (UF), also known as Homotopy Type Theory (HoTT) serves a foundation for constructive mathematics and is implemented in proof assistants such as Agda. UF extends intensional Martin-Löf Type Theory with Voevodsky's univalence axiom. Other axioms that one may wish to assume are Voevodsky's resizing axioms, which are said to make the type theory impredicative. If we don't assume such axioms, then we speak of predicative UF. In this talk we explore some limits of predicative UF. Crudely formulated, we show that various posets, such as sup-lattices, can only be small in impredicative UF, unless they are trivial. In stating this result precisely and in proving them, we are led to study nontriviality and its constructively stronger counterpart positivity, as well as a theory of size. As a byproduct, we also get that various nontrivial posets, including sup-lattices, cannot have decidable equality unless (weak) excluded middle holds. Finally, if time permits, we comment on the role of univalence in our results. This is joint work with Martín Escardó. |
| Speaker | Sina Hazratpour |
|---|---|
| Date | Tuesday March 9 at 16:00 |
| Abstract | Every topos has an internal higher-order intuitionistic logic. The so-called Kripke–Joyal semantics of a topos gives an interpretation to formulas written in this language used to express ordinary mathematics in that topos. The Kripke–Joyal semantics is in fact a higher order generalization of the well-known Kripke semantic for intuitionistic propositional logic. In this talk I shall report on joint work with Steve Awodey and Nicola Gambino on extending the Kripke–Joyal semantics to dependent type theories. If time permits, I shall discuss the extension of our semantics to homotopy type theory. |
| 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".