Promoted description of a polynomial as a span Dir -> Pos.

Unlike Poly, this grammar does not need a position-indexed Dir family; the projection is supplied by the SpanC class at the term level.

CComp is in the grammar but outside the span fragment: it has a netlist view, but no span projection. See SpanC and the module header.

Position set of a span polynomial.

Total direction space of a span polynomial.

For CProd, the total direction space includes the other position so that the projection to the product of positions is a pure function. In the double-category picture this is the universal property of the product of spans.

Values of a span polynomial functor evaluated at x.

ETC stores the tensor netlist directly: a pair of positions and a curried direction function. This is not structural like ESC or EPC, and it makes the tensor round-trip exact in the spike. See the module header.

Span polynomials: those constructors that admit a projection Dir -> Pos.

CComp is deliberately not an instance. A single direction (dp, dq) does not determine the hang map DirC p -> PosC q, so there is no function DirC (CComp p q) -> PosC (CComp p q) to write. This is a mathematical impossibility, not a Haskell limitation; it is documented at the type level by the missing instance.

Test whether a direction lies in the fibre of a given position.

This is the lowest-dimensional fibre law, equivalent to the Beck–Chevalley condition for the identity cell.

Polynomials that admit a netlist view in the span encoding.

The netlist view is EvalC p x ≅ (PosC p, DirC p -> Maybe x), where Nothing means "outside the fibre of the chosen position".

fromNetC assumes the supplied function respects the fibre. If it returns Nothing on a direction that is inside the fibre, fromNetC raises an internal error: that is the encoding's assertion of the Beck–Chevalley condition, not user-facing junk.

Every constructor is an instance, including CComp, because a value of any constructor can be stored together with its position and direction function. CComp is not a SpanC, so its netlist view is not a span netlist view.

Reassemble a value after taking it apart.

This is the executable form of the round-trip law fromNetC (toNetC v) ≡ v. It is exact for every constructor. The reverse direction toNetC (fromNetC i h) ≡ (i, h) holds exactly when h respects the fibre, and fails otherwise.

Left distributivity of CProd over CSum: CProd (CSum p q) r -> CSum (CProd p r) (CProd q r).

Right distributivity of CProd over CSum: CSum (CProd p r) ('CProd q r) -> CProd (CSum p q) r.

Position isomorphism for the left distributivity of CProd over CSum.

Direction isomorphism for the left distributivity of CProd over CSum.

Composition-product view of a nested span evaluation.

Correctness iso (right): EvalC p (EvalC q x) ≅ EvalC (CComp p q) x.

This is the span analogue of nestedToComp, but it works through the Maybe netlist view. Off-fibre directions in the outer polynomial have no canonical q-position, so the hang map is only defined on the fibre; this is the same cube boundary as the missing SpanC instance for CComp.

Nested span evaluation from a composition-product value.

Correctness iso (left): inverse of nestedToCompC.

Left associator for the composition product: ((p ◁ q) ◁ r) -> (p ◁ (q ◁ r)).

Right associator for the composition product.