SearcharxivSearch

arXiv subjects

Jamie Vicary

Publications and source records attributed to Jamie Vicary.

At least 19 recordsLinked to original sources

Algebraic Priors for Approximately Equivariant Networks

Equivariant neural networks incorporate symmetries through group actions, embedding them as an inductive bias to improve performance. Existing methods learn an equivariant action on the latent space, or design architectures that are equivariant by construction. These approaches often deliver strong empirical results but can involve architecture-specific constraints, large parameter counts, and high computational cost. We challenge the paradigm of complex equivariant architectures with a parameter-free approach grounded in group representation theory. We prove that for an equivariant encoder over a finite group, the latent space must almost surely contain one copy of its regular representation for each linearly independent data orbit, which we explore with a number of empirical studies. Leveraging this foundational algebraic insight, we impose the group's regular representation as an inductive bias via an auxiliary loss, adding no learnable parameters. Our extensive evaluation shows that this method matches or outperforms specialized models in several cases, even those for infinite groups. We further validate our choice of the regular representation through an ablation study, showing it consistently outperforms defining and trivial group representation baselines.

cs.LG

Beyond Eckmann-Hilton: Commutativity in Higher Categories

We show that in a weak globular $\omega$-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 $\omega$-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

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

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

The theory and applications of anticolimits

Colimits are a fundamental construction in category theory. They provide a way to construct new objects by gluing together existing objects that are related in some way. We introduce a complementary notion of anticolimits, which provide a way to decompose an object into a colimit of other objects. While anticolimits are not unique in general, we establish that in the presence of pullbacks, there is a "canonical" anticolimit which characterises the existence of other anticolimits. We also provide convenient techniques for computing anticolimits, by changing either the shape or ambient category. The main motivation for this work is the development of a new method, known as anticontraction, for constructing homotopies in the proof assistant homotopy.io for finitely presented $n$-categories. Anticontraction complements the existing contraction method and facilitates the construction of homotopies increasing the complexity of a term, enhancing the usability of the proof assistant. For example, it simplifies the naturality move and third Reidemeister move.

math.CT

A Categorical Model for Classical and Quantum Block Designs

Classical block designs are important combinatorial structures with a wide range of applications in Computer Science and Statistics. Here we give a new abstract description of block designs based on the arrow category construction. We show that models of this structure in the category of matrices and natural numbers recover the traditional classical combinatorial objects, while models in the category of completely positive maps yield a new definition of quantum designs. We show that this generalizes both a previous notion of quantum designs given by Zauner and the traditional description of block designs. Furthermore, we demonstrate that there exists a functor which relates every categorical block design to a quantum one.

cs.ET

On Structures in Arrow Categories

In this article we investigate which categorical structures of a category C are inherited by its arrow category. In particular, we show that a monoidal equivalence between two categories gives rise to a monoidal equivalence between their arrow categories. Moreover, we examine under which circumstances an arrow category is rigid and pivotal. Finally, we derive what the (co)algebra, bialgebra and Hopf algebra objects are in an arrow category.

math.CT

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

A layout algorithm for higher-dimensional string diagrams

The algebraic zigzag construction has recently been introduced as a combinatorial foundation for a higher dimensional notion of string diagram. For use in a proof assistant, a layout algorithm is required to determine the optimal rendering coordinates, across multiple projection schemes including 2D, 3D, and 4D. For construction of these layouts, a key requirement is to determine the linear constraints which the geometrical elements must satisfy in each dimension. Here we introduce a new categorical tool called injectification, which lifts a functorial factorization system on a category to diagrams over that category, and we show that implementing this recursively in the category of finite posets allows us to systematically generate the necessary constraints. These ideas have been implemented as the layout engine of the proof assistant homotopy.io, enabling attractive and practical visualisations of complex higher categorical objects.

math.CT

From dual-unitary to biunitary: a 2-categorical model for exactly-solvable many-body quantum dynamics

Dual-unitary brickwork circuits are an exactly-solvable model for many-body chaotic quantum systems, based on 2-site gates which are unitary in both the time and space directions. Prosen has recently described an alternative model called 'dual-unitary interactions round-a-face', which we here call 'clockwork', based on 2-controlled 1-site unitaries composed in a non-brickwork structure, yet with many of the same attractive global properties. We present a 2-categorical framework that simultaneously generalizes these two existing models, and use it to show that brickwork and clockwork circuits can interact richly, yielding new types of generalized heterogeneous circuits. We show that these interactions are governed by quantum combinatorial data, which we precisely characterize. These generalized circuits remain exactly-solvable and we show that they retain the attractive features of the original models such as single-site correlation functions vanishing everywhere except on the causal light-cone. Our presented framework allows us to directly extend the notion of solvable initial states to these biunitary circuits, which are shown to result in maximal entanglement growth and exact thermalization after finitely many time steps under biunitary circuit dynamics.

quant-ph

A Syntax for Strictly Associative and Unital $\infty$-Categories

We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces desired strictness conditions. The key technical device is a new computation rule in the definitional equality of the theory, which we call insertion, defined in terms of a universal property. On terms for which it is defined, this operation "inserts" one of the arguments of a substituted coherence into the coherence itself, appropriately modifying the pasting diagram and result type, and simplifying the syntax in the process. We generate an equational theory from this reduction relation and we study its properties in detail, showing that it yields a decision procedure for equality. Expressed as a type theory, our model is well-adapted for generating and verifying efficient proofs of higher categorical statements. We illustrate this via an OCaml implementation, and give a number of examples, including a short encoding of the syllepsis, a 5-dimensional homotopy that plays an important role in the homotopy groups of spheres.

math.CT

Computads for weak $\omega$-categories as an inductive type

We give a new description of computads for weak globular $\omega$-categories by giving an explicit inductive definition of the free words. This yields a new understanding of computads, and allows a new definition of $\omega$-category that avoids the technology of globular operads. Our framework permits direct proofs of important results via structural induction, and we use this to give new proofs that every $\omega$-category is equivalent to a free one, and that the category of computads with generator-preserving maps is a presheaf topos, giving a direct description of the index category. We prove that our resulting definition of $\omega$-category agrees with that of Batanin and Leinster and that the induced notion of cofibrant replacement for $\omega$-categories coincides with that of Garner.

math.CT

Exact dynamics in dual-unitary quantum circuits with projective measurements

Dual-unitary circuits have emerged as a minimal model for chaotic quantum many-body dynamics in which the dynamics of correlations and entanglement remains tractable. Simultaneously, there has been intense interest in the effect of measurements on the dynamics of quantum information in many-body systems. In this work we introduce a class of models combining dual-unitary circuits with particular projective measurements that allow the exact computation of dynamical correlations of local observables, entanglement growth, and steady-state entanglement. We identify a symmetry preventing a measurement-induced phase transition and present exact results for the intermediate critical purification phase.

quant-ph

A Type Theory for Strictly Unital $\infty$-Categories

We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, we extend the theory with a non-trivial definitional equality. This forces some operations to coincide strictly in any model, yielding the strict unit behaviour. We make a detailed investigation of the meta-theoretic properties of this theory. We give a reduction relation that generates definitional equality, and prove that it is confluent and terminating, thus yielding the first decision procedure for equality in a strictly-unital setting. Moreover, we show that our definitional equality relation identifies all terms in a disc context, providing a point comparison with a previously proposed definition of strictly unital $\infty$-category. We also prove a conservativity result, showing that every operation of the strictly unital theory indeed arises from a valid operation in the fully weak theory. From this, we infer that strict unitality is a property of an $\infty$-category rather than additional structure.

cs.LO

Zigzag normalisation for associative $n$-categories

The theory of associative $n$-categories has recently been proposed as a strictly associative and unital approach to higher category theory. As a foundation for a proof assistant, this is potentially attractive, since it has the potential to allow simple formal proofs of complex high-dimensional algebraic phenomena. However, the theory relies on an implicit term normalisation procedure to recognize correct composites, with no recursive method available for computing it. Here we describe a new approach to term normalisation in associative $n$-categories, based on the categorical zigzag construction. This radically simplifies the theory, and yields a recursive algorithm for normalisation, which we prove is correct. Our use of categorical lifting properties allows us to give efficient proofs of our results. This normalisation algorithm forms a core component of the proof assistant homotopy.io, and we illustrate our scheme with worked examples.

cs.LO

A Type Theory for Strictly Associative Infinity Categories

Many definitions of weak and strict $\infty$-categories have been proposed. In this paper we present a definition for $\infty$-categories with strict associators, but which is otherwise fully weak. Our approach is based on the existing type theory Catt, whose models are known to correspond to weak $\infty$-categories. We add a definitional equality relation to this theory which identifies terms with the same associativity structure, yielding a new type theory Catt$_{sa}$, for strictly associative $\infty$-categories. We also provide a reduction relation which generates definitional equality, and show it is confluent and terminating, giving an algorithm for deciding equality of terms, and making typechecking decidable. Our key contribution, on which our reduction is based, is an operation on terms which we call insertion. This has a direct geometrical interpretation, allowing a subterm to be inserted into the head of the term, flatting its syntactic structure. We describe this operation combinatorially in terms of pasting diagrams, and also show can be characterized as a pushout of contexts. This allows reasoning about insertion using just its universal property.

math.CT

Traced monoidal categories as algebraic structures in $\mathbf{Prof}$

We define a traced pseudomonoid as a pseudomonoid in a monoidal bicategory equipped with extra structure, giving a new characterisation of Cauchy complete traced monoidal categories as algebraic structures in $\mathbf{Prof}$, the monoidal bicategory of profunctors. This enables reasoning about the trace using the graphical calculus for monoidal bicategories, which we illustrate in detail. We apply our techniques to study traced $*$-autonomous categories, proving a new equivalence result between the left $\otimes$-trace and the right $\unicode{8523}$-trace, and describing a new condition under which traced $*$-autonomous categories become autonomous.

math.CT