Francesco Dagnino (Università degli Studi di Genova) will give a talk on
Comprehensions-Quotients Duality, relationally
Abstract:
The calculus of relations is a longstanding variable-free alternative to first-order logic, where the primitive concepts are (binary) relations instead of (unary) predicates.
A natural question thus arises: how do we recover unary predicates in such a relational setting?
A standard approach is to see them as coreflexive relations, that is, relations included in the identity. These behave very well mainly because one can show that coreflexive relations are also symmetric and interpolative, thus actually coequivalence relations. This proof crucially relies on the modularity law which, however, is not available in more general relational contexts such as metric relations used in quantitative reasoning.
In this talk, we explore the possibility of representing predicates directly as coequivalence relations using the language of relational doctrines, which provide a functorial description, in the spirit of Lawvere’s hyperdoctrines, of the core fragment of the calculus of relations.
Specifically, we introduce comprehensions of coequivalence relations together with an associated comprehension completion.
By leveraging a duality for relational doctrines, we recognize comprehensions as the dual of quotients, thus deriving that the comprehension completion is a lax idempotent 2-monad whose algebras are precisely relational doctrines with comprehensions.
Finally, we discuss the interaction between quotients and comprehensions, showing that, while the associated 2-monads do not compose in general, they do so when the relational doctrine has well-behaved conjunctions or disjunctions.