{'fraction_non_alphanumeric': 0.04317043688482127, 'fraction_numerical': 0.009867528430816291, 'mean_word_length': 4.375679618087787, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Lambek pregroups are Frobenius spiders in preorders

"Spider"is a nickname of special Frobenius algebras, a fundamental structure from mathematics, physics, and computer science. Pregroups are a fundamental structure from linguistics. Pregroups and spiders have been used together in natural language processing: one for syntax, the other for semantics. It turns out that pregroups themselves can be characterized as pointed spiders in the category of preordered relations, where they naturally arise from grammars. The other way around, preordered spider algebras in general can be characterized as unions of pregroups. This extends the characterization of relational spider algebras as disjoint unions of groups. The compositional framework that emerged with the results suggests new ways to understand and apply the basis structures in machine learning and data analysis.


Background
Special Frobenius algebras, lovingly nicknamed spiders due to their characteristic normal form (38), are frequently encountered on a wide swath of categorical applications, from topological quantum field theories, through group representations and linear algebra, to computability and complexity [23,34,56,57,59,65]. Pregroups are, on the other hand, the algebraic structure underlying modern categorial grammars [15,35,38,61]. Pregroups and spiders have been used together in computational linguistics, one for presenting the syntax, the other for assigning the vector space semantics [49,62,63]. The string diagram notation has been instrumental in combining these two structures of disjoint origins, at different levels of language modeling, to open an alley towards reconciling the two leading paradigms of natural language processing, the distributional and the compositional [8,18,24,28].
Lambek's Switching Lemma [38,Prop. 2] says that any sequent in a free pregroup can be normalized to a form where all contraction steps precede all expansion steps. It was proved inductively, as a form of cut elimination supported by the free pregroup sequents [40,Ch. 27]. The name "Switching Lemma" was introduced in Buszkowski's expositions of his decision procedure for the pregroup sequent calculus [11], and of the equivalence of pregroups and context-free languages [12]. The general method of cut elimination was introduced in Gentzen's seminal paper [26], and remained one of the central concepts of sequent calculi.

Results
Thm. 1 says that pregroups and pointed spiders are different presentations of the same variety of sequent algebras. It follows that all pregroups, not only the free ones, reduce to the normal form where all contractions are performed before all expansions. The property does not depend on inductive switching or cut elimination, which only arise in free sequent algebras. While sequent calculi generate free sequent algebras just like term calculi generate the equational algebras, the algebraic reductions, often conveniently presented as categorical diagram chasing, apply to both families of general algebras, not just the free ones. Thm. 2 is also a statement about general sequent algebras. It says that the residuation monoids are characterized by the Frobenius conditions, which determine the shape of a spider. Note that formal grammars are defined as a special family of sequent calculi (those where the generators are partitioned into the terminals and the nonterminals [16]), and that the categorial grammars are the sequent calculi corresponding to the residuation monoids [2, 36, 37, §1.2]. Thm. 3 is a statement about the spider algebras in general, which are more general than those in Thm. 1 because they are not necessarily pointed, but less general than the Frobenius algebras in Thm. 2, because the spider algebras are required to satisfy the special isometry condition, in addition to the Frobenius conditions. Thm. 3 says that a general spider can be decomposed into a consistent union of pregroups; and that the union of any consistent family of pregroups yields a spider.
The upshot is that the spiders do not appear only as the orthonormal bases of the vector space models used to assign meaning to pregroup sentences but also as the shapes of pregroups themselves. Any spider of preordered relations is a union of pregroups. A pregroup is precisely a pointed spider.

Related work
The characterization of the relational spiders over preorders extends the characterization [52] of the relational spiders over sets: unions of pregroups spiders of preordered relations = disjoint unions of groups spiders of relations While [52] was mainly concerned with the group structure of the basis elements as a quantum-algorithmic resource [53], pregroups are a structure used in natural language processing [24,45,47]. The structure of the basis elements and the basis sets correspond, respectively, to the syntactic and the semantical aspects. Modern applications require seamless integration of both aspects [32]. The presented results have been directly inspired by the DisCoCat program [24,28,62,63], and indirectly by the remarkable headways in the practices of computational linguistics over theory [10]. The author is at an early stage of studying the connections between the many fronts of progress in computational linguistics [44,48,49,61]. Beyond the current horizon, the conceptual veins from spiders' roots in categorical quantum mechanics [22,53] to their branchings through the theories of language and communication [28] continue to feed not only the theoretical explorations of sequent algebra [7,6,25] but also the practical applications and commercial technology transfers [45,47].

Why sequent algebra?
To relate Lambek's pregroups and Frobenius' algebras, both structures are presented in terms of preordered relations. This framework is slightly more general than the standard presentation, and it could be viewed as a novel contribution, or as an unnecessary distraction. In the following, I argue that it is neither.
Equational theories are usually presented as pairs (O, E), where O is a set of operations given with arities, and E is a set of equations between some terms generated from O. Algebra is the practice of deriving other valid equations. If the operations are presented as arrows, the composite operations are the paths along the arrows, the equations are the faces of directed graphs built from the arrows, and the sequences of equations can be presented as diagram chases, going back to [37].
Sequent theories are also specified as pairs (O, E), but the operations from O are now given as sequents, and E is a set of implications between some sequents derived from O. Since sequents are bulkier than terms, the sequences of sequent implications are usually written as proof trees. This gives the sequent calculi their typical appearance. Since the present work only gives rise to relatively simple sequents, I will not display the proof trees, but save space by writing the sequent derivations horizontally, with the sequents usually enclosed in parentheses. This should not conceal the fact that we are treading on the well ploughed ground of sequent algebra, going back to Axel Thue [66]. The category PRel is just a convenient categorical framework for it. But the use of sequents goes well beyond algebra. The main techniques were developed by Gerhard Gentzen, Emil Post and Andrey Markov 1 . Noam Chomsky refined and specialized sequent theories into grammars [16,17]. Formal grammars have been instrumental in specifying the syntax of programming languages [50], as well as in their operational semantics [60]. The use of sequents for specifying grammars of the natural languages goes back to Sanskrit philologist Panini from 6th century BC [5]. Lambek's pregroups belong to that tradition. The results show that the sequent view of the spider algebras and of the Frobenius conditions is a natural extension.

Overview of the paper
In Sec. 2 we set the stage for sequent algebra in the category of preorders and preordered relations, shortened to prelations. A reader with some categorical experience will be familiar with most of the concepts introduced in this section, and may want to skip forward and come back as needed. Sec. 3 describes the prelational monoids, one of the simplest structures of sequent algebra, and characterizes when they are representable as the ordinary preordered monoids. The structure of pregroups is also presented in this framework. Sec. 4 spells out the Frobenius conditions and the special isometry condition for prelations, and defines the spider algebras in this framework. Theorems 1, 2 and 3 are stated and proved in sections 5, 6, and 7, respectively. Sec. 8 discusses the repercussions of the results, in particular with respect to the goals and the limitations of pregroup grammars [40,Ch. 28].

Preorders and prelations
A preorder is a set A with a transitive, reflexive relation hold for all x, y, z ∈ A. When the underlying set A is clear or irrelevant, we write (x ← y). The preorder equivalence is the symmetric part of a preorder, defined by The quotient of A modulo the equivalence relation A ← → is the largest poset (partially ordered set) with a monotone map from A. Since this map is a surjective order embedding, every preorder is equivalent 2 to a poset.
A prelation Φ : A ց B between preorders A and B is a relation holds for all x, x ′ ∈ A and y, y ′ ∈ B. Given a prelation Ψ : B ց C, the composite (Φ ; Ψ) : A ց C is defined The transitivity makes the preordering A ← − ⊆ A × A into the identity prelation on A. The category of preorders and prelations is denoted by PRel.
Examples. Given a set A, any set of sequents {a i ← a ′ i } i∈J ⊆ A × A determines a preorder on A as its transitive reflexive closure. Given preorders A and B, any set of sequents {a i ← b i } i∈K ⊆ A × B determines a prelation A ց B as its transitive closure under A ← − on the left and B ← − on the right. 1 The same one who invented Markov chains and the n-gram model of language, all in the same paper [46]. 2 Order embeddings are a special case of what category theorists call full and faithful functors. Surjective order embeddings are thus a special case of categorical equivalences.

Monoidal structure
The main tensor products of PRel are familiar from their restrictions to PRel's smaller cousin Rel, the category of sets and relations. For any pair of preorders A and B, • the disjoint union A + B with the preorder is a biproduct in PRel, with the empty set ∅ as the zero; • the cartesian product A × B with the preorder written in the form is a symmetric monoidal product in PRel, with the singleton ½ = {∅} as the unit object.
The diagonals δ : A ց A × A and the projections ! : A ց ½ are defined by Just like in the category Rel of sets and relations, the diagonals and the projections do not form natural transformations: the former commutes only with the single-valued prelations, the latter only with the total ones.

Completions
Any preorder X embeds into the complete lattices of its lower sets and upper sets, respectively, with the opposite inclusion orderings: The embeddings map each x ∈ X into the principal lower set ↓ x = {y| x X ← − y } ∈ ⇓X and the principal It is easy to see that ⇓X is generated by the unions of the principal lower sets as the suprema, and that ⇑X is generated by the unions of the principal upper sets as the infima. They are thus X's supremum and infimum completions, respectively.

Dualities
PRel supports two dualities: where The object part of ‡ is the identity, i.e. A ‡ = A. The arrow parts map a prelation To understand ‡ : PRel op − → PRel, consider the special case when A = ½. A prelation Φ : ½ ց B can then be viewed as a lower set Φ ∈ ⇓B, and it is easy to see that Φ ‡ : B ց ½, defined as in (11), is the upper set Φ ‡ ∈ ⇑B of all upper bounds of the lower set Φ. When B = ½, then Ψ : A ց ½ is an upper set Ψ ∈ ⇑A and Ψ ‡ : ½ ց A in (11) The two dualities coincide just on the preorders that happen to be equivalence relations. The duality O gives rise to the internal adjoints in PRel on the level of objects, ‡ on the level of arrows. The former adjoints make PRel into a compact category, whereas the latter provide an internal characterization of the monotone maps between preorders.

Compact structure
On the level of the objects of PRel, the fact that every preorder B has a right adjoint 3 B o in PRel is realized by the bijections

Maps
On the level of morphisms, the adjunction conditions are In other words, (13) says that Φ is total, (14) that it is single-valued, up to the preorder equivalence. They hold together if and only if for every a ∈ A there is Φ(a) ∈ B, unique up to the preorder equivalence, such that Condition (15) means that the lower set of B-elements y that are Φ-related to a is representable by Φ(a). It is easy to see that any y ∈ B also satisfies (15) if and only if y . When B is a partial order, the preorder equivalence boils down to the equality, and a map Φ : A ց B boils down to a monotone function Φ : A − → B with (15). Maps between general preorders are still equivalent to monotone functions, but the representation is up to the preorder equivalence, and the representing functions need to be chosen.

Representations over completions
By (3) a prelation Φ : A ց B can be viewed as either of the functions and extended to which form a Galois connection which again form a Galois connection The composites of any pair of maps that form a Galois connection are closure operators, and the induced lattices of closed sets carry a reduced Galois connection. This is the nucleus of the original Galois connection [54,55,58,68]. A Galois connection is nuclear when it is its own nucleus. For the Galois connections in (16) and (17), the lattices of closed sets are isomorphic. A prelation satisfies Φ = Φ ‡ ‡ precisely when the induced Galois connections are nuclear. A representable prelation, i.e. a monotone map Φ : A − → B is always nuclear, i.e. satisfies Φ = Φ ‡ ‡ . This follows from the observation that the extensions Φ * and Φ # factor through Φ as its extensions where ↓ : B − → ⇓B and ↑ : B − → ⇑B are the supremum and the infimum completion embeddings, respectively,

Diagonals and projections are maps
The diagonal prelation δ : A ց A × A and the projection ! : Simplifying, and writing ̺ = δ ‡ and ! = ! ‡ we have It is now easy to prove which means that δ and ! are maps. In string diagrams, they are usually drawn as black-dot comonoids and monoids: It is interesting to note that ̺ :

Preordered monoids
which is upper-closed in the first two components and lower-closed in the third one, ⊥ : ½ ց A is a lower set in A. They are required to satisfy the usual monoid axioms, the associativity and the unit conditions, which correspond in PRel to the following sequents: Examples. Let M be the set of finite multisets of natural numbers, which can be viewed as functions N − → N that are 0 everywhere except at a finite number of points. Let the preordering be where Σx abbreviates the number Σ n∈N nx n . A prelational monoid can then be defined by where x + y is the multiset of (x + y) n = x n + y n . This prelational monoid is thus represented by the operation + on M. For a non-representable an non-commutative example, the reader may want to spell out the monoid over the set L of all words in some alphabet preordered by the prelation (x ← y) saying that the word x occurs within the word y, not necessarily as a prefix or contiguously. An interesting prelational monoid then admits x, y ∇ ← − z whenever z contains some shuffle of x and y. This is obviously not commutative and in the next section we explain what does it mean that it is not representable.

Representable, strict, pointed monoids
Lambek's pregroups [35,40] are monoids over preorders, with additional features and with special requirements. The additional features are the adjunction operations, discussed in Sec. 3.3. The first special requirement is that Lambek defined pregroups as partially ordered monoids, and not just preordered as above. A preordering is a partial ordering when (x ← y) and (y ← x) imply x = y. Since any preorder is order-isomorphic with its quotient 4 poset along the preorder equivalence (2), the choice between posets and preorders is a matter of notational conveniences. Posets are often more concise, but maintaining the antisymmetry in sequent algebra requires factoring out sequent loops at every step, so we leave pregroups preordered.
The second special requirement is that pregroups are representable as monoids. In other words, the underlying monoid structure (A, (∴), ι) of a pregroup in PRel is represented by monotone maps, the prelations that are total and single-valued, as defined in Sec. 2.5. A monoid (A, (∴), ι) in PRel is said to be • representable if it is both strict and pointed.
The duals (∵) = (∴) ‡ and ι = ι ‡ are drawn as the vertical flips of the diagrams for (∴) and ι. By (15) and (19), the strictness of (∴) : A × A ց A implies that for every x, y ∈ A, there is a representative x · y ∈ A such that By the same token, the unit ι : ½ ց A is pointed when it has a representative, also denoted ι ∈ A by abuse of notation, such that In other words, while a general prelational unit corresponds to a lower set ι ∈ ⇓A, a pointed unit is a principal lower set ↓ ι, and the corresponding counit ι ∈ ⇑A is the upper set ↑ ι. Note that a prelation ½ ց A can fail to satisfy the left-hand condition in (26) only if it is empty. A prelational monoid on A can have an empty unit only if A itself is empty. On the other hand, the right-hand requirement for a pointed monoid in (26) implies the right-hand condition for strictness in (25): Putting together (29) with the second part of strictness yields the equality ((∵) ; (∴)) = id A , i.e. ∃uv. x for all x, y ∈ A. In words, (30) says that (∵) : A − → A × A is total and injective, and that (∴) : A × A − → A is single-valued and surjective.

Adjunctions in monoids
The crucial structure which makes a preordered monoid into a pregroup are the operations ℓ, r : A − → A, called the ℓeft and the right adjunction, which satisfy the following inclusions Like the monoid operation (∴), the adjunction operations are assumed to be representable, i.e. for every x ∈ A there are x ℓ , x r ∈ A such that Since everything in sight in (31) is thus representable, the inclusions boil down to the implications Substituting x ℓ · x for u, the first implication gives ι ← x ℓ · x . Substituting ι, the second implication gives x · x ℓ ← ι . Proceeding with the third and the fourth implication in a similar way, and putting it all together gives the full set of adjunction sequents where we elide the dot and write ab for a · b.
Remark. Pregroups have been defined and used as partially ordered rather than preordered monoids, i.e. satisfying (x ↔ y) =⇒ x = y. The justification for reverting to preorders is given at the beginning of Sec. 3.2.
Examples. For applications in linguistics, the pregroup grammars are freely generated from some basic syntactic types. The elements of a free pregroup are sequences of literals, corresponding to all derived syntactic types, possibly annotated by sequences of a superscript ℓ or r. The ordering is generated by (34). The observations in the next section will carve out a rich source of pregroups "in nature". An interesting pair of an example and a non-example, going back to [41], which informed the introduction of pregroups into algebra, was presented in [39].

Pregroups are properties
It is often convenient to expand the adjunction sequents in (34) to adjunction correspondences valid for all a, b ∈ A. Conditions (34) and (35) are equivalent characterizations of the adjunction operations ℓ and r. The third equivalent characterization is These characterizations of adjunctions are well-known. We mention them to emphasize that being a pregroup is an intrinsic property that a monoid may have, and not an extrinsic structure that may be added to it. E.g., if every element of a monoid has an inverse, then it is a group, and this is its intrinsic property. On the other hand, an addtive group may support many different multiplication operations, and can therefore be extended into a ring in many different ways, extrinsically. Ditto for an additive monoid, which can be extended into a rig 5 in many different ways. For a monoid, being a group is thus a property, whereas being a rig is a structure. A preordered monoid (A, (∴), ι) may be a pregroup in at most one way, in if and only if for every x it has • suprema of sets in the form a| (xa ← ι) , and • infima of sets in the form b| (ι ← xb) .
Being a pregroup is thus a completeness property of a preordered monoid. E.g., all monoid structures over complete lattices are pregroups. Extending a preordered monoid into a pregroup is a completion of its preorder. The other way around, the pregroup operations also completely determine the pregroup preordering, since (35) implies A 'positive cone' of a pregroup A, i.e. a set of elements H = {h| (h ← ι)}, can be characterized without mentioning the preordering as a submonoid of the monoid A such that h ∈ H implies x r hx ∈ H for all x ∈ A and moreover x, x r ∈ H only if (x ↔ ι). Such a submonoid completely determines the preorder by (x ← y) ⇐⇒ y r x ∈ H. The crucial property that drives the applications of pregroups as algebra of sequents suitable for presenting the syntax of natural languages is that their operations, the adjoints, close the open sequents in the form (x · · · ← ι) and (ι ← x · · ·), which can be construed as capturing the processes of generation and parsing. This turns out to be an inherent capability of the spider algebras as well.

Spiders
The name spider has been used 6 to denote the monoid-comonoid couples in monoidal categories that give rise to string diagrams in the general form ∆ ∇ (38) A spider may have any number of legs. The front legs are spanned by the comonoid operation, the hind legs by the monoid operation. In each case, the multiple applications of the operation, are "flattened out" using the associativity. The crucial feature of spider algebra is the normalization to the shape of a spider, whereby all applications of the monoid operation are moved before all applications of the comonoid operation. The string diagrams representing the spider normalization laws are displayed in (39)(40). The sequent rewrites corresponding to the spider laws in PRel are spelled out above the diagrams. Formally, a spider is thus a monoid-comonoid couple satisfying the following conditions.
It is easy to see that the implications and containments dual to those displayed in (39)(40) are satisfied in all monoids: those in (39) by the associativity, the one on (40) because of the monoid unit. This was discussed at the end of Sec. 3.1. Strengthened to equations, the conditions in (39) are known as the Frobenius conditions, for reasons explained in [43,51], and the structures satisfying them are called Frobenius algebras [13,14,22,53,65]. The equational version of the condition in (40) makes the induced convolution operation isometric, and the Frobenius algebras satisfying it are called special, or shortly spiders. The sequent form in (39)(40) displays the logical content of the spider equations without the implications that are satisfied by all monoids. Since the eliminated implications are satisfied automatically, the presented analyses apply to the standard equational definitions and intuitions without a gain in generality. (26) and a spider in the sense of (39)(40).

Theorem 1. A monoid in PRel is a pregroup if and only it is pointed in the sense of
Proof. Suppose that ∇ = (∴) : A×A − → A is a pregroup operation, with the dual ∆ = (∵) : A ց A×A.
Since ∇ is thus a map, (27)(28) yield the representations The assumption x, y ii) t such that (x ← ut) and (ty ← v).
Since A is a pregroup, we use the adjoints to define s = x ℓ u and t = vy r . Together with (xy ← uv), the sequents ι ← x ℓ x and (ι ← yy r ) yield To complete the proof that the pregroup A is a pointed spider, it remains to be proved that the monoid satisfies the "specialty" condition (40) and that the point requirement (26). Both conditions are satisfied by any representable monoid, since they correspond to This completes the proof that a pregroup structure induces a pointed spider. The other way around, suppose that a dual monoid-comonoid couple (A, ∇, ∆, ⊥, ⊤) in PRel satisfy conditions (39-40) for a spider, and also the point condition (26). The Frobenius conditions (39) and the point condition (26) make ∇ total, as follows Hence the left-hand part of the strictness (25). The right-hand part of the strictness condition is just the specialty condition (40). Since the monoid is thus strict, and by the assumption in (26) also pointed, we have the representatives in (27)(28) again. To prove that the monoid ∇ : A × A − → A is a pregroup, we derive the adjoints satisfying (34) from the Frobenius conditions in (39). For a representable monoid, these conditions take the form For v = x and u = y = ι = ⊥, (44) becomes (x ← x) =⇒ ∃s. (xs ← ι) ∧ (ι ← sx) . Hence x ℓ = s.

Frobenius algebras are residuated monoids
The tight alignment of the structures of pregroups and spiders depends essentially on the assumptions which make them into maps. While convenient, these assumptions are not always natural for sequent derivations, and preclude some applications. Towards a finer alignment of the structures, and a more flexible derivational framework, in this section we characterize the Frobenius conditions (39) in terms of the monoid residue operations, on which Lambek's categorial grammars were based [36]. In the next section we shall add the isometry conditions (40) back in, and return to the spiders. A preordered monoid is said to be residuated when its operation admits the adjoints, which are for monoids called the residuations, because that is what they are for the extensions of modular multiplication monoids. Residuated monoids were first studied in [67], and the monoids of additive subgroups of rings ordered by inclusion appear in [37, §1.2]. Given a prelational monoid-comonoid dual couple (A, (∴), (∵), ι, ι ), we define • the right residuations as the mappings r⊲, ⊳r : ⇑A − → ⇓A such that ξ, y (46) hold for all x, y, z ∈ A and ξ, υ ∈ ⇑A; • the left residuations as the mappings ⊳ℓ, ℓ⊲ : ⇓A − → ⇑A such that hold for all x, y, z ∈ A and υ, ζ ∈ ⇑A

Theorem 2. A monoid in PRel satisfies the Frobenius condition if and only if it is left residuated, or equivalently if and only if it is right residuated.
Proof. Given a Frobenius algebra (A, ∇, ∆, ⊥, ⊤), the right residue operations can be defined as The left-hand equivalence in (46) follows from the left-hand Frobenius condition in (39): The right-hand equivalence corresponds to the right-hand Frobenius condition. The equivalences in (47) are ‡-dual to (46). For variation, we prove the converse by deriving the Frobenius condition from the left residual. Note that the defining conditions of the residuals say that the functions r⊲, ⊳r : ⇑A − → ⇓A and ⊳ℓ, ℓ⊲ : ⇓A − → ⇑A are surjective. For a given residuated monoid (A, (∴), (∵), ι, ι ), the left-hand of condition in (47) thus implies: We use it at the first and at the last step, and in the middle the associativity: The second Frobenius law follows symmetrically from the second residuation condition.
Examples. Genuinely prelational, non-representable monoids M and L were described in Sec The preorder Z of finite signed multisets of natural numbers, presented by finitely supported functions N − → Z, provides a slightly different situation, and another opportunity for an exercise in sequent algebra. The monoid L based on shuffling words, also described in Sec. 3.1, provides a non-example, as the residuation operations cannot be adjoined to it conservatively.
7 Spiders are unions of pregroups

Unions
A union J of a family of sets J ⊆ ℘A is its supremum in the lattice of subsets ℘A. The concept of union extends naturally to a large class of categories [3]. It also extends from lattices of subsets to lattices of subalgebras. Lattice theory was originally developed to describe such extensions [4]. If each element of J carries some structure, say of a group, then their union will also carry that structure, provided that they are consistent in a suitable sense. The consistency is usually equivalent to the requirement that any two structures in the given family are contained in a joint superstructure. The union is then the filtered supremum in the lattice of substructures. If a putative structure is a group, then the consistency requirement implies that all members of the family of groups J share the same group unit. If they don't, then their union will not be a group, but a suitable generalization. When the putative structure is not a group, but a pregroup, then the suitable generalization of the concept of pregroup is the concept of spider algebra. Our claim in this section is that the spider algebras of prelations are the unions of pregroups that are consistent, but not necessarily representable. Pregroups are monoids in the category Prd of preorders and monotone maps, but their unions are monoids in the category PRel of preorders and prelations, and the unions lift the property of being a pregroup into the property of being a spider.
family J ⊆ ℘A of subpreorders of A we define: To specify how J unifies the pregroup structures carried by the elements of J , we need to specify a notion of consistency. It seems simplest to specify it using pregroup representations.

Cayley representation of monoids
Any monoid (A, ∇, ⊥) in any monoidal category C can be represented in the monoid of endomorphisms over its carrier along the embeddings ⋉, ⋊ : where the elements C(A) are the morphisms from the monoidal unit. The embeddings in (53) , and ⊥ ⋉ = ⊥ ⋊ = id make both embeddings into monoid homomorphisms. When C is enriched, the monoid enrichment is preserved by definition.
How about the duality? When C has an identity-on-the-objects monoidal duality ‡ : C op − → C, then the Frobenius conditions assure that the monoid operations L, R : induce dualities on the monoid A, and that these dualities are preserved under the representations, in the sense This is proved by applying a Frobenius condition on each side. The converse, that such dualities also imply the Frobenius conditions, is in [53,Thm. 4.3]. The embeddings of self-dual monoids into the monoids of endomorphisms in self-dual categories were further discussed and exploited in [23,53].
It is easy to see that any lower set υ ⊆ ⊥ induces representations υ ⋉ , υ ⋊ ⊆ id A which determine a subpreorder A υ ⊆ A such that υ ⋉ = υ ⋊ = id Aυ .
A monoid covering of a preorder A is • a family of preorders J ⊆ ⇓A, written in the form J = {A i } i∈J , such that J = A, • a family of monoids (A i , ∇ i , ⊥ i ) such that for all i, j ∈ I the monoids A i and A j consistent, i.e.
a, x holds for every a ∈ A i ∩ A j and all x, y ∈ A.

