Itaca Fest 2025

ItaCa Fest is an online webinar aimed to gather the community of ItaCa.

The seminar will be live on Zoom at this link. The time is: 3pm Italian time.

Here the list of seminars

• April 15, 2025
• May 20, 2025
• June 17, 2025
• September 23, 2025
• October 21, 2025
• November 18, 2025

April 15, 2025

Zurab Janelidze

Relational Duality for Barr Exact Mal'tsev Categories

As we now know, a powerful self-dual approach to semi-abelian categories is given by isolating the fibration of subobjects as a primitive. This leads to the concept of a noetherian form, which, apart from semi-abelian categories also includes Grandis exact categories in its scope. Is there a similar approach to Barr exact Mal'tsev categories? In the talk, which is based on an on-going joint work with D. Rodelo, we present an idea that could lead to a positive answer to this question. Unlike the axioms of a semi-abelian category, it does not seem to be possible to capture axioms of a Barr exact Mal'tsev category as self-dual properties of the fibration of subobjects. What we propose in this paper is to replace this structure with a richer structure of a relation calculus (to be defined in the talk), which will be required to possess certain self-dual properties of a tabular allegory.

Nelson Martins-Ferreira

Categorical Analysis of MATLAB and Octave Programming Functions

In this talk, we introduce a category that models programming languages with complex-valued matrices as default variables, focusing on MATLAB and Octave. We demonstrate how indexation in these languages corresponds to function composition and analyze the categorical behavior of built-in functions such as unique, ismember, sortrows, and sparse.

We then explore a procedure to transform arbitrary graphs, represented as pairs of complex-valued matrices in MATLAB and Octave, into an indexed structure with a surjective index for the domain matrix. Finally, we discuss the implementation of a programming function exhibiting categorical behavior akin to a coequalizer. This work is motivated by some ideas and results from [1,2].

[1] N. Martins-Ferreira, Internal Categorical Structures and Their Applications, Mathematics (2023) 11(3), 660; https://doi.org/10.3390/math11030660

[2] N. Martins-Ferreira, On the Structure of an Internal Groupoid, Applied Categorical Structures (2023) 31:39 https://doi.org/10.1007/s10485-023-09740-1

Xabier García Martínez

A universal Kaluzhnin-Krasner embedding theorem

Given two groups A and B, the Kaluzhnin--Krasner universal embedding theorem states that the wreath product A ≀ B acts as a universal receptacle for extensions from A to B. For a split extension, this embedding is compatible with the canonical splitting of the wreath product, which is further universal in a precise sense. This result was recently extended to Lie algebras and cocommutative Hopf algebras.

In this talk we will explore the feasibility of adapting the theorem to other types of algebraic structures. By explaining the underlying unity of the three known cases, our analysis gives necessary and sufficient conditions for this to happen.

We will also see that the theorem cannot be adapted to a wide range of categories, such as loops, associative algebras, commutative algebras or Jordan algebras. Working over an infinite field, we may prove that amongst non-associative algebras, only Lie algebras admit a Kaluzhnin--Krasner theorem.

Joint work with Bo Shan Deval and Tim Van der Linden

May 20, 2025

Peter Lumsdaine

Organising syntax in arithmetic universes

“Arithmetic Universes” — aka list-arithmetic pretoposes — were proposed by Joyal as a categorial setting for syntax, and developed into their current form by (among others) Maietti and Vickers. But what does it mean that they give a setting for syntax?

One good answer is that they should host free models of finitely presented essentially algebraic theories. The essential techniques for this are well established, but a thorough general treatment are elusive — not perhaps because it is difficult, but because a head-on approach, carried through carefully, is gruellingly bureaucratic.

What helps is a good organising framework. One such is provided by schemes of inductive types from type theory — in particular, indexed-inductive and (quotient) inductive-inductive types — and established techniques for reducing very general such schemes to a few primitives. I will show how these techniques can be applied in arithmetic universes, with a little care to handle finitariness, to build up from basic primitives to schemes that provide free models of essentially algebraic theories.

Sanjiv Ranchod

Substitution for Linear-Cartesian and Full Substructural Theories

The characterisation of cartesian (or, algebraic) theories as monoids for a substitution monoidal structure [1] has also been considered in the substructural settings of linear theories [2] and affine theories [3].

In this talk, we revisit these constructions, recasting them as arising from free symmetric monoidal theories. With this new perspective, we generalise to two settings of interest: Firstly, the linear-cartesian setting, which combines linear and cartesian structures together with a substructural coercion between them. Secondly, to a full substructural setting, which encompasses linear, affine, relevant and cartesian structures with coercions.

Following this, we exhibit various free-forgetful adjunctions between these theories, notably between Lawvere theories, symmetric operads and linear-cartesian theories. We conclude with comments on the bicategories associated with substitution monoidal structures, on applying this construction to other theories and on models for single-variable substitution in these settings.

Joint work with Marcelo Fiore.

[1] M. Fiore, G. Plotkin and D. Turi, Abstract syntax and variable binding (extended abstract), 14th Symposium on Logic in Computer Science (1999), 193–202.
[2] G.M. Kelly, On the operads of J.P. May, Reprints in Theory and Applications of Categories (2005), no. 13, 1–13.
[3] M. Tanaka and J. Power, A unified category-theoretic semantics for binding signatures in substructural logics, J. Logic Comput. (2006), vol. 16, no. 1, 5–25.

Pablo Donato

The Flower Calculus

We introduce the flower calculus, a diagrammatic proof system for intuitionistic first-order logic inspired by Peirce's existential graphs. It works as a rewriting system on syntactic objects called "flowers", that enjoy both a graphical presentation as topological diagrams, and an inductive characterization as nested geometric sequents in normal form. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an invertible and analytic fragment with respect to Kripke semantics. We also showcase the intended application of this calculus to the design of graphical user interfaces for interactive theorem proving.

June 17, 2025

Urs Schreiber

TBA

Vova Sosnilo

TBA

Francesca Pratali

TBA

September 23, 2025

Benjamin Merlin Bumpus

TBA

Ruben Van Belle

TBA

TBA

TBA

October 21, 2025

TBA

TBA

Soichiro Fujii

TBA

Nathanael Arkor

TBA

November 18, 2025

Paul Taylor

TBA

Umberto Tarantino

TBA

TBA

TBA