I am a PhD student working on categorical logic and homotopy type theory at the School of Mathematics of the University of Leeds (UK), supervised by Nicola Gambino, Federico Olimpieri, and Michael Rathjen. Prior to that, I studied pure mathematics at the University of Trento (IT) and at Utrecht University (NL), supervised by Stefano Baratella and Jaap van Oosten.

In categorical logic I am interested in the notion(s) of (hyper)doctrines and Grothendieck fibrations to phrase the semantics of (fragments of many-sorted) first-order logic, focusing on quantifier completions, the dialectica construction, and canonicity properties. Regarding homotopy type theory, I have been focusing on propositional (a.k.a. weak, objective, axiomatic) theories, where computation rules are all explicit, essentially via categorical semantics methods, in order to study property-like, completeness, coherence, and conservativity properties.

Click here for a curriculum vitae and here for a research statement.

Ongoing research.

• Type constructors as algebras.
• Torsion theories and dependent types. Together with Federico Campanini.
• Coherence for path categories. Together with Daniël Otten and Benno van den Berg. YouTube presentation here.

Publications and preprints (arXiv versions here)

• [Preprint] A conservativity result for homotopy elementary types in dependent type theory [2303.05623v1]. March 2023.
• [Journal paper] Dialectica principles via Gödel doctrines [2205.07093v1]. Theoretical Computer Science. May 2022. Together with Davide Trotta and Valeria de Paiva.
• [Refereed conference paper] Dialectica logical principles [2109.08064v1]. Proceedings of Logical Foundations of Computer Science 2022. September 2021. Extended version → [Journal paper] Dialectica logical principles: not only rules. Journal of Logic and Computation (LFCS 2022 post-conference volume). March 2022. Together with Davide Trotta and Valeria de Paiva.
• [Refereed conference paper] The Gödel fibration. Proceedings of Mathematical Foundations of Computer Science 2021. August 2021. Extended version → [Preprint] The Gödel fibration [2104.14021v1]. April 2021. Together with Davide Trotta and Valeria de Paiva.
• [Preprint] Quantifier completions, choice principles and applications [2010.09111v3]. Submitted. October 2020. Together with Davide Trotta.

Talks in conferences and workshops + some talks in seminars

• Coherence in the semantics of dependent types. Leeds Postgraduate Logic Seminar. Leeds, June 2023.
• Coherence for Extensional, Intensional and Propositional Identities. Category Theory Lunch. Leeds & Manchester, June 2023.
• What is a dependent type theory? Leeds Maths PGR Conference 2023. Leeds, June 2023.
• Strictifying Path Categories. Workshop on Doctrines & Fibrations. YouTube Recording. Slides. Padua, June 2023.
• Propositional dependent type theories: a conservativity result for homotopy elementary types. Homotopy Type Theory 2023. Slides. Pittsburgh, May 2023.
• Weak type theories: a conservativity result for homotopy elementary types. DutchCATS. Amsterdam, May 2023.
• A conservativity-like result for a propositional type theory. 3rd ItaCa Workshop. YouTube Recording. Pisa, December 2022.
• Dialectica: fibrations and logical principles. Applied Category Theory 2022. YouTube Recording. Slides. Glasgow, July 2022.
• Propositional in Dependent Type Theory. Leeds Maths PGR Conference 2022. Leeds, June 2022.
• Towards the notion of Propositional Dependent Sum Types. Proofs, Constructions, Computations and Categories. Leeds, February 2022.
• Dialectica completion & dialectica logical principles. 26th Yorkshire and Midlands Category Theory Seminar. Slides. Birmingham, January 2022.
• Dialectica completion & Gödel fibrations. 2nd ItaCa Workshop. Genoa, December 2021.
• Dialectica logical principles. Eighth Symposium on Compositional Structures. Tallinn, December 2021.
• On the notions of exact completion. Leeds Postgraduate Logic Seminar. Leeds, November 2021.
• Existential, universal and dialectica completion. Proofs, Constructions, Computations and Categories. Leeds, November 2021.
• Regular (first-order) logic symbols & doctrines. Groningen Mathematics PhD Seminar. Groningen, October 2021.
• The Gödel Fibration. Applied Category Theory 2021. Poster. Cambridge, July 2021.
• Quantifier completions of doctrines. Categories and Companions Symposium 2021. YouTube Recording. Sydney, June 2021.

Visiting activities

• ILLC, Amsterdam, the Netherlands. Host Benno van den Berg. April-May 2023.
• University of Padua, Italy. Host Maria Emilia Maietti. December 2022.

Some links

• Leeds SoM account
• Google Scholar account
• ResearchGate account
• ORCID
• Mathematics Stack Exchange account

Other stuff

• An introduction to doctrines
• An introduction to TQFT
• Master’s thesis
• Some sciarade (charades)
• Curriculum vitæ
• Research statement

A portrait of me and my collaborator working together.