A wire: a labelled wire, the dual of one, or the unit wire.

The dual of a wire. The unit wire is its own dual.

The duals of the wires.

The labels of the wires that carry something: the unit wires left out, and a dual wire labelled as the wire it is the dual of.

A wire whose label is known. The methods are facts about DualW and Erase that hold for each kind of wire, from which withIsListDual, withIsListErase, withEraseAppend, withDualDual and withEraseDual prove them for lists by induction.

The duals of a list of wires are a list of wires.

The erased wires of a list of wires are a list of labels.

Erasing commutes with appending.

Dualising twice gives the wires back.

Dualising commutes with appending.

The duals of wires erase to the same labels as the wires.

The labels of the wires of ws as they are shown, and their kinds.

A diagram: its meaning, as a Dot diagram on the erased wires, and how it was built, which is drawn when it is rendered.

A diagram from its meaning, which may use that the erased wires are lists, and how it is drawn.

A diagram that means the identity on the erased wires, drawn as given.

An arrow between wires that erase to the same labels, a wire and its dual for example: in meaning the identity. It is drawn as nothing, the wires carrying on in the style of their new kinds.

Choices about what to draw.

Nothing drawn that the meaning does not need, legs in order.

The meaning of a diagram, forgetting how it is drawn.

Wires with a unit wire on the right are a list, and erase to the same labels.

An associator, from the given grouping to the other one.

A wire bent upwards, a on the left and its dual on the right. It means cup, and is drawn as one bend that turns into the dual at its apex.

A wire bent downwards, the dual of a on the left and a on the right. It means cap, and is drawn as one bend that turns into the dual at its apex.

dualCup as a strictified arrow. The *-autonomous structure is built from it, not from the compact closed dualityUnit, so that the laws relating the two compare different definitions.

dualCap as a strictified arrow.

A box with the given name, its inputs along the top and its outputs along the bottom, each output labelled with its wire.

A wire, the identity on it.

A crossing of fixed height. A plain swap is drawn as a crossing too, but in the band where the wires next change position.

The unit of an adjunction, drawn as a box named η.

The counit of an adjunction, drawn as a box named ϵ.

What kind of wire a wire is, which decides how it is drawn.

How a diagram was built. The options come in only when it is drawn: hideUnits takes out what explicitCoherence would show, and layout decides the rest.

The points a (co)monoid is drawn with.

Whether a bend opens downwards, a cup, or upwards, a cap.

Which pair an associator groups first: (a ⊗ b) ⊗ c or a ⊗ (b ⊗ c).

Which side of the other wires a unit wire joins them.

Whether a unitor ends a unit wire on another wire, or starts one from it.

The diagram with its unit wires left out, and its unitors and associators turned into wires carrying straight on.

The diagram laid out with the given options.

The boundary wires that are drawn with the given options.

A point in the plane, y growing downwards.

The course of a piece of wire.

What a diagram is drawn with.

A shape moved right by dx and down by dy.

Where a wire enters a drawing along its top or leaves it along its bottom: how far along, the kind of wire, and, for a leg of a copy or merge point that may trade places with the point's other leg, which point it is a leg of.

A port moved right by dx.

A drawn diagram: its size, its input and output ports, and its shapes.

How a diagram is drawn. A diagram that only permutes its wires has no height of its own: its crossings are drawn in the band where the wires next change position, so that a swap next to a box does not make the box taller.

The distance between neighbouring wires.

The length of wire above and below a box.

The height of a box.

The distance between the rails of neighbouring trace loops.

How far the innermost trace loop runs below and above the diagram it loops round, clear of the wire labels.

The width of a name, roughly, in the box font.

The positions of n wires, one slot apart.

Ports at the given positions, for wires of the given kinds.

A permutation of wires of the given kinds, drawn over the given height.

Straight wires of the given kinds at the given positions, from the top down to h.

A layout as geometry, a permutation drawn over the given height.

Geometry made taller, centred, with its wires extended to the new top and bottom.

Two layouts side by side, as tall as the taller one.

The layout of after . before. A permutation is absorbed into the layout next to it, so its crossings end up in the next band.

before above after, with a band of wires between them. The two are placed so that the wires between them move sideways as little as possible.

Ports with the legs of each point that may trade places reordered, so that they run to their targets without crossing each other.

The height of a band whose wires move sideways by at most d.

A box with inputs of the given kinds, and outputs with the given labels and kinds. Unit wires get no label.

The points of a (co)monoid, one on each wire of the given kinds; nothing drawn when there are no wires. The legs of copy and merge points may trade places when free.

The height of a swap drawn on its own.

A permutation of wires of the given kinds, drawn on its own when explicit.

The identity on wires of the given kinds, drawn in a dashed frame when explicit.

Bends joining each wire of the given kinds to its dual: for a Cup the wires and then their duals leave along the bottom, for a Cap the duals and then the wires enter along the top. Each bend changes style at its apex.

An associator from the grouping given to the other one, on wires of the given kinds: the wires with a bracket over the pair grouped at the top and one under the pair grouped at the bottom.

A unitor on wires of the given kinds: a dotted unit wire that runs into the outermost wire on its side or out of it.

The end of a unit wire.

Geometry upside down: its inputs become its outputs and the other way round, so that a merge point becomes a copy point, a cup a cap, and so on. A point is filled when it was hollow and hollow when it was filled, as the points of a comonoid are the mirror images of a monoid's. A piece of wire still runs from top to bottom, except a bend's, which runs towards its apex.

The first k wires fed back from the outputs to the inputs, each looping round the side where it crosses fewer other wires. The loops on one side are nested: the one whose ends are nearest that side runs innermost.

The height of the row of boundary labels.

Geometry with its boundary: the input labels above and the output labels below, each joined to its wire by a band top and bottom tall. Legs that may trade places are put in the boundary's order.

The positions of ports, the legs of each point that may trade places put in the order of the wires.

The height of the bands joining the boundary to the wires.

The diagram as an SVG document, with the defaultOptions.

The diagram as an SVG document.

Two parallel diagrams side by side, with an equals sign between them, with the defaultOptions.

Two parallel diagrams side by side, with an equals sign between them. Neither is simplified: the picture shows two different diagrams that mean the same.

Diagrams from the wires as to the wires bs as one SVG document: side by side, each with the boundary labels, stretched to the height of the tallest, and with an equals sign between each and the next.

The laws of cs drawn with the defaultOptions, see lawSvgsWith.

The laws of cs, each drawn as an equation by renderEquationWith, with its name. The object variables are single wires Wire "a" to Wire "e", and the arrows a law asks for are nodes with the names it gives them.

An SVG document showing the geometry. Wires, outlines and text use the current colour. Boxes are not filled, and the wires stop at the edge of a hollow point, so the background shows through both. Only the core of a dual wire is painted, in --sd-paper (white when it is not set), which a page can set to its background.

Where a piece of wire starts and ends, and the SVG path from its start.

Pieces of wire joined where one ends where the next starts, each chain as one path. A chain starts at a piece that no other piece leads into.

One shape as SVG.

How far along its tangent a cubic curve's control point lies, as a fraction of the radius, for the curve to be a quarter circle.

The radius of a bend, and of the corners of a trace loop, so that a small loop is a cup and a cap joined by straight wire.

A path from the first of the given corners along the rest, each corner rounded with a quarter circle of radius bendRadius, or less where the wire on either side of it is too short. A stretch of wire between two corners is shared between them; one at either end belongs to its corner alone.