arXiv subjects

Chiara Sarti

Publications and source records attributed to Chiara Sarti.

6 recordsLinked to original sources

arXiv2025

Beyond Eckmann-Hilton: Commutativity in Higher Categories

We show that in a weak globular $ω$-category, all composition operations are equivalent and commutative for cells with sufficiently degenerate boundary, which can be considered a higher-dimensional generalisation of the Eckmann-Hilton argument. Our results are formulated constructively in a type-theoretic presentation of $ω$-categories. The heart of our construction is a family of padding and repadding techniques, which gives an equivalence relation between cells which are not necessarily parallel. Our work has been implemented, allowing us to explicitly compute suitable witnesses, which grow rapidly in complexity as the dimension increases. These witnesses can be exported as inhabitants of identity types in Homotopy Type Theory, and hence are of relevance in synthetic homotopy theory.

math.CT↗

arXiv2025

Naturality for higher-dimensional path types

We define a naturality construction for the operations of weak omega-categories, as a meta-operation in a dependent type theory. Our construction has a geometrical motivation as a local tensor product with a directed interval, and behaves logically as a globular analogue of Reynolds parametricity. Our construction operates as a ``power tool'' to support construction of terms with geometrical structure, and we use it to define composition operations for cylinders and cones in omega-categories. The machinery can generate terms of high complexity, and we have implemented our construction in a proof assistant, which verifies that the generated terms have the correct type. All our results can be exported to homotopy type theory, allowing the explicit computation of complex path type inhabitants.

math.CT↗

arXiv2024

CaTT contexts are finite computads

Two novel descriptions of weak ω-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are ω-categories. The second is a recursive description of a category of computads together with an adjunction to globular sets, such that the algebras for the induced monad are again ω-categories. We compare the two descriptions by showing that there exits a fully faithful morphism of categories with families from the syntactic category of CaTT to the opposite of the category of computads, which gives an equivalence on the subcategory of finite computads. We derive a more direct connection between the category of models of CaTT and the category of algebras for the monad on globular sets, induced by the adjunction with computads.

math.CT↗

arXiv2024

homotopy.io: a proof assistant for finitely-presented globular $n$-categories

We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical representation. We describe the user interface and explain how the tool can be used in practice. We also describe the essential subsystems of the tool, including collapse, contraction, expansion, typechecking, and layout, as well as key implementation details including data structure encoding, memoisation, and rendering. These technical innovations have been essential for achieving good performance in a resource-constrained setting.

cs.LO↗

arXiv2023

Posetal Diagrams for Logically-Structured Semistrict Higher Categories

We now have a wide range of proof assistants available for compositional reasoning in monoidal or higher categories which are free on some generating signature. However, none of these allow us to represent categorical operations such as products, equalizers, and similar logical techniques. Here we show how the foundational mathematical formalism of one such proof assistant can be generalized, replacing the conventional notion of string diagram as a geometrical entity living inside an n-cube with a posetal variant that allows exotic branching structure. We show that these generalized diagrams have richer behaviour with respect to categorical limits, and give an algorithm for computing limits in this setting, with a view towards future application in proof assistants.

math.CT↗

arXiv2022

Zeta-regularized Lattice Field Theory with Lorentzian background metrics

Lattice field theory is a very powerful tool to study Feynman's path integral non-perturbatively. However, it usually requires Euclidean background metrics to be well-defined. On the other hand, a recently developed regularization scheme based on Fourier integral operator $ζ$-functions can treat Feynman's path integral non-pertubatively in Lorentzian background metrics. In this article, we formally $ζ$-regularize lattice theories with Lorentzian backgrounds and identify conditions for the Fourier integral operator $ζ$-function regularization to be applicable. Furthermore, we show that the classical limit of the $ζ$-regularized theory is independent of the regularization. Finally, we consider the harmonic oscillator as an explicit example. We discuss multiple options for the regularization and analytically show that they all reproduce the correct ground state energy on the lattice and in the continuum limit. Additionally, we solve the harmonic oscillator on the lattice in Minkowski background numerically.

hep-lat↗