Theorem 3. A preorder is a spider if and only if it has a pregroup covering.
Proof. For any monoid (A, ∇, ⊥) in PRel, the representative ⊥ ⋉ : A ց A is the identity. Viewing ⊥ : ½ ց A as the lower set ⊥ ∈ ⇓A, every t ∈ ⊥ also induces a prelation t : ½ ց A corresponding to the principal lower set ↓ t ∈ ⇓A. The representative t ⋉ : which means that A t is closed under the monoid operation in A. Denoting the restriction of ∇ to A t by ∇ t yields the submonoid (A t , ∇ t , t) of (A, ∇, ⊥). If the latter monoid is a spider, then it has the dualities from (54), which are inherited by A t by reasoning similar to (57). It follows that the monoid A t is also a spider, since conditions (39)(40) follow from the dualities. But A t is a pointed monoid, with the unit represented by t. As a pointed spider, A t is thus a pregroup, by Thm. 1. Since t was taken as an arbitrary element of ⊥, and id A = ⊥ ⋉ = t∈⊥ t ⋉ = t∈⊥ id At , it follows that where all A t are pregroups. The consistency follows from the fact that for all t ∈ ⊥, the monoid operations ∇ t on A t are restrictions of ∇ on A, and hence x ⋉t = x ⋉ . We have thus constructed a pregroup cover of an arbitrary spider.
The other way around, let J = {(A i , (∴) i , ι i )} i∈J be a consistent family of pregroups over subpreorders of A = i∈J A i . For representable monoids, the consistency boils down to the requirement that all a, x ∈ A i ∩ A j satisfy 7 a · i x = a · j x. The consistency thus implies that (∴) = i∈J (∴) i , together with ι = i∈J yields a monoid structure (A, (∴), ι), since the monoid conditions lift from the components to the union. It remains to be proved that the monoid is a spider. Thm. 1 assured that each of the pregroups A i is a spider. The fact that the consistency assures that the spider conditions also lift from the components to the union can also be checked directly, but less directly than the monoid conditions, because it involves the dual comonoids. A shorter path is to show that the consistency of the monoids implies the consistency of the duality operations L i , R i from (54) for all i ∈ J, which is straightforward. The union then produces the duality operations L, R on the monoid (A, (∴), ι), which are equivalent to the Frobenius conditions by [53,Thm. 4.3], and the specialty condition by [53,Lemma. 4.8]. This completes the construction of the spider A as a union of a consistent family of pregroups J . 7 We lift the notation a · x for the representive a · x Pregroupoids? Restricted to symmetric preorders, the unions in Thm. 3 become disjoint, pregroups boil down to groups, and the result essentially boils down to [52], where the abelian spiders in the category Rel of sets and relations were characterized as the disjoint unions of abelian groups. That result has at times been restated in terms of groupoids instead of the disjoint unions of groups. Formally, the two frameworks are equivalent, in the sense that any disjoint union of groups is a groupoid, and the skeleton of any groupoid is a disjoint union of groups, equivalent to it. In practice, however, groupoids are often significantly more flexible than the disjoint unions of groups. In homotopy theory, this was compellingly argued a while ago [9,29,64]. Reducing fundamental groupoids to fundamental groups, or splitting the quotient functors from categories to their skeletons in general, requires choosing base points, which can be arbitrarily hard. It is therefore important to note that the decompositions of spider algebras into disjoint unions of groups in Rel [52], and into unions of pregroups in PRel here, come with canonical base points, which are given by the units as the canonical base points. Omitting the base points and stating the results in terms of groupoids substantially weakens the original claims. The descriptions in terms of unions are less flexible precisely because they are more informative. On the other hand, the flexibility gained by weakening the described spider decompositions allows capturing a different correspondence, aligning the Frobenius law with invertible partial compositions [27]. Lifting this idea to the current framework suggests an interesting generalization of the pregroup unions to suitable fibrations, which must be left for future work. This is yet another paper about adjunctions. Lawvere showed that logical operations arise from adjunctions [42]. The reason is that the logical introduction and elimination rules can be specified as sequent adjunctions.
Lambek showed that substantial fragments of the syntax of natural languages can be reconstructed in terms of adjunctions [40]. The reason is that the sequents used to analyze syntax can be reduced to contractions along the counits of adjoint pairs of syntactic types. 8 Ongoing work suggests that data analysis, concept mining, and even communication in general evolve as adjunctions [30,33,54,58]. What is the impact of the presented results on these observations?
The conceptual impact is that there is a sequent-algebraic connection between a) the pregroup reductions xx ℓ ← ι ← x ℓ x and x r x ← ι ← xx r and b) the spider decompositions of (xy ← uv) into (xy ← xsv ← uv) and (xy ← uty ← uv).
The syntactic processes depicted in (a) open and close the brackets of meaning, as noted by Husserl [31,Logical Investigation IV] and formalized by Ajdukiewicz [1]. The formalism distinguished x ℓ , as a charge of a later reference x, from x r , as a discharge of an earlier x. Closing such "connexions" by reducing them to ι set the well-formed sentences apart from the background. Processes (b) allow factoring general syntactic reductions into single-component reductions. The algebraic equivalence of the two different presentations of the syntactic process does seem to have repercussions on the original epistemological analyses of language, and possibly on the present computational applications, but they are far from clear at present. 8 Since the adjunction units are never used in syntactic analyses, the question whether the actual adjunctions are really needed has been raised from the outset. In [38], pregroups were introduced only after an extended discussion about "protogroups", which are partially ordered monoids with left and right "protoinverses" x ℓ and x r equipped with contractions ι ← x ℓ x and (ι ← xx r ), but no expansions that would make them adjoint to x. The structure of a protogroup without the equation x ℓr = x rℓ = x imposed is not intrinsic to a monoid in the sense of Sec 3.4. Adding such protoinverses to a monoid obliterates any protoinverses, or any adjoints, that might have existed in it previously, and proliferates spurious types and contractions. On the other hand, a protogroup satisfying the equation x ℓr = x rℓ is a pregroup, with xx ℓ ← ι = ℓ (ι ← xx r ) and (x r x ← ι) = r ι ← x ℓ x . Maybe the observation that only the adjunction counits are used is in the eye of the observer? Maybe we use the units without noticing? Maybe the symmetry of the adjunction structure echoes the symmetry of communication: the counits are used to analyze sentences, the units to synthesize them?
The technical impact of the presented results is clearer, but they only provide an algebraic stepping stone into a problem area that opens in many directions. In [40,Ch. 28], Lambek discussed the limitations of pregroups as a context-insensitive model, and the paths forward. In the meantime, the advances in the pragmatics of natural language processing by neural nets broadened the scope of the concept of context. A context is not a mere interface between syntax and semantics. In the architecture of fast-learning nets, a context is more fruitfully interpreted as a process of selecting a syntax suitable for a given source. The narratives are parsed at several levels, with many layers of syntax. The grammars applicable at lower levels are determined by higher-level contexts. The source streams the contextual information. This communication architecture is echoed in the presented sequent-algebra model as the incremental narrowing of the monoid unit from sequent to sequent, selecting within the lower set that plays the role of the spider-algebra unit an element that plays the role of a pregroup unit and enables a syntactic reduction of the given phrase. This informal description of the process is offered as an indication of the research tasks ahead.
Leaving aside the presented results and their interpretations, the alignment of the general framework of prelational sequent algebra with the DisCoCat program seems to suggest a possible link between the functorial vector space semantics [19] and the task of understanding the monoidal functorial semantics in general [7]. If the characterization of the relational spider algebras as groups broadened the view of the basis sets beyond the linear spaces, uncovering groups as resources within the basis elements, then the characterization of the perordered spider algebras as pregroups refines the view of that resource beyond groups. Initially, the spider algebras over vector spaces provided an element-free view of the linear decompositions over the basis sets [23]. The relational and the prelational algebras as presented also provide access to the dynamic compositions within the basis elements. The comonoid part of a spider provides the external decompositions, the monoid part provides the internal compositions, and the Frobenius condition provides the interface between the two. It keeps the spider together.