Proof assistants and formalization projects

Monoidal categories

monoidal categories

With symmetry

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory



DisCoPy is a toolbox for computing with string diagrams, monoidal categories and strong monoidal functors in Python. It is available on GitHub.

The name stands for Distributional Compositional Python, indeed the package was first intended as an implementation of the DisCoCat models of natural language.

String diagrams

The core data structure is Diagram, an implementation of string diagrams in the free premonoidal category.

Fix a monoidal signature Σ=Σ 1dom,codΣ 0 \Sigma = \Sigma_1 \xrightarrow{\text{dom}, \text{cod}} \Sigma_0^\star for a set of boxes Σ 1\Sigma_1, a set of objects Σ 0\Sigma_0 and its free monoid Σ 0 \Sigma_0^\star, we write f:stf \colon s \to t for fΣ 1f \in \Sigma_1 whenever dom(f)=s\text{dom}(f) = s and cod(f)=t\text{cod}(f) = t. Let L(Σ)=Σ 0 ×Σ 1×Σ 0 L(\Sigma) = \Sigma_0^\star \times \Sigma_1 \times \Sigma_0^\star, a layer is a triple l=(u,f:st,v)L(Σ)l = (u, f \colon s \to t, v) \in L(\Sigma), where we define dom(l)=usv\text{dom}(l) = u s v and cod(l)=utv\text{cod}(l) = u t v. It is depicted, in string diagram-notation, as:

The set of diagrams D(Σ)D(\Sigma) is the set of arrows in the free category generated by the layers L(Σ)L(\Sigma), considered as a directed graph. Concretely, dd is given by a length len(d)=n\text{len}(d) = n \in \mathbb{N}, a domain dom(d)Σ 0 \text{dom}(d) \in \Sigma_0^\star and a list of layers layers(d)=(d 1,,d n)L(Σ) n\layers(d) = (d_1, \dots, d_n) \in L(\Sigma)^n such that dom(d)=dom(d 0)\text{dom}(d) = \text{dom}(d_0) and cod(d i)=dom(d i+1)\text{cod}(d_i) = \text{dom}(d_{i + 1}) for each ini \leq n. The codomain of a diagram is the codomain of its last layer cod(d)=cod(d n)\cod(d) = \cod(d_n).

Note that in order to define a diagram uniquely, its layers have more data than necessary. It is enough to specify a list boxes(d)Σ 1 n\boxes(d) \in \Sigma_1^n of generators together with a list offsets(d)N n\offsets(d) \in \N^n: the number of wires on the left of each box. This is the definition used in Delpeuch and Vicary (2018), Globular, as well as DisCoPy.

We can define identity, composition and tensor of diagrams in terms of this combinatorial encoding:

Diagrams in the free monoidal category can be seen as premonoidal diagrams quotiented by the interchanger, i.e. the naturality equation for the monoidal product: f1 c1 bg=1 agf1 df \otimes 1_c \circ 1_b \otimes g = 1_a \otimes g \circ f \otimes 1_d for all f:abf : a \to b and g:cdg : c \to d. Diagrams in the free rigid monoidal category can be seen as monoidal diagrams quotiented by the snake equations. In practice, these quotients are computed by calling Diagram.normal_form.

Diagrams are equipped with an involution Diagram.dagger that implements dagger categories. Furthermore, formal sums of diagrams can also be composed and tensored, making all the diagams enriched in monoids. DisCoPy also implements the syntax for diagrams in the free cartesian monoidal category and biclosed monoidal category, although their normal form is not yet implemented.

Monoidal functors

Diagrams can be evaluated in concrete monoidal categories by applying Functor instances to them.

Let :MonSigMonCat\mathcal{F} : \text{MonSig} \to \text{MonCat} be the functor that sends a monoidal signature to its free monoidal category, and its right adjoint 𝒰:MonCatMonSig\mathcal{U} : \text{MonCat} \to \text{MonSig} the forgetful functor. From the free-forgetful adjunction, we get that monoidal functor F:(Σ)SF : \mathcal{F}(\Sigma) \to S from a free monoidal category generated by a signature Σ\Sigma into some monoidal category SS is uniquely defined by a morphism of signature F:Σ𝒰(S)F : \Sigma \to \mathcal{U}(S). That is, in order to define a functor F:(Σ)SF : \mathcal{F}(\Sigma) \to S, it’s enough to define two mappings F 0:Σ 0Ob(S)F_0 : \Sigma_0 \to \text{Ob}(S) and F 1:Σ 1Ar(S)F_1 : \Sigma_1 \to \text{Ar}(S) which commute with dom\text{dom} and cod\text{cod}.

Concretely, a DisCoPy functor is defined by F = Functor(ob, ar) where ob and ar are mappings from generating object to types and from box to diagram respectively. These mappings can be either given as Python dictionaries if they have finite domains or as Python functions otherwise. Once its image for each generating object and each box is given, F can be applied to arbitrary diagrams. Optional arguments ob_factory and ar_factory can be used to define functors with arbitrary categories as codomain. By default DisCoPy functors are endofunctors from the free category to itself, i.e. they send diagrams to diagrams.

Currently, DisCoPy implements strong monoidal functors into:

Natural language processing

Diagrams can be used to encode derivations in a formal grammar. Indeed, the first use case of DisCoPy was to apply monoidal diagrams to these grammar diagrams in order to compute their semantics. Currently, DisCoPy can handle the following frameworks: