Phantom polarity pair. IN ap am is the Int object with forward face ap and backward face am.

A morphism in the Int construction from (ap, am) to (bp, bm) over a traced monoidal base category.

The underlying arrow runs from the forward input plus the backward output (t ap bm) to the backward input plus the forward output (t am bp).

Identity in Int is the symmetry that swaps the two factors.

>>> let i = id :: IntMorph (,) (->) Int Bool Int Bool
>>> runIntMorph i (1, False)
(False,1)

Composition in the Int construction.

Tensor the two base morphisms, reassociate the four factors so the middle pair (bm, bp) sits on the feedback wire, and close it with trace. The result is again a single base arrow arr (t ap cm) (t am cp).

Nontrivial composition over Trace (,) (->). Both morphisms transform both legs; the middle trace closes the feedback loop. The chosen bodies are lazy in the feedback component so the lazy (,) knot stays productive. Hand-computed: input (4, 1) gives output (5, 2).

>>> let f = IntMorph (base (\(a, _) -> (a + 1, a))) :: IntMorph (,) (Trace (,) (->)) Int Int Int Int
>>> let g = IntMorph (base (\(_, c) -> (c, c + 1))) :: IntMorph (,) (Trace (,) (->)) Int Int Int Int
>>> eval (runIntMorph (g `comp` f)) (4, 1)
(5,2)

The composite over Trace inherits the one-Yank normal form: the inner plumbing is absorbed into a single yank over one base arrow.

>>> if isYank (runIntMorph (g `comp` f)) then "one-Yank" else "not one-Yank"
"one-Yank"

Dual of an Int morphism: swap the polarities of domain and codomain.

The underlying arrow is pre- and post-composed with the symmetry so that the types line up: arr (t bm ap) (t bp am).

>>> let f = IntMorph (\(a, d) -> (a * 2, d + 1)) :: IntMorph (,) (->) Int Int Int Int
>>> runIntMorph (dual f) (5, 1)
(6,2)

Tensor product of two Int morphisms.

On objects this is componentwise: (ap, am) u2297 (cp, cm) = (t ap cp, t am cm). On morphisms it threads the two base arrows side-by-side and reassociates the factors into the required arr (t (t ap cp) (t bm dm)) (t (t am cm) (t bp dp)) shape.

Cap (unit introduction) for Int(->) at object IN a b.

The unit object is IN () (); the cap produces the tensor IN (a, b) (b, a).

Cup (unit elimination) for Int(->) at object IN a b.

Left-unitor for Int(->): I u2297 A -> A.

Inverse left-unitor for Int(->): A -> I u2297 A.

Right-unitor for Int(->): A u2297 I -> A.

Inverse left-unitor for Int(->): A -> I u2297 A.

Associator for Int(->): A u2297 (B u2297 C) -> (A u2297 B) u2297 C.

Inverse associator for Int(->): (A u2297 B) u2297 C -> A u2297 (B u2297 C).

Inverse associator used in the left yanking equation for IN a b.

Symmetric braiding for Int(->): A u2297 B -> B u2297 A.

Yanking witness. In the Int construction the identity is the swap on the two factors; tracing that swap over the Either tensor returns the input unchanged.

>>> let i = id :: IntMorph Either (->) Int Int Int Int
>>> trace (runIntMorph i) (42 :: Int)
42

Mat Bool middle trace with coupled blocks. The feedback channel is Bool, the aa block is the swap (so its reflexive-transitive closure is the universal relation on Bool), and the off-diagonal ba/ac blocks are non-constant. The helper below repeats the same parT + slide + trace-middle wiring as comp, but specialised to the Mat/Either setup so the doctest can live in the finite-type setting.

>>> let aa = mat (\a a' -> a /= a') :: Mat Bool Bool
>>> let acF = mat (\a c -> a && c) :: Mat Bool Bool
>>> let baF = mat (\b a -> b && a) :: Mat Bool Bool
>>> let bcF = mat (\_ _ -> False) :: Mat Bool Bool
>>> let mF = mat (\x y -> case x of { Left a -> case y of { Left a' -> a /= a'; Right c -> a && c }; Right b -> case y of { Left a' -> b && a'; Right _ -> False } })
>>> let f = IntMorph mF :: IntMorph Either Mat Bool Bool Bool Bool
>>> let acG = mat (\_ c -> c) :: Mat Bool Bool
>>> let baG = mat (\c b -> c || b) :: Mat Bool Bool
>>> let mG = mat (\x y -> case x of { Left b -> case y of { Left b' -> b /= b'; Right c -> c }; Right c -> case y of { Left b' -> c || b'; Right _ -> False } })
>>> let g = IntMorph mG :: IntMorph Either Mat Bool Bool Bool Bool
>>> runMat (runIntMorph (compMatEither g f)) (Right False) (Right False)
False
>>> runMat (runIntMorph (compMatEither g f)) (Right False) (Right True)
True
>>> runMat (runIntMorph (compMatEither g f)) (Right True) (Right False)
False
>>> runMat (runIntMorph (compMatEither g f)) (Right True) (Right True)
True

Include a Poly monomial lens as an Int morphism over (->).

A monomial Mono da a is the Int object IN a da: forward face a, backward face da. A lens Morphism (Mono da a) (Mono db b) carries a forward pass a -> b and a backward pass a -> db -> da; causal packs them into the single joint map (a, db) -> (da, b) that an IntMorph demands.

This is the causal fragment: the forward output b is read from a alone, never from the backward input db. The image therefore carries no feedback — composing two causal images under comp leaves the middle trace with nothing to close, so the knot is trivial.

>>> let l1 = dagger (+10) (*2) :: Morphism (Mono Int Int) (Mono Int Int)
>>> runIntMorph (causal l1) (100, 3)
(6,110)

The forward face ignores the backward input — feeding two different backward values leaves the forward output b fixed at 110:

>>> [ snd (runIntMorph (causal l1) (100, db)) | db <- [3, 99] ]
[110,110]

Point-dependent lenses cross too: lens show (\n d -> n + d) at 40 gives forward "40" and backward 40 + 2 = 42.

>>> let l2 = lens show (\n d -> n + d) :: Morphism (Mono Int Int) (Mono Int String)
>>> runIntMorph (causal l2) (40, 2)
(42,"40")

Trivial knot under composition. Take causal into the Trace base and compose two images with comp. Composition ties a Yank (the middle trace fires) — yet the observed value equals plain lens Compose under the polarity swap, because the causal fragment feeds nothing back through the loop. The knot is tied and does nothing: pullback magnitude of the trace is zero here.

>>> let cz (m :: Morphism (Mono xd x) (Mono yd y)) = IntMorph (base (\(a, db) -> let (b, put) = applyLens m a in (put db, b))) :: IntMorph (,) (Trace (,) (->)) x xd y yd
>>> let f = dagger (+1) (*2) :: Morphism (Mono Int Int) (Mono Int Int)
>>> let g = dagger (*10) (+5) :: Morphism (Mono Int Int) (Mono Int Int)
>>> let (b, put) = applyLens (Compose g f) 7 in (b, put 100)
(80,210)
>>> eval (runIntMorph (comp (cz g) (cz f) :: IntMorph (,) (Trace (,) (->)) Int Int Int Int)) (7, 100)
(210,80)
>>> if isYank (runIntMorph (comp (cz g) (cz f) :: IntMorph (,) (Trace (,) (->)) Int Int Int Int)) then "Yank (tied, trivial)" else "Lift (no knot)"
"Yank (tied, trivial)"