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".
Formalizing Games with Explicit Strategies
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.
|
Converse extensionality and apartness
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.
|
Partition functor for effect algebras: a model of quantum measurements
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.
|
1-truncated Universal Algebra in HoTT
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.
|
A topos embedding of continuous logic
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.
|
Completeness Theorems for First-Order Logic Analyzed in Constructive Type Theory
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".