Law diagrams
The laws proarrow states as code, drawn as string diagrams. Each law is an equation between two ways of building an arrow, and each picture draws both sides exactly as the law builds them, without simplifying either one. So where a law says two different constructions agree, you see two different pictures next to each other.
The object variables of a law are single wires, labelled a to e, and the arbitrary arrows a law asks for are boxes with the names the law gives them. In the profunctor sections at the end, the elements a law is about are shaded boxes named p, p′ and p″ and the wires go up to f. Copying and merging are drawn as points, a dual wire is drawn hollow and labelled with ⁻¹, the unit is a dotted wire labelled I, and a trace is a loop round the side.
The pictures are made by Proarrow.Tools.Diagrams.Svg, which lays each diagram out from how it is built: a tensor puts its sides next to each other, a composite stacks them with a band of wires in between, and a trace draws its loops. Some sections are drawn with options that show more of the structure; the code under each heading says which.
Category · Monoidal · Symmetric monoidal · Traced · *-autonomous · Closed · Isomix · Compact closed · Monoids · Comonoids · Copy and discard · Frobenius · Monoidal profunctor · Strong · Costrong
Identities are units for composition, which is associative. Drawn with explicit identities, so each id is a dashed frame; associativity draws the same on both sides, as a string diagram does not record how a composite was bracketed.
lawSvgsWith @'[CategoryOf] defaultOptions{explicitIdentities = True}
left identity
|
right identity
|
associativity
|
Unitors and associator are invertible and natural, the tensor is a bifunctor, and the triangle and pentagon commute. Drawn with explicit coherence. The unit is a wire of its own, drawn dotted and labelled 𝐈, so a unitor is a unit wire running into another wire or out of it. The associator is drawn with brackets: at the top the pair grouped in its input, at the bottom the pair grouped in its output. Without explicit coherence, both sides of these laws draw the same. Tensor interchange draws the same either way: that string diagrams do not tell the two apart is what the law says.
lawSvgsWith @'[Monoidal] defaultOptions{explicitCoherence = True}
leftUnitor left inverse
|
leftUnitor right inverse
|
rightUnitor left inverse
|
rightUnitor right inverse
|
associator left inverse
|
associator right inverse
|
tensor identity
|
tensor interchange
|
leftUnitor naturality
|
leftUnitorInv naturality
|
rightUnitor naturality
|
rightUnitorInv naturality
|
associator naturality
|
associatorInv naturality
|
triangle identity
|
pentagon identity
|
The swap undoes itself, is natural, and satisfies the hexagon. Drawn with explicit swaps, so each swap is a crossing of its own; without them, a swap only moves wires and most of these draw the same.
lawSvgsWith @SymMonoidalStructures defaultOptions{explicitSwaps = True}
swap self-inverse
|
swap naturality
|
hexagon identity
|
The trace of f over u feeds its u output back to its u input, drawn as a loop round the side. It is natural in the other wires, slides along the loop, is trivial over the unit and nests over a tensor, lets a wire run past, and turns a swap into a plain wire. Drawn with explicit coherence, so the trace over the unit is a dotted loop and the regroupings the nested traces need show as brackets.
lawSvgsWith @TracedStructures defaultOptions{explicitCoherence = True}
naturality
|
sliding
|
vanishing (unit)
|
vanishing (tensor)
|
superposing
|
yanking
|
Duals and linear distribution. The dual of a wire is a wire of its own, labelled with ⁻¹ and drawn hollow. A wire is bent with a cup or a cap, drawn as one bend: the half that runs backwards is the dual wire, and the style switches at the apex. Double negation is only a relabelling here, so its inverse laws are straight wires; the definition law compares it with the one derived from linDist and the duality unit.
lawSvgs @StarAutonomousStructures
dual identity
|
dual composition
|
linDist naturality
|
dual left inverse
|
dual right inverse
|
linDist left inverse
|
linDist right inverse
|
doubleNegInv definition
|
doubleNeg left inverse
|
doubleNeg right inverse
|
Currying and apply. The exponential is the *-autonomous one, the dual of a ⊗ b⁻¹, so curry bends a wire round, and the part running backwards is a dual wire.
lawSvgs @ClosedStructures
curry left inverse
|
curry right inverse
|
curry naturality
|
internal hom on arrows
|
The unit of par is isomorphic to the unit: dualUnit and its inverse are drawn as a relabelling of the unit wire, so both inverse laws are empty diagrams. The duality counit joins a dual and its wire into the unit, drawn as one bend; its definition law compares it with the one derived from the *-autonomous structure, which goes into the unit of par first.
lawSvgs @IsoMixStructures
dualUnit left inverse
|
dualUnit right inverse
|
dualityCounit definition
|
The dual distributes over the tensor, and the zigzag identities hold, with the duality unit and counit drawn as one bend each, so a zigzag is a wire bent up and down again, dual on its middle stretch. The definition law compares the unit with the one derived from the *-autonomous structure; the counit comes from the isomix structure.
lawSvgs @CompactClosedStructures
distribDual left inverse
|
distribDual right inverse
|
dualityUnit definition
|
zigzag (a)
|
zigzag (Dual a)
|
Every object is a monoid: the unit point is a unit for the merge point, which is associative, and commutative when the monoids are commutative ones. The unit laws are drawn with explicit coherence, so they show the unitor they equal.
lawSvgsWith @'[Monoidal, Supplies Monoid] defaultOptions{explicitCoherence = True}
lawSvgs @'[Monoidal, SymMonoidal, Supplies CommutativeMonoid]
left unit
|
right unit
|
associativity
|
commutativity
|
Every object is a comonoid: the discard point is a counit for the copy point, which is coassociative, and cocommutative when the comonoids are cocommutative ones. The counit laws are drawn with explicit coherence.
lawSvgsWith @'[Monoidal, Supplies Comonoid] defaultOptions{explicitCoherence = True}
lawSvgs @'[Monoidal, SymMonoidal, Supplies CocommutativeComonoid]
left counit
|
right counit
|
coassociativity
|
cocommutativity
|
A copy-discard category copies and discards with its supplied comonoids, and these respect the tensor: copying or discarding a pair is copying or discarding both parts, and on the unit they do nothing. Drawn with explicit coherence, so the unit wire and the regrouping show.
lawSvgsWith @CopyDiscardStructures defaultOptions{explicitCoherence = True}
copy is comult
|
discard is counit
|
copy of a tensor
|
discard of a tensor
|
copy of the unit
|
discard of the unit
|
The monoids and comonoids together are special Frobenius algebras: a copy then a merge is the identity, and the Frobenius law holds. These are the spiders that make every other bend here work.
lawSvgs @FrobeniusStructures
speciality
|
Frobenius (left)
|
Frobenius (right)
|
A monoidal profunctor puts elements side by side with **, with one as its unit. The unit laws and associativity hold up to the unitors and the associator, and ** is natural. The profunctor is drawn as the identity profunctor on diagrams, so an element is a shaded box. Drawn with explicit coherence.
proLawSvgsWith @MonoidalProfunctor defaultOptions{explicitCoherence = True}
left unit
|
right unit
|
associativity
|
** naturality
|
Strength for the tensor: act puts a wire next to an element. Acting with the unit or with a tensor is the unitor or the associator, act is natural in the element, and an arrow on the extra wire can go above the element or below it. Drawn with explicit coherence.
proLawSvgsWith @(Strong Tensor) defaultOptions{explicitCoherence = True}
act unit
|
act tensor
|
act naturality
|
act dinaturality
|
Costrength for the tensor: coact feeds wires of an element back as a loop, as a trace does. An element with tensored ends is made from p with arbitrary arrows g and h around it. Coacting is natural, an arrow slides along the loop, and coacting with the unit or with a tensor is trivial or nests. Drawn with explicit coherence.
proLawSvgsWith @(Costrong Tensor) defaultOptions{explicitCoherence = True}
coact unit
|
coact tensor
|
coact naturality
|
coact sliding
|