A finite span with apex x hidden existentially.

The apex must be Eq so that pullback composition is computable. Unlike the relation view, the apex is part of the value: two spans with the same boundary relation but different apexes are different spans. This is the "residual remembered on the nose" rung of the ladder.

Forget the apex and return the boundary pairs.

The companion of a function: its graph read forward.

companion xs f is the span A ←id— A —f→ B.

The conjoint of a function: its graph read backward.

conjoint xs f is the span B ←f— A —id→ A.

Pullback composition of spans. The new apex is the set of pairs that agree on the shared boundary.

The identity span on a finite type, given by its enumeration.

Present a span as its own two legs: ⟨s,t⟩ = s* ⊙ t_*.

The result has the same boundary pairs as the original, but its apex is the diagonal pulled back along identity — the same span up to apex isomorphism, never up to quotient.

Does a span 2-cell from the first span to the second exist?

A 2-cell is an apex map h with a . h = s and b . h = t. Over finite enumerations such an h exists exactly when every boundary pair of the source occurs in the target, so existence is decidable from the pairs view alone — no access to the apexes required.

This is the existence statement; checking a given witness needs the apexes and lives with the caller that built them. The gap between the two is the ladder: refinesS is what the Rel rung can see, and it is strictly less than the Span rung, which distinguishes non-isomorphic apexes with the same pairs.

>>> let p = Span [1 :: Int, 2] id id :: Span Int Int
>>> let q = Span [1 :: Int, 2, 3] id id :: Span Int Int
>>> (refinesS p q, refinesS q p)
(True,False)

Directed Hausdorff distance between two spans over a common boundary:

  d((s,t),(a,b)) = sup_x inf_y [ d(s x, a y) + d(b y, t x) ]

The sup ranges over the domain apex and the inf over the codomain apex. Those are not two spellings of the same thing: in ([0,∞], ≥)-enrichment limits are suprema and colimits are infima, so the sup is the end and the inf is the coend. This function is therefore the general ∫_x ∫^y shape made concrete, not merely a metric analogue of it — which is also why it cannot be written in a bare semiring: for the tropical scalar the inf is the semiring addition but the sup belongs to the dual semiring.

The two units are the degenerate cases and must be supplied:

• bot is the value of a sup over an empty domain apex (0 for a tropical scalar) — a span with no apex points is distance bot from anything;
• top is the value of an inf over an empty codomain apex (+∞) — nothing can be approximated by a span with no apex points.

Passing them explicitly is what keeps this total; folding with maximum and minimum would throw on either empty enumeration.

>>> let dist x y = abs (fromIntegral x - fromIntegral y) :: Double
>>> let sA = Span [0 :: Int, 1] id id
>>> let sB = Span [0 :: Int] id id
>>> spanDistance 0 (1 / 0) (+) dist dist sA sA
0.0
>>> spanDistance 0 (1 / 0) (+) dist dist sA sB
2.0

The empty codomain apex is total, not an exception:

>>> spanDistance 0 (1 / 0) (+) dist dist sA (Span ([] :: [Int]) id id)
Infinity