Spring 2026

This talk has two loosely connected parts centered around the formalization of category theory in Lean.

In the first part, I will give a brief overview of how category theory is implemented in mathlib. Beyond serving as an introduction, this will illustrate some general design principles behind Lean libraries, as well as common challenges that arise when formalizing categorical mathematics. In particular, these challenges provide concrete examples of the kinds of issues that univalence is designed to address, but which are not directly available in Lean.

In the second part, I will discuss my current work on formalizing the bi-Yoneda lemma in Lean. This serves as a case study in formalizing higher-categorical ideas within the constraints of the existing type theory and library infrastructure. I will highlight both the technical approach and some of the conceptual obstacles that arise along the way. The code for my formalization can be found at https://github.com/SpencerWoolfson/biyoneda.

The aim of this talk is to express the fully algebraic theory of monoidal bicategories as developed in the 1990's by Kapranov-Voevodsky, Baez-Neuchl, Day-Street and many others in the homotopical language of higher algebra as developed in the 2010's by Lurie. Therefore, we show that the theory of E_n-operads, which originates from May's geometric classification of n-fold loop spaces, provides a convenient and meaningful way to handle concepts in both areas. In particular, we prove that braided, sylleptic and symmetric monoidal bicategories, in the sense of Day and Street, are exactly the E_n-monoidal bicategories, for n = 2, 3, 4, respectively, in the sense of Lurie. This implies that the theories of braided, sylleptic and symmetric monoidal bicategories can be captured by the practice of higher dimensional universal algebra. As an application, we state a bicategorical generalization of the well-known fact that monoids in a (symmetric) braided monoidal category form a (braided, and in fact symmetric) monoidal category, and give a conceptual proof thereof that requires virtually no computational effort.

This talk presents a conceptual path from classical Stone duality to its extension in the setting of stably compact spaces and the Multilingual Sequent Calculus (MLS).

We begin with the classical case of Stone duality for Boolean algebras, emphasizing the correspondence between algebraic and topological structures. We then move to the setting of stably compact spaces, where a similar duality persists but requires a refinement of the logical framework. In this context, MLS is introduced as a sequent calculus capable of relating propositions across different logical systems, providing a proof-theoretic counterpart to domain-theoretic constructions.

Building on this perspective, we present MLS explicitly as a sequent calculus and explain how its structure reflects the duality between logic and topology. We then introduce William Lawvere’s insight that quantifiers can be understood as adjoints to substitution, first in the classical setting of Boolean algebras. Finally, we explore how this adjoint perspective suggests a possible extension of MLS to the first-order level, highlighting both the conceptual challenges and the expected structural features of such an extension.

