Provenance. Both texts derived from
scip://discopy— 90 docs · 7,800 defs · 38,901 occurrences — each line carrying its symbol-graph anchor (in parens, linked to the DisCoPy documentation where documented, to source where not). The index holds counts and symbols; the shaping is interpretation — but every line is bound to a measurement actually run. Two measured gaps, kept visible:is_implementationedges came back empty (scip-python cannot see through the@factory/generics machinery), so the doctrine lattice below stands on the module set, not resolved inheritance; and the docs place some symbols differently than the source does (Composableis defined inutils.py, documented underdiscopy.cat) — both names are real, the links follow the docs.
Everything is composition; dom and cod are the only universal truths.
(Composable#dom ×384, Composable#cod ×376 — the two most-referenced symbols in the library)
Two operations suffice: then (>>) and tensor (@).
(the only two core mixins: cat.Composable, monoidal.Whiskerable)
Each axiom earns its own module; structure is opt-in, never assumed.
(24 doctrine submodules: cat ⊂ monoidal ⊂ braided ⊂ symmetric … markov, frobenius, compact, rigid)
A diagram is syntax; a functor is meaning.
(Functor(ob, ar, cod) — the universal map; semantics is functor application)
The category is a parameter, passed by factory.
(@factory ×62, factory_name ×71, ty_factory — the doctrine is injected, not hardcoded)
Types are checked, never trusted.
(utils.assert_isinstance ×106 — the substructural discipline)
An equation is an axiom; to break it is an error, by name.
(utils.AxiomError ×60 — equality failures are first-class, named)
Only connectivity matters.
(discopy.hypergraph — the combinatorial core where structural laws dissolve into isomorphism)
Equality is decided by normalization, doctrine by doctrine — and only as far as each doctrine reaches.
(Diagram.normal_form yanks the snake but not the swap: partial, per-doctrine completeness)
The runtime is just another category; semantics is a functor into python.
(discopy.python.Function as a codomain — the model we ran everything in)
What a category lacks defines it as much as what it holds.
(no discopy.cartesian module; python.Function has copy/discard/trace, lacks cup/cap/merge)
And when in doubt — draw it.
(drawing.Node ×84, drawing.Point — drawing is a first-class citizen; every diagram .draw()s)
i. The category that can be named is not the eternal category.
The free diagram is nameless; only the functor gives it a name —
and a different functor gives it another.
(one box if 0 1 2; three functors; 2 / 1 / ERROR)
ii. Syntax and meaning are not two.
A functor turns the one into the other and keeps all that must be kept.
This keeping is the Way; it adds nothing, forgets nothing it owes.
(functoriality: F(d₁>>d₂) = F(d₁)>>F(d₂) — the only law)
iii. Sameness is what every functor preserves. Difference hides — in the functor, or in the wire. Pursue it into the functor and it becomes undecidable; pull it into the wire and it becomes a knot you can see. (difference is semantic-and-undecidable, or topological-and-drawn)
iv. Reversal is the movement of the Way.
Bend a wire through its dual and it returns straight;
the way out and the way back are one wire.
(the snake yanks to Id — verified by normal_form)
v. Thirty spokes share one hub; the use is in the emptiness.
The runtime has no merge, no cup, no cap.
In what it cannot form, it is exactly itself.
(python.Function: copy/discard/trace, never Frobenius nor compact)
vi. The hard is born from the soft.
Where no wire joins them, two acts have no order.
Thread the runtime through both and order is born — and cannot be undone.
(pure f@g is order-free; the control wire makes it premonoidal)
vii. What is pure cannot be seen, only declared. You may watch a morphism forever and not know it is central; you mark it, and trust the mark. The named pure is not the eternal pure. (purity is undecidable black-box; effectful categories choose the centre)
viii. Do not decree the verdict; read it off the step. The Way conserves the balance, it does not chase it. A trit you assign is decoration; a trit you measure can be wrong — and only what can be wrong is true. (GF(3) measured, never assigned; Σ≡0 conserved, not maximized)
ix. There is no floor. Python is not the ground beneath the diagram; it is one more category, a place the functor happens to land. (the runtime is a codomain like any other)
x. The Dao that yanks straight leaves no trace of the bend. When the work is done and the diagram drawn, the scaffolding is gone: what remains is a wire, and you cannot tell it ever curved. (the certificate, when sound, vanishes into the result)
The Zen is the ten thousand things; the Dao is the one functor they are all images of. Equivalence is what survives every map; everything else is either a knot you can draw or a question you must run.