-
A computational method for left-adjointness
Authors:
Simon Forest
Abstract:
In this work, we investigate an effective method for showing that functors between categories are left adjoints. The method applies to a large class of categories, namely locally finitely presentable categories, which are ubiquitous in practice and include standard examples like Set, Grp, etc. Our method relies on a known description of these categories as orthogonal sub-classes of presheaf catego…
▽ More
In this work, we investigate an effective method for showing that functors between categories are left adjoints. The method applies to a large class of categories, namely locally finitely presentable categories, which are ubiquitous in practice and include standard examples like Set, Grp, etc. Our method relies on a known description of these categories as orthogonal sub-classes of presheaf categories. The functors on which our method applies are the ones that can be presented as particular profunctors, called Kan models in this context. The method for left-adjointness then relies on computing that a particular criterion is satisfied. From this method, we also derive another method for showing that a category is cartesian closed. As proofs of concept and effectivity, we give a concrete implementation of the structures and of the left-adjointness criterion in OCaml and apply it on several examples.
△ Less
Submitted 27 January, 2025; v1 submitted 8 November, 2024;
originally announced November 2024.
-
An Analysis of Symmetry in Quantitative Semantics
Authors:
Pierre Clairambault,
Simon Forest
Abstract:
In this paper, we build on a recent bicategorical model called thin spans of groupoids, introduced by Clairambault and Forest. Notably, thin spans feature a decomposition of symmetry into two sub-groupoids of polarized -- positive and negative -- symmetries. We first construct a variation of the original exponential of thin spans, based on sequences rather than families. Then we give a syntactic c…
▽ More
In this paper, we build on a recent bicategorical model called thin spans of groupoids, introduced by Clairambault and Forest. Notably, thin spans feature a decomposition of symmetry into two sub-groupoids of polarized -- positive and negative -- symmetries. We first construct a variation of the original exponential of thin spans, based on sequences rather than families. Then we give a syntactic characterisation of the interpretation of simply-typed lambda-terms in thin spans, in terms of rigid intersection types and rigid resource terms. Finally, we formally relate thin spans with the weighted relational model and generalized species of structure. This allows us to show how some quantities in those models reflect polarized symmetries: in particular we show that the weighted relational model counts witnesses from generalized species of structure, divided by the cardinal of a group of positive symmetries.
△ Less
Submitted 30 January, 2024;
originally announced January 2024.
-
The Cartesian Closed Bicategory of Thin Spans of Groupoids
Authors:
Pierre Clairambault,
Simon Forest
Abstract:
Recently, there has been growing interest in bicategorical models of programming languages, which are "proof-relevant" in the sense that they keep distinct account of execution traces leading to the same observable outcomes, while assigning a formal meaning to reduction paths as isomorphisms.
In this paper we introduce a new model, a bicategory called thin spans of groupoids. Conceptually it is…
▽ More
Recently, there has been growing interest in bicategorical models of programming languages, which are "proof-relevant" in the sense that they keep distinct account of execution traces leading to the same observable outcomes, while assigning a formal meaning to reduction paths as isomorphisms.
In this paper we introduce a new model, a bicategory called thin spans of groupoids. Conceptually it is close to Fiore et al.'s generalized species of structures and to Melliès' homotopy template games, but fundamentally differs as to how replication of resources and the resulting symmetries are treated. Where those models are saturated -- the interpretation is inflated by the fact that semantic individuals may carry arbitrary symmetries -- our model is thin, drawing inspiration from thin concurrent games: the interpretation of terms carries no symmetries, but semantic individuals satisfy a subtle invariant defined via biorthogonality, which guarantees their invariance under symmetry.
We first build the bicategory $\mathbf{Thin}$ of thin spans of groupoids. Its objects are certain groupoids with additional structure, its morphisms are spans composed via plain pullback with identities the identity spans, and its $2$-cells are span morphisms making the induced triangles commute only up to natural isomorphism. We then equip $\mathbf{Thin}$ with a pseudocomonad $!$, and finally show that the Kleisli bicategory $\mathbf{Thin}_{!}$ is cartesian closed.
△ Less
Submitted 27 January, 2023;
originally announced January 2023.
-
Free precategories as presheaf categories
Authors:
Simon Forest,
Samuel Mimram
Abstract:
Precategories generalize both the notions of strict $n$-category and sesquicategory: their definition is essentially the same as the one of strict $n$-categories, excepting that we do not require the various interchange laws to hold. Those have been proposed as a framework in which one can express semi-strict definitions of weak higher categories: in dimension 3, Gray categories are an instance of…
▽ More
Precategories generalize both the notions of strict $n$-category and sesquicategory: their definition is essentially the same as the one of strict $n$-categories, excepting that we do not require the various interchange laws to hold. Those have been proposed as a framework in which one can express semi-strict definitions of weak higher categories: in dimension 3, Gray categories are an instance of them and have been shown to be equivalent to tricategories, and definitions of semi-strict tetracategories have been proposed, and used as the basis of proof assistants such as Globular. In this article, we are mostly interested in free precategories. Those can be presented by generators and relations, using an appropriate variation on the notion of polygraph (aka computad), and earlier works have shown that the theory of rewriting can be generalized to this setting, enjoying most of the fundamental constructions and properties which can be found in the traditional theory, contrarily to polygraphs for strict categories. We further study here why this is the case, by providing several results which show that precategories and their associated polygraphs bear properties which ensure that we have a good syntax for those. In particular, we show that the category of polygraphs for precategories form a presheaf category.
△ Less
Submitted 29 November, 2022;
originally announced November 2022.
-
An extension of Batanin's approach to globular algebras
Authors:
Simon Forest
Abstract:
In earlier work, Batanin has shown that an important class of definitions of higher categories could be apprehended together simply as monads over globular sets. This allowed him to generalize the notion of polygraph, initially introduced by Street and Burroni for strict categories, to all algebraic globular higher categories. In this work, we refine this perspective and introduce new construction…
▽ More
In earlier work, Batanin has shown that an important class of definitions of higher categories could be apprehended together simply as monads over globular sets. This allowed him to generalize the notion of polygraph, initially introduced by Street and Burroni for strict categories, to all algebraic globular higher categories. In this work, we refine this perspective and introduce new constructions and properties for this class of higher categories. In particular, we define the notion of cellular extension and its associated free construction, from which we obtain another definition of polygraphs and the adjunction between globular algebras and polygraphs. We moreover introduce two criteria allowing one to use most of the constructions of this article without having to describe explicitly the underlying globular monad.
△ Less
Submitted 5 April, 2022;
originally announced April 2022.
-
Rewriting in Gray categories with applications to coherence
Authors:
Simon Forest,
Samuel Mimram
Abstract:
Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which include Gray categor…
▽ More
Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which include Gray categories as particular cases, and are adapted to mechanized computations. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed. We also extend Squier's theorem to our context, showing that a convergent rewriting system is coherent, which means that any two parallel 3-cells are necessarily equal. This allows us to prove coherence results for several well-known structures in the context of Gray categories: monoids, adjunctions, Frobenius monoids.
△ Less
Submitted 29 November, 2022; v1 submitted 11 September, 2021;
originally announced September 2021.
-
Unifying notions of pasting diagrams
Authors:
Simon Forest
Abstract:
In this work, we relate the three main formalisms for the notion of pasting diagram in strict $ω$-categories: Street's parity complexes, Johnson's pasting schemes and Steiner's augmented directed complexes. In the process, we show that the axioms of parity complexes and pasting schemes are not strong enough for them to correctly represent pasting diagrams, and we do so by providing a counter-examp…
▽ More
In this work, we relate the three main formalisms for the notion of pasting diagram in strict $ω$-categories: Street's parity complexes, Johnson's pasting schemes and Steiner's augmented directed complexes. In the process, we show that the axioms of parity complexes and pasting schemes are not strong enough for them to correctly represent pasting diagrams, and we do so by providing a counter-example. Then, we introduce a new formalism, called torsion-free complexes, which aims at encompassing the three other ones. We prove its correctness by providing a detailed proof that an instance induces a free $ω$-category. Next, we prove that the three other formalisms can be embedded in some sense in the new one. Finally, we show that there are no other embedding between these four formalisms.
△ Less
Submitted 23 July, 2021; v1 submitted 1 March, 2019;
originally announced March 2019.
-
Well-posedness for the microcurl model in both single and polycrystal gradient plasticity
Authors:
Francois Ebobisse,
Patrizio Neff,
Samuel Forest
Abstract:
We consider the recently introduced microcurl model which is a variant of strain gradient plasticity in which the curl of the plastic distortion is coupled to an additional micromorphic-type field. For both single crystal and polycrystal cases, we formulate the model and show its well-posedness in the rate-independent case provided some local hardening (isotropic or linear kinematic) is taken into…
▽ More
We consider the recently introduced microcurl model which is a variant of strain gradient plasticity in which the curl of the plastic distortion is coupled to an additional micromorphic-type field. For both single crystal and polycrystal cases, we formulate the model and show its well-posedness in the rate-independent case provided some local hardening (isotropic or linear kinematic) is taken into account. To this end, we use the functional analytical framework developed by Han-Reddy. We also compare the model to the relaxed micromorphic model as well as to a dislocation-based gradient plasticity model.
△ Less
Submitted 22 August, 2016;
originally announced August 2016.
