-
Directed First-Order Logic
Authors:
Andrea Laretto,
Fosco Loregian,
Niccolò Veltri
Abstract:
We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as transitions/rewrites between terms, allowing for types to be interpreted as preorders. We then provide a universal property to such "directed equalities" by describing introduction and elimination rules that allows them to be contracted only with certain syntactic restrictions, base…
▽ More
We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as transitions/rewrites between terms, allowing for types to be interpreted as preorders. We then provide a universal property to such "directed equalities" by describing introduction and elimination rules that allows them to be contracted only with certain syntactic restrictions, based on polarity, which do not allow for symmetry to be derived. We give a characterization of such directed equality as a relative left adjoint, generalizing the idea by Lawvere of equality as left adjoint. The logic is equipped with a precise syntactic system of polarities, inspired by dinaturality, that keeps track of the occurrence of variables (positive/negative/both). The semantics of this logic and its system of variances is then captured categorically using the notion of directed doctrine, which we prove sound and complete with respect to the syntax.
△ Less
Submitted 15 April, 2025;
originally announced April 2025.
-
Monads and limits in bicategories of circuits
Authors:
Fosco Loregian
Abstract:
We study monads in the (pseudo-)double category $\mathbf{KSW}(\mathcal{K})$ where loose arrows are Mealy automata valued in an ambient monoidal category $\mathcal{K}$, and the category of tight arrows is $\mathcal{K}$. Such monads turn out to be elegantly described through instances of semifree bicrossed products (bicrossed products of monoids, in the sense of Zappa-Szép-Takeuchi, where one factor…
▽ More
We study monads in the (pseudo-)double category $\mathbf{KSW}(\mathcal{K})$ where loose arrows are Mealy automata valued in an ambient monoidal category $\mathcal{K}$, and the category of tight arrows is $\mathcal{K}$. Such monads turn out to be elegantly described through instances of semifree bicrossed products (bicrossed products of monoids, in the sense of Zappa-Szép-Takeuchi, where one factor is a free monoid). This result which gives an explicit description of the `free monad' double left adjoint to the forgetful functor. (Loose) monad maps are interesting as well, and relate to already known structures in automata theory. In parallel, we outline what double co/limits exist in $\mathbf{KSW}(\mathcal{K})$ and express in a synthetic language, based on double category theory, the bicategorical features of Katis-Sabadini-Walters `bicategory of circuits'.
△ Less
Submitted 3 January, 2025;
originally announced January 2025.
-
Directed equality with dinaturality
Authors:
Andrea Laretto,
Fosco Loregian,
Niccolò Veltri
Abstract:
We show how dinaturality plays a central role in the interpretation of directed type theory where types are interpreted as (1-)categories and directed equality is represented by $\hom$-functors. We present a general elimination principle based on dinaturality for directed equality which very closely resembles the $J$-rule used in Martin-Löf type theory, and we highlight which syntactical restricti…
▽ More
We show how dinaturality plays a central role in the interpretation of directed type theory where types are interpreted as (1-)categories and directed equality is represented by $\hom$-functors. We present a general elimination principle based on dinaturality for directed equality which very closely resembles the $J$-rule used in Martin-Löf type theory, and we highlight which syntactical restrictions are needed to interpret this rule in the context of directed equality. We then use these rules to characterize directed equality as a left relative adjoint to a functor between (para)categories of dinatural transformations which contracts together two variables appearing naturally with a single dinatural one, with the relative functor imposing the syntactic restrictions needed. We then argue that the quantifiers of such a directed type theory should be interpreted as ends and coends, which dinaturality allows us to present in adjoint-like correspondences to a weakening functor. Using these rules we give a formal interpretation to Yoneda reductions and (co)end calculus, and we use logical derivations to prove the Fubini rule for quantifier exchange, the adjointness property of Kan extensions via (co)ends, exponential objects of presheaves, and the (co)Yoneda lemma. We show transitivity (composition), congruence (functoriality), and transport (coYoneda) for directed equality by closely following the same approach of Martin-Löf type theory, with the notable exception of symmetry. We formalize our main theorems in Agda.
△ Less
Submitted 16 September, 2024;
originally announced September 2024.
-
Fibrations of algebras
Authors:
Danel Ahman,
Greta Coraglia,
Davide Castelnovo,
Fosco Loregian,
Nelson Martins-Ferreira,
Ülo Reimaa
Abstract:
We study fibrations arising from indexed categories of the following form: fix two categories $\mathcal{A},\mathcal{X}$ and a functor $F : \mathcal{A} \times \mathcal{X} \longrightarrow\mathcal{X} $, so that to each $F_A=F(A,-)$ one can associate a category of algebras $\mathbf{Alg}_\mathcal{X}(F_A)$ (or an Eilenberg-Moore, or a Kleisli category if each $F_A$ is a monad). We call the functor…
▽ More
We study fibrations arising from indexed categories of the following form: fix two categories $\mathcal{A},\mathcal{X}$ and a functor $F : \mathcal{A} \times \mathcal{X} \longrightarrow\mathcal{X} $, so that to each $F_A=F(A,-)$ one can associate a category of algebras $\mathbf{Alg}_\mathcal{X}(F_A)$ (or an Eilenberg-Moore, or a Kleisli category if each $F_A$ is a monad). We call the functor $\int^{\mathcal{A}}\mathbf{Alg} \to \mathcal{A}$, whose typical fibre over $A$ is the category $\mathbf{Alg}_\mathcal{X}(F_A)$, the "fibration of algebras" obtained from $F$.
Examples of such constructions arise in disparate areas of mathematics, and are unified by the intuition that $\int^\mathcal{A}\mathbf{Alg} $ is a form of semidirect product of the category $\mathcal{A}$, acting on $\mathcal{X}$, via the `representation' given by the functor $F : \mathcal{A} \times \mathcal{X} \longrightarrow\mathcal{X}$.
After presenting a range of examples and motivating said intuition, the present work focuses on comparing a generic fibration with a fibration of algebras: we prove that if $\mathcal{A}$ has an initial object, under very mild assumptions on a fibration $p : \mathcal{E}\longrightarrow \mathcal{A}$, we can define a canonical action of $\mathcal{A}$ letting it act on the fibre $\mathcal{E}_\varnothing$ over the initial object. This result bears some resemblance to the well-known fact that the fundamental group $π_1(B)$ of a base space acts naturally on the fibers $F_b = p^{-1}b$ of a fibration $p : E \to B$.
△ Less
Submitted 29 August, 2024;
originally announced August 2024.
-
Automata and coalgebras in categories of species
Authors:
Fosco Loregian
Abstract:
We study generalized automata (in the sense of Adámek-Trnková) in Joyal's category of (set-valued) combinatorial species, and as an important preliminary step, we study coalgebras for its derivative endofunctor $\partial$ and for the "Euler homogeneity operator" $L\circ\partial$ arising from the adjunction $L\dashv\partial\dashv R$. The theory is connected with, and in fact provides relatively non…
▽ More
We study generalized automata (in the sense of Adámek-Trnková) in Joyal's category of (set-valued) combinatorial species, and as an important preliminary step, we study coalgebras for its derivative endofunctor $\partial$ and for the "Euler homogeneity operator" $L\circ\partial$ arising from the adjunction $L\dashv\partial\dashv R$. The theory is connected with, and in fact provides relatively nontrivial examples of, "differential 2-rigs", a notion recently introduced by the author putting combinatorial species on the same relation a generic (differential) semiring $(R,d)$ has with the (differential) semiring $\mathbb N[\![ X]\!]$ of power series with natural coefficients. The desire to study categories of "state machines" valued in an ambient monoidal category $(\mathcal K,\otimes)$ gives a pretext to further develop the abstract theory of differential 2-rigs, proving lifting theorems of a differential 2-rig structure from $(\mathcal R,\partial)$ to the category of $\partial$-algebras on objects of $\mathcal R$, and to categories of Mealy automata valued in $(\mathcal R,\otimes)$, as well as various constructions inspired by differential algebra such as jet spaces and modules of differential operators. These theorems adapt to various "species-like" categories such as coloured species, $k$-vector species (both used in operad theory), linear species (introduced by Leroux to study combinatorial differential equations), Möbius species, and others.
△ Less
Submitted 15 August, 2024; v1 submitted 8 January, 2024;
originally announced January 2024.
-
Adjoint functor theorems for lax-idempotent pseudomonads
Authors:
Nathanael Arkor,
Ivan Di Liberti,
Fosco Loregian
Abstract:
For each pair of lax-idempotent pseudomonads $R$ and $I$, for which $I$ is locally fully faithful and $R$ distributes over $I$, we establish an adjoint functor theorem, relating $R$-cocontinuity to adjointness relative to $I$. This provides a new perspective on the nature of adjoint functor theorems, which may be seen as methods to decompose adjointness into cocontinuity and relative adjointness.…
▽ More
For each pair of lax-idempotent pseudomonads $R$ and $I$, for which $I$ is locally fully faithful and $R$ distributes over $I$, we establish an adjoint functor theorem, relating $R$-cocontinuity to adjointness relative to $I$. This provides a new perspective on the nature of adjoint functor theorems, which may be seen as methods to decompose adjointness into cocontinuity and relative adjointness. As special cases, we recover variants of the adjoint functor theorem of Freyd, the multiadjoint functor theorem of Diers, and the pluriadjoint functor theorem of Solian--Viswanathan, as well as the adjoint functor theorems for locally presentable categories. More generally, we recover enriched $Φ$-adjoint functor theorems for weakly sound classes of weight $Φ$.
△ Less
Submitted 5 June, 2024; v1 submitted 17 June, 2023;
originally announced June 2023.
-
The semibicategory of Moore automata
Authors:
Guido Boccali,
Bojana Femić,
Andrea Laretto,
Fosco Loregian,
Stefano Luneia
Abstract:
We study the semibicategory $\textsf{Mre}$ of "Moore automata": an arrangement of objects, 1- and 2-cells which is inherently and irredeemably nonunital in dimension one.
Between the semibicategory of Moore automata and the better behaved bicategory $\textsf{Mly}$ of "Mealy automata" a plethora of adjunctions insist: the well-known essential equivalence between the two kinds of state machines th…
▽ More
We study the semibicategory $\textsf{Mre}$ of "Moore automata": an arrangement of objects, 1- and 2-cells which is inherently and irredeemably nonunital in dimension one.
Between the semibicategory of Moore automata and the better behaved bicategory $\textsf{Mly}$ of "Mealy automata" a plethora of adjunctions insist: the well-known essential equivalence between the two kinds of state machines that model the definitions of $\textsf{Mre}$ and $\textsf{Mly}$ is appreciated at the categorical level, as the equivalence induced between the fixpoints of an adjunction, in fact exhibiting $\textsf{Mre}(A,B)$ as a coreflective subcategory of $\textsf{Mly}(A,B)$; the comodality induced by this adjunction is but the $0$th step of a `level-like' filtration of the bicategory $\textsf{Mre}$ in a countable family of essential bi-localizations $\textsf{s}^n\textsf{Mre}\subseteq\textsf{Mre}$. We outline a way to generate intrinsically meaningful adjunctions of this form. We mechanize some of our main results using the proof assistant Agda.
△ Less
Submitted 29 April, 2023;
originally announced May 2023.
-
Completeness for categories of generalized automata
Authors:
Guido Boccali,
Andrea Laretto,
Fosco Loregian,
Stefano Luneia
Abstract:
We present a slick proof of completeness and cocompleteness for categories of $F$-automata, where the span of maps $E\leftarrow E\otimes I \to O$ that usually defines a deterministic automaton of input $I$ and output $O$ in a monoidal category $(\mathcal K,\otimes)$ is replaced by a span $E\leftarrow F E \to O$ for a generic endofunctor $F : \mathcal K\to \mathcal K$ of a generic category…
▽ More
We present a slick proof of completeness and cocompleteness for categories of $F$-automata, where the span of maps $E\leftarrow E\otimes I \to O$ that usually defines a deterministic automaton of input $I$ and output $O$ in a monoidal category $(\mathcal K,\otimes)$ is replaced by a span $E\leftarrow F E \to O$ for a generic endofunctor $F : \mathcal K\to \mathcal K$ of a generic category $\mathcal K$: these automata exist in their `Mealy' and `Moore' version and form categories $F\text{-}\mathsf{Mly}$ and $F\text{-}\mathsf{Mre}$; such categories can be presented as strict 2-pullbacks in $\mathsf{Cat}$ and whenever $F$ is a left adjoint, both $F\text{-}\mathsf{Mly}$ and $F\text{-}\mathsf{Mre}$ admit all limits and colimits that $\mathcal K$ admits. We mechanize some of of our main results using the proof assistant Agda and the library `agda-categories`.
△ Less
Submitted 7 March, 2023;
originally announced March 2023.
-
Bicategories of Automata, Automata in Bicategories
Authors:
Guido Boccali,
Andrea Laretto,
Fosco Loregian,
Stefano Luneia
Abstract:
We study bicategories of (deterministic) automata, drawing from prior work of Katis-Sabadini-Walters, and Di Lavore-Gianola-Román-Sabadini-Sobociński, and linking their bicategories of `processes' to a bicategory of Mealy machines constructed in 1974 by R. Guitart. We make clear the sense in which Guitart's bicategory retains information about automata, proving that Mealy machines á la Guitart ide…
▽ More
We study bicategories of (deterministic) automata, drawing from prior work of Katis-Sabadini-Walters, and Di Lavore-Gianola-Román-Sabadini-Sobociński, and linking their bicategories of `processes' to a bicategory of Mealy machines constructed in 1974 by R. Guitart. We make clear the sense in which Guitart's bicategory retains information about automata, proving that Mealy machines á la Guitart identify to certain Mealy machines á la K-S-W that we call fugal automata; there is a biadjunction between fugal automata and the bicategory of K-S-W. Then, we take seriously the motto that a monoidal category is just a one-object bicategory. We define categories of Mealy and Moore machines inside a bicategory B; we specialise this to various choices of B, like categories, relations, and profunctors. Interestingly enough, this approach gives a way to interpret the universal property of reachability as a Kan extension and leads to a new notion of 1- and 2-cell between Mealy and Moore automata, that we call intertwiners, related to the universal property of K-S-W bicategory.
△ Less
Submitted 14 December, 2023; v1 submitted 7 March, 2023;
originally announced March 2023.
-
Fibrational Linguistics (FibLang): Language Acquisition
Authors:
Fabrizio Genovese,
Fosco Loregian,
Caterina Puca
Abstract:
In this work we show how FibLang, a category-theoretic framework concerned with the interplay between language and meaning, can be used to describe vocabulary acquisition, that is the process with which a speaker acquires new vocabulary (through experience or interaction).
We model two different kinds of vocabulary acquisition, which we call 'by example' and 'by paraphrasis'. The former captures…
▽ More
In this work we show how FibLang, a category-theoretic framework concerned with the interplay between language and meaning, can be used to describe vocabulary acquisition, that is the process with which a speaker acquires new vocabulary (through experience or interaction).
We model two different kinds of vocabulary acquisition, which we call 'by example' and 'by paraphrasis'. The former captures the idea of acquiring the meaning of a word by being shown a witness representing that word, as in 'understanding what a cat is, by looking at a cat'. The latter captures the idea of acquiring meaning by listening to some other speaker rephrasing the word with others already known to the learner.
We provide a category-theoretic model for vocabulary acquisition by paraphrasis based on the construction of free promonads. We draw parallels between our work and Wittgenstein's dynamical approach to language, commonly known as 'language games'.
△ Less
Submitted 31 July, 2023; v1 submitted 14 July, 2022;
originally announced July 2022.
-
Fibrational linguistics: First concepts
Authors:
Fabrizio Genovese,
Fosco Loregian,
Caterina Puca
Abstract:
We define a general mathematical framework for linguistics based on the theory of fibrations, called FibLang.
We start by modelling the interaction between linguistics and cognition in the most general way possible, with a heavy focus on conceptually motivating any assumption we make. The advantage is that FibLang remains agnostic with respect to any particular axiomatization of grammar one may…
▽ More
We define a general mathematical framework for linguistics based on the theory of fibrations, called FibLang.
We start by modelling the interaction between linguistics and cognition in the most general way possible, with a heavy focus on conceptually motivating any assumption we make. The advantage is that FibLang remains agnostic with respect to any particular axiomatization of grammar one may choose. As such, it is compatible with already existing categorical models of language (such as for example, DisCoCat), providing a formally sound framework to apply mathematical tools developed in the context of category theory, mainly categorical logic, to the study of language
△ Less
Submitted 11 July, 2022; v1 submitted 4 January, 2022;
originally announced January 2022.
-
Escrows are optics
Authors:
Fabrizio Genovese,
Fosco Loregian,
Daniele Palombi
Abstract:
We provide a categorical interpretation for escrows, i.e. trading protocols in trustless environment, where the exchange between two agents is mediated by a third party where the buyer locks the money until they receive the goods they want from the seller.
A simplified escrow system can be modeled as a certain kind of morphism in the category of optics on a monoidal category. When objects in the…
▽ More
We provide a categorical interpretation for escrows, i.e. trading protocols in trustless environment, where the exchange between two agents is mediated by a third party where the buyer locks the money until they receive the goods they want from the seller.
A simplified escrow system can be modeled as a certain kind of morphism in the category of optics on a monoidal category. When objects in the base category have monoid and comonoid structures, more involved kinds of escrows `with intermediaries' can be modelled as morphisms with action-like properties.
△ Less
Submitted 2 April, 2024; v1 submitted 20 May, 2021;
originally announced May 2021.
-
Differential 2-rigs
Authors:
Fosco Loregian,
Todd Trimble
Abstract:
We study the notion of a "differential 2-rig", a category R with coproducts and a monoidal structure distributing over them, also equipped with an endofunctor D : R -> R that satisfies a categorified analogue of the Leibniz rule. This is intended as a tool to unify various applications of such categories to computer science, algebraic topology, and enumerative combinatorics. The theory of differen…
▽ More
We study the notion of a "differential 2-rig", a category R with coproducts and a monoidal structure distributing over them, also equipped with an endofunctor D : R -> R that satisfies a categorified analogue of the Leibniz rule. This is intended as a tool to unify various applications of such categories to computer science, algebraic topology, and enumerative combinatorics. The theory of differential 2-rigs has a geometric flavour but boils down to a specialization of the theory of tensorial strengths on endofunctors; this builds a surprising connection between apparently disconnected fields. We build "free 2-rigs" on a signature, and we prove various initiality results: for example, a certain category of colored species is the free differential 2-rig on a single generator.
△ Less
Submitted 31 July, 2023; v1 submitted 1 March, 2021;
originally announced March 2021.
-
A Categorical Semantics for Hierarchical Petri Nets
Authors:
Fabrizio Romano Genovese,
Jelle Herold,
Fosco Loregian,
Daniele Palombi
Abstract:
We show how a particular variety of hierarchical nets, where the firing of a transition in the parent net must correspond to an execution in some child net, can be modelled utilizing a functorial semantics from a free category -- representing the parent net -- to the category of sets and spans between them. This semantics can be internalized via Grothendieck construction, resulting in the category…
▽ More
We show how a particular variety of hierarchical nets, where the firing of a transition in the parent net must correspond to an execution in some child net, can be modelled utilizing a functorial semantics from a free category -- representing the parent net -- to the category of sets and spans between them. This semantics can be internalized via Grothendieck construction, resulting in the category of executions of a Petri net representing the semantics of the overall hierarchical net. We conclude the paper by giving an engineering-oriented overview of how our model of hierarchical nets can be implemented in a transaction-based smart contract environment.
△ Less
Submitted 21 December, 2021; v1 submitted 29 January, 2021;
originally announced February 2021.
-
A Categorical Semantics for Bounded Petri Nets
Authors:
Fabrizio Romano Genovese,
Fosco Loregian,
Daniele Palombi
Abstract:
We provide a categorical semantics for bounded Petri nets, both in the collective- and individual-token philosophy. In both cases, we describe the process of bounding a net internally, by just constructing new categories of executions of a net using comonads, and externally, using lax-monoidal-lax functors. Our external semantics is non-local, meaning that tokens are endowed with properties that s…
▽ More
We provide a categorical semantics for bounded Petri nets, both in the collective- and individual-token philosophy. In both cases, we describe the process of bounding a net internally, by just constructing new categories of executions of a net using comonads, and externally, using lax-monoidal-lax functors. Our external semantics is non-local, meaning that tokens are endowed with properties that say something about the global state of the net. We then prove, in both cases, that the internal and external constructions are equivalent, by using machinery built on top of the Grothendieck construction. The individual-token case is harder, as it requires a more explicit reliance on abstract methods.
△ Less
Submitted 3 November, 2022; v1 submitted 22 January, 2021;
originally announced January 2021.
-
Nets with Mana: A Framework for Chemical Reaction Modelling
Authors:
Fabrizio Romano Genovese,
Fosco Loregian,
Daniele Palombi
Abstract:
We use categorical methods to define a new flavor of Petri nets where transitions can only fire a limited number of times, specified by a quantity that we call mana. We do so with chemistry in mind, looking at ways of modelling the behavior of chemical reactions that depend on enzymes to work. We prove that such nets can be either obtained as a result of a comonadic construction, or by enriching t…
▽ More
We use categorical methods to define a new flavor of Petri nets where transitions can only fire a limited number of times, specified by a quantity that we call mana. We do so with chemistry in mind, looking at ways of modelling the behavior of chemical reactions that depend on enzymes to work. We prove that such nets can be either obtained as a result of a comonadic construction, or by enriching them with extra information encoded into a functor. We then use a well-established categorical result to prove that the two constructions are equivalent, and generalize them to the case where the firing of some transitions can "regenerate" the mana of others. This allows us to represent the action of catalysts and also of biochemical processes where the byproducts of some chemical reaction are exactly the enzymes that another reaction needs to work.
△ Less
Submitted 22 April, 2021; v1 submitted 15 January, 2021;
originally announced January 2021.
-
Rosen's no-go theorem for regular categories
Authors:
Fosco Loregian
Abstract:
The famous biologist Robert Rosen argued for an intrinsic difference between biological and artificial life, supporting the claim that `living systems are not mechanisms'. This result, understood as the claim that life-like mechanisms are non-computable, can be phrased as the non-existence of an equivalence between a category of `static'/analytic elements and a category of `variable'/synthetic ele…
▽ More
The famous biologist Robert Rosen argued for an intrinsic difference between biological and artificial life, supporting the claim that `living systems are not mechanisms'. This result, understood as the claim that life-like mechanisms are non-computable, can be phrased as the non-existence of an equivalence between a category of `static'/analytic elements and a category of `variable'/synthetic elements.
The property of a system of being synthetic, understood as being the gluing of `variable families' of analytica, must imply that the latter class of objects does not retain sufficient information in order to describe said variability; we contribute to this thesis with an argument rooted in elementary category theory.
Seen as such, Rosen's `proof' that no living system can be a mechanism arises from a tension between two contrapuntal needs: on one side, the necessity to consider (synthetically) variable families of systems; on the other, the necessity to describe a syntheticum via an universally chosen analyticum.
△ Less
Submitted 20 May, 2021; v1 submitted 21 December, 2020;
originally announced December 2020.
-
Coends of higher arity
Authors:
Fosco Loregian,
Emily de Oliveira Santos
Abstract:
We specialise a recently introduced notion of generalised dinaturality for functors $T : (\mathcal{C}^\text{op})^p \times \mathcal{C}^q \to \mathcal{D}$ to the case where the domain (resp., codomain) is constant, obtaining notions of ends (resp., coends) of higher arity, dubbed herein $(p,q)$-ends (resp., $(p,q)$-coends). While higher arity co/ends are particular instances of "totally symmetrised"…
▽ More
We specialise a recently introduced notion of generalised dinaturality for functors $T : (\mathcal{C}^\text{op})^p \times \mathcal{C}^q \to \mathcal{D}$ to the case where the domain (resp., codomain) is constant, obtaining notions of ends (resp., coends) of higher arity, dubbed herein $(p,q)$-ends (resp., $(p,q)$-coends). While higher arity co/ends are particular instances of "totally symmetrised" (ordinary) co/ends, they serve an important technical role in the study of a number of new categorical phenomena, which may be broadly classified as two new variants of category theory.
The first of these, weighted category theory, consists of the study of weighted variants of the classical notions and construction found in ordinary category theory, besides that of a limit. This leads to a host of varied and rich notions, such as weighted Kan extensions, weighted adjunctions, and weighted ends.
The second, diagonal category theory, proceeds in a different (albeit related) direction, in which one replaces universality with respect to natural transformations with universality with respect to dinatural transformations, mimicking the passage from limits to ends. In doing so, one again encounters a number of new interesting notions, among which one similarly finds diagonal Kan extensions, diagonal adjunctions, and diagonal ends.
△ Less
Submitted 27 November, 2020;
originally announced November 2020.
-
Functorial Semantics for Partial Theories
Authors:
Ivan Di Liberti,
Fosco Loregian,
Chad Nester,
Paweł Sobociński
Abstract:
We provide a Lawvere-style definition for partial theories, extending the classical notion of equational theory by allowing partially defined operations. As in the classical case, our definition is syntactic: we use an appropriate class of string diagrams as terms. This allows for equational reasoning about the class of models defined by a partial theory. We demonstrate the expressivity of such eq…
▽ More
We provide a Lawvere-style definition for partial theories, extending the classical notion of equational theory by allowing partially defined operations. As in the classical case, our definition is syntactic: we use an appropriate class of string diagrams as terms. This allows for equational reasoning about the class of models defined by a partial theory. We demonstrate the expressivity of such equational theories by considering a number of examples, including partial combinatory algebras and cartesian closed categories. Moreover, despite the increase in expressivity of the syntax we retain a well-behaved notion of semantics: we show that our categories of models are precisely locally finitely presentable categories, and that free models exist.
△ Less
Submitted 12 November, 2020;
originally announced November 2020.
-
t-structures on stable infinity-categories
Authors:
Fosco Loregian
Abstract:
The present work re-enacts the classical theory of t-structures reducing the classical definition given in *Faisceaux Pervers* to a rather primitive categorical gadget: suitable reflective factorization systems. This translation is only possible due to the virtues of the infinity-categorical setting. Once the basic theory of t-structure has been developed, a natural direction of research is to dev…
▽ More
The present work re-enacts the classical theory of t-structures reducing the classical definition given in *Faisceaux Pervers* to a rather primitive categorical gadget: suitable reflective factorization systems. This translation is only possible due to the virtues of the infinity-categorical setting. Once the basic theory of t-structure has been developed, a natural direction of research is to develop a comprehensive treatment of t-structure in the "torsio-centric" perspective: we apply the technology of factorization systems to the theory of Postnikov towers, to the proof of the abelianity of the heart of a t-structure, and to the theory of Bridgeland's stability conditions.
△ Less
Submitted 28 May, 2020;
originally announced May 2020.
-
Profunctor Optics, a Categorical Update
Authors:
Bryce Clarke,
Derek Elkins,
Jeremy Gibbons,
Fosco Loregian,
Bartosz Milewski,
Emily Pillmore,
Mario Román
Abstract:
Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed sett…
▽ More
Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.
△ Less
Submitted 20 February, 2024; v1 submitted 21 January, 2020;
originally announced January 2020.
-
The Essence of Petri Net Gluings
Authors:
Fabrizio Genovese,
Fosco Loregian,
Daniele Palombi
Abstract:
Many categorical frameworks have been proposed to formalize the idea of gluing Petri nets with each other. Such frameworks model net gluings in terms of sharing of resources or synchronization of transitions. Interpretations given to these gluings are more or less satisfactory when we consider Petri nets with a semantics attached to them.
In this work, we define a framework to compose Petri nets…
▽ More
Many categorical frameworks have been proposed to formalize the idea of gluing Petri nets with each other. Such frameworks model net gluings in terms of sharing of resources or synchronization of transitions. Interpretations given to these gluings are more or less satisfactory when we consider Petri nets with a semantics attached to them.
In this work, we define a framework to compose Petri nets together in such a way that their semantics is respected. In addition to this, we show how our framework generalizes the previously defined ones.
△ Less
Submitted 26 June, 2023; v1 submitted 8 September, 2019;
originally announced September 2019.
-
A Fubini rule for $\infty$-coends
Authors:
Fosco Loregian
Abstract:
We prove a Fubini rule for $\infty$-co/ends of $\infty$-functors $F : \mathcal C^\text{op}\times\mathcal C\to \mathcal D$. This allows to lay down "integration rules", similar to those in classical co/end calculus, also in the setting of $\infty$-categories.
We prove a Fubini rule for $\infty$-co/ends of $\infty$-functors $F : \mathcal C^\text{op}\times\mathcal C\to \mathcal D$. This allows to lay down "integration rules", similar to those in classical co/end calculus, also in the setting of $\infty$-categories.
△ Less
Submitted 16 February, 2019;
originally announced February 2019.
-
A standard theorem on adjunctions in two variables
Authors:
Fosco Loregian
Abstract:
We record an explicit proof of the theorem that lifts a two-variable adjunction to the arrow categories of its domains.
We record an explicit proof of the theorem that lifts a two-variable adjunction to the arrow categories of its domains.
△ Less
Submitted 16 February, 2019;
originally announced February 2019.
-
On the unicity of formal category theories
Authors:
Ivan Di Liberti,
Fosco Loregian
Abstract:
We prove an equivalence between cocomplete Yoneda structures and certain proarrow equipments on a 2-category $\mathcal K$. In order to do this, we recognize the presheaf construction of a cocomplete Yoneda structure as a relative, lax idempotent monad sending each admissible 1-cell $f :A \to B$ to an adjunction $\boldsymbol{P}_!f\dashv\boldsymbol{P}^*f$. Each cocomplete Yoneda structure on…
▽ More
We prove an equivalence between cocomplete Yoneda structures and certain proarrow equipments on a 2-category $\mathcal K$. In order to do this, we recognize the presheaf construction of a cocomplete Yoneda structure as a relative, lax idempotent monad sending each admissible 1-cell $f :A \to B$ to an adjunction $\boldsymbol{P}_!f\dashv\boldsymbol{P}^*f$. Each cocomplete Yoneda structure on $\mathcal K$ arises in this way from a relative lax idempotent monad "with enough adjoint 1-cells", whose domain generates the ideal of admissibles, and the Kleisli category of such a monad equips its domain with proarrows. We call these structures "yosegi". Quite often, the presheaf construction associated to a yosegi generates an ambidextrous Yoneda structure; in such a setting there exists a fully formal version of Isbell duality.
△ Less
Submitted 6 January, 2019;
originally announced January 2019.
-
Categorical notions of fibration
Authors:
Fosco Loregian,
Emily Riehl
Abstract:
Fibrations over a category $B$, introduced to category theory by Grothendieck, encode pseudo-functors $B^{op} \rightsquigarrow {\bf Cat}$, while the special case of discrete fibrations encode presheaves $B^{op} \to {\bf Set}$. A two-sided discrete variation encodes functors $B^{op} \times A \to {\bf Set}$, which are also known as profunctors from $A$ to $B$. By work of Street, all of these fibrati…
▽ More
Fibrations over a category $B$, introduced to category theory by Grothendieck, encode pseudo-functors $B^{op} \rightsquigarrow {\bf Cat}$, while the special case of discrete fibrations encode presheaves $B^{op} \to {\bf Set}$. A two-sided discrete variation encodes functors $B^{op} \times A \to {\bf Set}$, which are also known as profunctors from $A$ to $B$. By work of Street, all of these fibration notions can be defined internally to an arbitrary 2-category or bicategory. While the two-sided discrete fibrations model profunctors internally to ${\bf Cat}$, unexpectedly, the dual two-sided codiscrete cofibrations are necessary to model $\cal V$-profunctors internally to $\cal V$-$\bf Cat$.
△ Less
Submitted 16 February, 2019; v1 submitted 15 June, 2018;
originally announced June 2018.
-
Accessibility and presentability in 2-categories
Authors:
Ivan Di Liberti,
Fosco Loregian
Abstract:
We outline a definition of accessible and presentable objects in a 2-category $\mathcal K$ endowed with a "KZ context", that is to say a pair of lax-idempotent monads interacting in a prescribed way; this perspective suggests a unified treatment of many "Gabriel-Ulmer like" theorems, asserting how presentable objects arise as reflections of generating ones. We outline the notion of "(Gabriel-Ulmer…
▽ More
We outline a definition of accessible and presentable objects in a 2-category $\mathcal K$ endowed with a "KZ context", that is to say a pair of lax-idempotent monads interacting in a prescribed way; this perspective suggests a unified treatment of many "Gabriel-Ulmer like" theorems, asserting how presentable objects arise as reflections of generating ones. We outline the notion of "(Gabriel-Ulmer) envelope" for a KZ context, sufficient to concoct Gabriel-Ulmer duality. We end the paper with a roundup of examples, involving classical (set-based and enriched), low dimensional category theory, and a perspective for future work, rooted in higher category theory and homotopy theory.
△ Less
Submitted 25 May, 2022; v1 submitted 23 April, 2018;
originally announced April 2018.
-
Localization theory for derivators
Authors:
Fosco Loregian
Abstract:
We outline the theory of reflections for prederivators, derivators and stable derivators. In order to parallel the classical theory valid for categories, we outline how reflections can be equivalently described as categories of fractions, reflective factorization systems, and categories of algebras for idempotent monads. This is a further development of the theory of monads and factorization syste…
▽ More
We outline the theory of reflections for prederivators, derivators and stable derivators. In order to parallel the classical theory valid for categories, we outline how reflections can be equivalently described as categories of fractions, reflective factorization systems, and categories of algebras for idempotent monads. This is a further development of the theory of monads and factorization systems for derivators.
△ Less
Submitted 22 February, 2018;
originally announced February 2018.
-
Factorization systems on (stable) derivators
Authors:
Fosco Loregian,
Simone Virili
Abstract:
We define triangulated factorization systems on triangulated categories, and prove that a suitable subclass thereof (the normal triangulated torsion theories) corresponds bijectively to $t$-structures on the same category. This result is then placed in the framework of derivators regarding a triangulated category as the base of a stable derivator. More generally, we define derivator factorization…
▽ More
We define triangulated factorization systems on triangulated categories, and prove that a suitable subclass thereof (the normal triangulated torsion theories) corresponds bijectively to $t$-structures on the same category. This result is then placed in the framework of derivators regarding a triangulated category as the base of a stable derivator. More generally, we define derivator factorization systems in the 2-category $\mathrm{PDer}$, describing them as algebras for a suitable strict 2-monad (this result is of independent interest), and prove that a similar characterization still holds true: for a stable derivator $\mathbb D$, a suitable class of derivator factorization systems (the normal derivator torsion theories) correspond bijectively with $t$-structures on the base $\mathbb{D}(\mathbb{1})$ of the derivator. These two result can be regarded as the triangulated- and derivator- analogues, respectively, of the theorem that says that `$t$-structures are normal torsion theories' in the setting of stable $\infty$-categories, showing how the result remains true whatever the chosen model for stable homotopy theory is.
△ Less
Submitted 10 February, 2018; v1 submitted 23 May, 2017;
originally announced May 2017.
-
Homotopical algebra is not concrete
Authors:
Fosco Loregian,
Ivan Di Liberti
Abstract:
We generalize Freyd's well-known result that "homotopy is not concrete", offering a general method to show that under certain assumptions on a model category $\mathcal M$, its homotopy category $\text{ho}(\mathcal M)$ cannot be concrete. This result is part of an attempt to understand more deeply the relation between set theory and abstract homotopy theory.
We generalize Freyd's well-known result that "homotopy is not concrete", offering a general method to show that under certain assumptions on a model category $\mathcal M$, its homotopy category $\text{ho}(\mathcal M)$ cannot be concrete. This result is part of an attempt to understand more deeply the relation between set theory and abstract homotopy theory.
△ Less
Submitted 26 January, 2018; v1 submitted 2 April, 2017;
originally announced April 2017.
-
Recollements in stable $\infty$-categories
Authors:
Domenico Fiorenza,
Fosco Loregian
Abstract:
We develop the theory of recollements in a stable $\infty$-categorical setting. In the axiomatization of Beilinson, Bernstein and Deligne, recollement situations provide a generalization of Grothendieck's "six functors" between derived categories. The adjointness relations between functors in a recollement $\mathbf{D}^0\leftrightarrow \mathbf{D} \leftrightarrow \mathbf{D}^1$ induce a "recollée"…
▽ More
We develop the theory of recollements in a stable $\infty$-categorical setting. In the axiomatization of Beilinson, Bernstein and Deligne, recollement situations provide a generalization of Grothendieck's "six functors" between derived categories. The adjointness relations between functors in a recollement $\mathbf{D}^0\leftrightarrow \mathbf{D} \leftrightarrow \mathbf{D}^1$ induce a "recollée" $t$-structure $\mathfrak{t}_0\uplus\mathfrak{t}1$ on $\mathbf{D}$ , given $t$-structures $\mathfrak{t}_0,\mathfrak{t}_1$ on $\mathbf{D}^0, \mathbf{D}^1$. Such a classical result, well-known in the setting of triangulated categories, is recasted in the setting of stable $\infty$-categories and the properties of the associated ($\infty$-categorical) factorization systems are investigated. In the geometric case of a stratified space, various recollements arise, which "interact well" with the combinatorics of the intersections of strata to give a well-defined, associative $\uplus$ operation. From this we deduce a generalized associative property for $n$-fold gluing $\mathfrak{t}_0\uplus\cdots\uplus \mathfrak{t}_n$, valid in any stable $\infty$-category.
△ Less
Submitted 26 May, 2016; v1 submitted 14 July, 2015;
originally announced July 2015.
-
Hearts and towers in stable infinity-categories
Authors:
Domenico Fiorenza,
Fosco Loregian,
Giovanni Marchetti
Abstract:
We exploit the equivalence between $t$-structures and normal torsion theories on a stable $\infty$-category to show how a few classical topics in the theory of triangulated categories, i.e., the characterization of bounded $t$-structures in terms of their hearts, their associated cohomology functors, semiorthogonal decompositions, and the theory of tiltings, as well as the more recent notion of Br…
▽ More
We exploit the equivalence between $t$-structures and normal torsion theories on a stable $\infty$-category to show how a few classical topics in the theory of triangulated categories, i.e., the characterization of bounded $t$-structures in terms of their hearts, their associated cohomology functors, semiorthogonal decompositions, and the theory of tiltings, as well as the more recent notion of Bridgeland's slicings, are all particular instances of a single construction, namely, the tower of a morphism associated with a $J$-slicing of a stable $\infty$-category $\mathcal C$, where $J$ is a totally ordered set equipped with a monotone $\mathbb{Z}$-action.
△ Less
Submitted 1 May, 2019; v1 submitted 19 January, 2015;
originally announced January 2015.
-
Coend calculus
Authors:
Fosco Loregian
Abstract:
The book formerly known as "This is the (co)end, my only (co)friend".
The book formerly known as "This is the (co)end, my only (co)friend".
△ Less
Submitted 21 May, 2023; v1 submitted 11 January, 2015;
originally announced January 2015.
-
t-structures are normal torsion theories
Authors:
Domenico Fiorenza,
Fosco Loregian
Abstract:
We characterize $t$-structures in stable $\infty$-categories as suitable quasicategorical factorization systems. More precisely we show that a $t$-structure $\mathfrak{t}$ on a stable $\infty$-category $\mathbf{C}$ is equivalent to a normal torsion theory $\mathbb{F}$ on $\mathbf{C}$, i.e. to a factorization system $\mathbb{F}=(\mathcal{E},\mathcal{M})$ where both classes satisfy the 3-for-2 cance…
▽ More
We characterize $t$-structures in stable $\infty$-categories as suitable quasicategorical factorization systems. More precisely we show that a $t$-structure $\mathfrak{t}$ on a stable $\infty$-category $\mathbf{C}$ is equivalent to a normal torsion theory $\mathbb{F}$ on $\mathbf{C}$, i.e. to a factorization system $\mathbb{F}=(\mathcal{E},\mathcal{M})$ where both classes satisfy the 3-for-2 cancellation property, and a certain compatibility with pullbacks/pushouts.
△ Less
Submitted 3 April, 2015; v1 submitted 29 August, 2014;
originally announced August 2014.