Foundational investigations into quantum theory have long shown that local, or non contextual value assignment to the mathematical representatives of physical quantities is problematic in quantum theory. These results relied on the study of mathematical structures suitable to represent the quantum observables (such as orthomodular lattices or partial Boolean algebras), either in a lattice-theoretic or an algebraic framework. A short lived research program in quantum foundations ("modal interpretations"), emerging from quantum logic in the 1980-1990s, showed how to avoid said results by defining and studying "quasiBoolean lattices", or equivalently on "quasiCommutative algebras". These structures allow non-contextual value assignments to its elements, as well as the embedding of quantum statistics into a classical probability space. I will present such works, before showing how modern no-go theorems in quantum foundations (extended Wigner's friend scenarios) can be derived in this formalism, thereby relating them to the older no hidden-variables theorems.

Categorification of a mathematical structure often reveals a common abstraction connecting previously studied but seemingly unrelated structures. In the case of de Paiva’s Dialectica categories, specializing the categorification of Gödel’s Dialectica construction to partial orders produces functorial embeddings of Heyting algebras into residuated lattices that appear to have been overlooked. We review Gödel’s original construction and de Paiva’s generalization, then examine the specialization to partial orders and share some insights it provides on the propositional logics associated to Dialectica categories proof-theoretically. Special attention is paid to the Dialectica construction on the two-element Boolean algebra, which is shown to have a surprising connection to the Dialectica construction on the large category Set. 

Multiplicative linear logic, the fragment of linear logic with only the multiplicative connectives, has the finite model property and its entailment is known to be NP-complete. As free algebras for the multiplicative linear logic are infinite and not well understood in general, it seems reasonable to study the structural theory of finite algebraic models of this logic, namely because they encompass all the counterexamples to invalid sequents. Algebraic models of multiplicative linear logic MML are partially ordered algebras - involutive partially ordered monoids - where the partial order is generated by its sequent calculus, the multiplication is associative and order-preserving, and the linear negations form an involutive pair. Cyclic involutive partially ordered monoids are therefore algebraic models of cyclic multiplicative linear logic CyMLL, and the commutative ones are algebras for multiplicative fragment of relevant logic RW. In this project, we aim at structural understanding of certain classes of involutive partially ordered monoids.

Because lattice connectives are not present in the signature, the underlying poset of an ipo-monoid does not always form a (semi)-lattice, and some interesting posets, including in particular certain unions of chains, arise this way. In general, the underlying poset is a disjoint union of directed connected components, indexed by elements of a group, with the monoid unit contained in the component indexed by the group unit. This can be observed from (i) every connected component is up-directed and down-directed, hence in finite ipo-monoids every connected component is bounded, (ii) the equivalence relation that has each connected component as an equivalence class is a congruence, and the quotient algebra is a group.

We aim at understanding such algebras as Płonka sums, in particular using techniques described in [1]. Therefore we wish to understand how certain important properties of the algebra arise, in particular in which cases it is balanced (x\x = x/x), cyclic, or commutative. Assuming A is an ipo-monoid with 0≤1 and every element of A has a finite order, we can see the following: in case A is conic with no elements between 0 and 1, there is an order-embedding from each connected component to the unital component, limiting the size of the components in case the algebra is finite, and imposing further structure on A, depending on the unital component. For example, the unital component is (i) idempotent if and only if A satisfies periodic n-contraction equation x^{n+1} = x for sime n (for n = |G| in the finite case), (ii) if the unital component is idempotent, then it is cyclic if and only if A is balanced (iii) if the unital component is cyclic, then it is a commutative subalgebra of A, isomorphic to a Sugihara monoid. If moreover the whole algebra A is finite, then it is also cyclic.

We in particular describe involutive partially ordered monoids with Sugihara monoids as their unital component. Using Płonka sums described in [1] to show these algebras can be constructed from groups with the antichain order and involutive partially ordered monoids that are disjoint unions of one-element and two-element chains. This result closely relates to work on unilinear residuated lattices [2]. 

Some of the results were discovered with the help of Prover9/Mace4.

[1] S. Bonzio, J. Gil-Férez, P. Jipsen, A. Přenosil, M. Sugimoto: On the structure of balanced residuated partially ordered monoids, RAMiCS (2024).

[2] X. Zhuang: Unilinear residuated lattices, PhD thesis (2023).

Circulant matrices play an important role in algebra, graph theory, and many other areas. A classical result due to Glaisher (1879) states that any circulant determinant of order 2n can be expressed as the product of two circulants of order n, constructed in a precise way. We revisit this theorem by showing that any circulant of order 4 can be written in three different ways as a difference of special squares, and that any circulant determinant of order 8 can be written in seven different ways as a difference of squares. We also explain how this latter case is related to the Fano plane and why eight is special among all powers of 2. Finally, we show that all of this is connected to Pfister’s modern theory of quadratic forms.

If E is a real inner product space (a real vector space equipped with a bilinear, positive definite scalar product) and u is a vector in E of norm ≤ 1, the projection operator from E onto the orthogonal complement of u can be computed using an iterative construction that bears a strong resemblance to a construction in category theory called the "small object argument" for weak factorization systems.

If C is a category with all colimits and f is a suitably "small" morphism in C, the small object argument is an iterative construction that, starting with any morphism in C, results in a morphism that is in an "orthogonal complement" of f.

The goal of this talk is to show that this analogy with vector spaces can be extended quite far. For any cocomplete category C, its arrow category Arr(C) has the structure of an Arr(Set)-module, where Arr(Set) is the arrow category of the category of sets, equipped with the symmetric monoidal tensor product known as the "pushout-product". By adjointness, this module structure on Arr(C) equips Arr(C) with an enrichment over Arr(Set) that is the analogue of an inner product for a vector space. This enrichment can be used to define various notions of orthogonality between morphisms of C. From this point of view, the small object argument can be seen as an iterative construction that computes a suitable projection operator.

This perspective extends to enriched categories, where Set can be replaced by any locally presentable, closed symmetric monoidal category V. Moreover, this perspective on orthogonality extends to (enriched) ∞-categories.

The Płonka sum is a construction introduced in Universal Algebra in the 1960s by the eponymous Polish mathematician to obtain new algebras out of a semilattice direct system of similar (disjoint) algebras. This construction is particularly useful in characterizing the structure of the members of the regularization of a strongly irregular variety. In this talk, after a brief introduction to the general theory of Płonka sums, we discuss some structural and algebraic properties of Płonka sums and regularized varieties. In particular, we examine the nature of splitting pairs of the lattice of subvarieties of a regularized variety, the congruence lattices of a Płonka sum, and the preservation of epimorphism surjectivity. This is joint work with Stefano Bonzio (U. Cagliari).

The talk is based on the following paper: https://arxiv.org/html/2602.06188v1.

Traditionally, Stone duality is thought of as a certain type of dual equivalence of concrete categories in which the arrows are structure preserving functions. In previous work, we showed that Stone duality for structure preserving relations (as opposed to structure preserving functions) needs the richer framework of order-enriched category theory. In this talk, we will argue that Stone duality for relations finds its proper home in double categories that can accommodate both functions and relations. 

This talk explores a modal extension of a three-valued paraconsistent logic of the LFI family, aiming to model epistemic and doxastic attitudes under inconsistency. By combining modal operators with a trivalent semantics, the proposed framework allows for a natural distinction among different epistemic states that are often conflated in classical settings.  

In particular, the interaction between modality and paraconsistency makes it possible to distinguish three epistemic levels associated with belief and knowledge, reflecting different strengths of epistemic commitment in the presence of contradictory but non-trivial information. These distinctions are not imposed extralogically, but instead emerge from the underlying logical structure of the system.

From a foundational perspective, the framework contributes to a resilient epistemology, in which agents can acknowledge contradictions without epistemic collapse, while preserving controlled reasoning and revisability.

Finally, the talk briefly discusses motivations from artificial intelligence and the misalignment problem, where rational agents must operate under incomplete, evolving, and sometimes incoherent information. The proposed logical setting offers tools for representing graded epistemic attitudes compatible with cautious and robust reasoning in such environments.