diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,25 @@
+# Revision history for circuits
+
+## 0.1.0.0 — 2025-05-26
+
+- Initial release (not yet published to Hackage).
+- **Circuit** — GADT: Lift, Compose, Knot. Free traced monoidal category with Profunctor instance.
+- **Hyper** — final coinductive encoding. Category, Profunctor, Functor instances. Feedback dissolves into the type.
+- **Trace** class with `(,)` (lazy knot) and `Either` (iteration) tensors. `Trace (Kleisli IO) Either` via delimited continuations.
+- Triangle identity: `reify = lower . encode`. `flatten` for the reverse direction (lossy).
+- `ambient` / `ambientBy` — state wire threading through feedback loops.
+- Cocartesian combinators in `Circuit.Monoidal`: `coassoc`, `coassoc'`, `coseed`, `coabsorbL`, `coabsorbR`, `coreleaseL`, `coreleaseR`.
+- `Braided` class with instances for `(,)` and `Either` — merged with cartesian/cocartesian structure into `Circuit.Monoidal`.
+- `cellIO` — stateful `Kleisli IO` arrow via `IORef` for strict accumulators in `(,)`-traced pipelines.
+- Removed `Circuit.Queue` and `these` dependency — consolidated into `circuits-io`.
+- Removed `Iter`/`loopIter` — duplicates `Trace (Kleisli m) Either`.
+- Canonical API uses lowercase names: `lift`, `lower`, `reify`, `encode`, `push`, `run`, `trace`, `untrace`.
+- Notation conventions in `other/symbols.md`. No `Circuit.Symbols` module — symbols are prose notation, not Haskell identifiers.
+- Narrative arc in `other/`: marks → GADT → Hyper → tensors → Mendler case → making stuff.
+- 15+ example cards: parsers, pipes, while-loops, Elgot iteration, delimited continuations, proequipment, ambient, hyper-chain, state, pure-queue, etc.
+- Boundary rule: symbols in tables/axioms only; names everywhere else.
+- `Step` convention unified with `Trace (->) Either`: `Left` = feedback, `Right` = exit.
+- Push is Hyper-only — no direct GADT counterpart.
+- Axiom doctests and QuickCheck properties for JSV laws and Hyper embedding/functoriality.
+- No Applicative or Monad instances — these collapse feedback structure.
+- README: tank mode, Hackage/CI badges, paper link.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+Copyright (c) 2026
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived
+   from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS
+OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED
+AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF
+THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGE.
diff --git a/circuits.cabal b/circuits.cabal
new file mode 100644
--- /dev/null
+++ b/circuits.cabal
@@ -0,0 +1,68 @@
+cabal-version: 3.0
+name: circuits
+version: 0.1.0.0
+license: BSD-3-Clause
+license-file: LICENSE
+copyright: Tony Day (c) 2025
+category: control
+author: Tony Day
+maintainer: tonyday567@gmail.com
+homepage: https://github.com/tonyday567/circuits#readme
+bug-reports: https://github.com/tonyday567/circuits/issues
+synopsis: traced categories and circuits
+description:
+  circuits is a Haskell library that makes feedback first-class, by providing Circuit, the initial traced category over a base category, hyperfunctions via Hyper, and combinators and interpreters. It is experimental, but could be a promising approach to programming circuits that is intensional, ergonomic and performant.
+
+build-type: Simple
+tested-with:
+  ghc ==9.10.1
+  ghc ==9.12.2
+  ghc ==9.14.1
+
+extra-doc-files:
+    ChangeLog.md
+    readme.md
+    LICENSE
+    other/symbols.md
+    other/axioms.md
+
+source-repository head
+  type: git
+  location: https://github.com/tonyday567/circuits
+
+common ghc-options-stanza
+  ghc-options:
+    -Wall
+    -Wno-unused-imports
+    -Wcompat
+    -Widentities
+    -Wincomplete-record-updates
+    -Wincomplete-uni-patterns
+    -Wpartial-fields
+    -Wredundant-constraints
+
+common ghc2024-stanza
+  if impl(ghc >=9.10)
+    default-language:
+      GHC2024
+  else
+    default-language:
+      GHC2021
+
+library
+  import: ghc-options-stanza
+  import: ghc2024-stanza
+  hs-source-dirs: src
+  exposed-modules:
+    Circuit
+    Circuit.Circuit
+    Circuit.Classes
+    Circuit.Hyper
+    Circuit.Monoidal
+    Circuit.Traced
+
+  build-depends:
+    base >=4.18 && <5,
+
+  if impl(ghc)
+    build-depends: profunctors >=5.0 && <6,
diff --git a/other/axioms.md b/other/axioms.md
new file mode 100644
--- /dev/null
+++ b/other/axioms.md
@@ -0,0 +1,356 @@
+# Traced Monoidal Category Axioms
+
+**Summary:** Equational proofs for all five axioms, both tensors. For when
+you need to be sure.
+**Reference:** https://ncatlab.org/nlab/show/traced+monoidal+category
+**See also:** `02-a-knot-recovers-fix.md` (GADT derivation), `src/Circuit/Traced.hs` (Trace instances)
+
+The five Joyal–Street–Verity axioms proved for tensors `(,)` and `Either`
+over the base arrow `(->)`. Narrative motivation lives in the arc docs (01–07).
+
+## Preliminaries
+
+```haskell
+class Trace arr t where
+  trace   :: arr (t a b) (t a c) -> arr b c   -- close the channel
+  untrace :: arr b c -> arr (t a b) (t a c)   -- inject into channel
+```
+
+For `arr = (->)`:
+
+| Tensor | `trace` | `untrace` |
+|--------|---------|-----------|
+| `(,)` | `\f b -> let (a, c) = f (a, b) in c` | `fmap` / `second` |
+| `Either` | while-loop: `Left` continues, `Right` exits | `fmap` / `right` |
+
+The left-channel convention puts the channel on the left: `t a b` means
+channel `a`, payload `b`. So `id ⊗ f` means `first f` for `(,)` and
+`left f` for `Either` — both act on the channel component, leaving the
+payload untouched.
+
+The two tensors are operationally dual:
+
+- **`(,)`** ties a lazy knot — feedback and output co-occur in a single
+  recursive binding. Proofs reduce to substituting the knot.
+- **`Either`** runs a while-loop — `Left` re-enters, `Right` exits.
+  Proofs compare the reachable states of two state machines.
+
+Every axiom holds for both by the same logical structure, reached by
+different computational paths.
+
+## The Five Axioms
+
+**1. Vanishing.** Tracing over the unit does nothing. Nested channels
+trace in sequence.
+```
+(a) tr^I(f) = f           for f : A ⊗ I → B ⊗ I
+(b) tr^{X⊗Y}(f) = tr^X(tr^Y(f))   for f : A ⊗ X ⊗ Y → B ⊗ X ⊗ Y
+```
+
+**2. Sliding.** A morphism on the channel can slide from one side of `f`
+to the other inside the trace.
+```
+tr^X((id_B ⊗ g) ∘ f) = tr^Y(f ∘ (id_A ⊗ g))
+for f : A ⊗ X → B ⊗ Y,  g : Y → X
+```
+
+**3. Tightening.** Payload morphisms pass freely through the trace.
+```
+tr^X((g ⊗ id_X) ∘ f ∘ (h ⊗ id_X)) = g ∘ tr^X(f) ∘ h
+for h : A → B,  f : B ⊗ X → C ⊗ X,  g : C → D
+```
+
+**4. Strength.** An independent payload wire is invisible to the trace.
+```
+tr^X(g ⊗ f) = g ⊗ tr^X(f)
+for g : A → B,  f : C ⊗ X → D ⊗ X
+```
+
+**5. Yanking.** Tracing the braiding is the identity.
+```
+tr^X(swap_{X,X}) = id_X
+```
+
+Yanking is the only axiom that requires a braiding. The other four hold
+in any monoidal category with a trace.
+
+## Connection to the Hyperfunction Axioms
+
+Launchbury, Krstic & Sauerwein (2013) state six axioms for hyperfunctions.
+`push` is primitive — it prepends a function on the input side of the
+feedback channel. The six axioms reduce to three structural roles:
+
+| LKS Axiom | JSV Axiom | Structural role |
+|-----------|-----------|-----------------|
+| 1–3 | — | Free category (`Lift` + `Compose`) |
+| 4 | — | `run (lift f) = fix f` — fixed points of base arrows (Hasegawa Thm 3.1) |
+| 5 | — | Push composition: `push f p . push g q = push (f . g) (p . q)`. Push distributes over composition — a homomorphism constraint on the primitive. |
+| 6 | Sliding | Feedback (forces `Knot` constructor) |
+
+LKS axioms 1–5 have no direct JSV counterpart — LKS 1–3 fall out of the free
+category structure, LKS 4 (`run (lift f) = fix f`) follows from the Hasegawa fixpoint correspondence for base arrows,
+and LKS 5 (push composition) constrains how push interacts with composition.
+Only LKS 6 (sliding/feedback) maps cleanly to a JSV axiom.
+
+Axioms 4 and 5 introduce no new constructors on the final side. Axiom 4
+(`run (lift f) = fix f`) is the key property showing that fixed points of
+base arrows are available in the final encoding; it is part of the motivation
+for why the initial encoding needs the structure that `Knot` provides.
+Only axiom 6 (sliding) forces a new constructor on the initial side.
+See `02-a-knot-recovers-fix.md` for the derivation.
+
+## The Mendler Case
+
+In `Circuit`, the sliding axiom is reified as a pattern match in `reify`:
+
+```haskell
+reify :: (Category arr, Trace arr t) => Circuit arr t x y -> arr x y
+reify (Lift f)             = f
+reify (Compose (Knot f) g) = ↪ (f . ↩ (reify g))   -- Mendler
+reify (Compose f g)        = reify f . reify g
+reify (Knot k)             = ↪ k
+```
+
+The Mendler case must appear before the general `Compose` case. Without
+it, `Compose (Knot f) g` falls through to `trace f . reify g` — the
+naive form that closes the channel immediately, losing the feedback
+structure. One pattern match separates a free traced monoidal category
+from the degenerate model. For the full story see `02-a-knot-recovers-fix.md` and
+`05-no-remorse-once-removed.md`.
+
+## Proofs
+
+### Axiom 1: Vanishing
+
+#### (a) Unit channel is a no-op
+
+**With `(,)` — unit `I = ()`.**
+
+A morphism `f :: ((), a) -> ((), b)` is, under the unit isomorphism,
+`f = \((), x) -> ((), g x)` for some `g :: a -> b`.
+
+```haskell
+trace f b
+  = let (a, c) = f (a, b) in c       -- Trace (->) (,) definition
+  = let ((), c) = f ((), b) in c     -- a :: ()
+  = let ((), c) = ((), g b) in c     -- definition of f
+  = g b
+  = trace (Lift g) b                  -- same as a plain Lift
+```
+
+The lazy knot has nothing to tie — `()` is determined immediately.
+
+**With `Either` — unit `I = Void`.**
+
+`Either Void a ≅ a` since `Left v` is uninhabited. A morphism
+`f :: Either Void a -> Either Void b` can only map `Right x` to
+`Right (g x)`.
+
+The while-loop enters at `Right b`. On each step, `f` returns either
+`Right c` (exit) or `Left v` — but `Left v` is uninhabited, so the
+loop terminates immediately at `g b`. The trace degenerates to plain
+function application.
+
+#### (b) Nested channels trace in sequence
+
+**With `(,)`.**
+
+`f :: ((x, y), a) -> ((x, y), b)`. Channel is `(x, y)`, payload is `a`.
+
+**LHS** — trace over `(x, y)` in one lazy knot:
+```haskell
+trace f a0 = let ((x, y), b) = f ((x, y), a0) in b
+```
+
+**RHS** — trace `y` first, then `x`. Reshape `f` via associativity:
+
+```haskell
+shuffle   (y, (x, a)) = ((x, y), a)
+unshuffle ((x, y), b) = (y, (x, b))
+f_Y = unshuffle . f . shuffle   -- channel y, payload (x, a)
+```
+
+Inner trace ties `y`, yielding a function of `(x, a0)`. Outer trace
+ties `x`. Both find the same fixed point: `((x, y), b) = f ((x, y), a0)`.
+Lazy evaluation makes the nested knots equivalent to the single knot.
+
+**With `Either`.**
+
+Channel is `Either a b`. LHS runs one while-loop over the state
+`Either a b`. RHS runs two nested loops (trace `b` first, then `a`)
+via associativity `Either (Either a b) c ≅ Either a (Either b c)`.
+Both reach the same exit state — nested state machines vs one.
+
+The `(,)` and `Either` traces are operationally dual: coinductive lazy
+knot vs inductive while-loop. Vanishing holds for both by the same
+logical structure, reached by different computational paths.
+
+### Axiom 2: Sliding
+
+`f :: (x, a) -> (y, b)`, `g :: y -> x`. Channel changes from `x` to `y`;
+`g` bridges them back.
+
+**With `(,)`.**
+
+LHS — apply `g` to the output channel, trace over `x`:
+```haskell
+trace (first g . f) a
+  = let (x, b) = (first g . f) (x, a) in b
+  = let (x, b) = let (y, b') = f (x, a) in (g y, b') in b
+  = let (y, b) = f (g y, a) in b             -- substitute x = g y
+```
+
+RHS — apply `g` to the input channel, trace over `y`:
+```haskell
+trace (f . first g) a
+  = let (y, b) = (f . first g) (y, a) in b
+  = let (y, b) = f (g y, a) in b
+```
+
+Both reduce to `\a -> let (y, b) = f (g y, a) in b`. The lazy knot ties
+`y` to `g y` from `f`'s output — the same fixed point either side.
+
+**With `Either`.**
+
+`f :: Either x a -> Either y b`, `g :: y -> x`.
+
+LHS — apply `g` to the output channel, trace over `x`:
+
+Enter at `Right b`. On step `s :: Either x a`, call `f s`:
+- `Right c` → exit with `c`
+- `Left y` → re-enter at `Left (g y)`
+
+RHS — apply `g` to the input channel, trace over `y`:
+
+Enter at `Right b`. On `Right a`, call `f (Right a)`. On `Left y`,
+call `f (Left (g y))`.
+
+Both implement the same state machine: each loop step feeds `g`-transformed
+values back into `f`. The sequence of states fed to `f` is identical;
+the exit condition depends only on `f`'s output. Same result.
+
+### Axiom 3: Tightening
+
+`h :: a -> b`, `f :: (x, b) -> (x, c)`, `g :: c -> d`. Channel `x`
+is untouched by `h` and `g` throughout.
+
+**With `(,)`.**
+
+```haskell
+trace (second g . f . second h) a
+  = let (x, d) = (second g . f . second h) (x, a) in d
+  = let (x, d) = second g (f (x, h a)) in d
+  = let (x, c) = f (x, h a) in g c
+  = g (let (x, c) = f (x, h a) in c)
+  = g (trace f (h a))
+  = (g . trace f . h) a
+```
+
+**With `Either`.**
+
+`h :: a -> b`, `f :: Either x b -> Either x c`, `g :: c -> d`.
+`second h` maps `Right a` to `Right (h a)`, leaves `Left x` alone.
+
+The while-loop enters at `Right (h a)`. The channel `x` flows through
+`Left` transitions in `f`, never touching `h` or `g`. Exit occurs
+when `f` returns `Right c`, at which point `g c` is returned.
+
+Both sides: enter at `Right (h a)`, loop on `f`'s `Left` transitions,
+exit with `g c`. `h` and `g` are straight wires — they pass freely
+through the trace.
+
+### Axiom 4: Strength
+
+`g :: a -> b` acts on payload `a` independently; `f :: (x, c) -> (x, d)`
+runs with the channel `x`. They operate on disjoint parts of the tensor.
+
+**With `(,)`.**
+
+`g ⊗ f` acts on payload `(a, c)` with channel `x`:
+```haskell
+g `par` f :: (x, (a, c)) -> (x, (b, d))
+g `par` f (x, (a, c)) = let (x', d) = f (x, c) in (x', (g a, d))
+```
+
+```haskell
+trace (g `par` f) (a, c)
+  = let (x, (b, d)) = (g `par` f) (x, (a, c)) in (b, d)
+  = let (x', d) = f (x, c) in (g a, d)       -- x tied to x' by knot
+  = (g a, let (x, d) = f (x, c) in d)
+  = (g a, trace f c)
+  = (g ⊗ trace f) (a, c)
+```
+
+`g` is invisible to the channel — the lazy knot ties only `c`/`d` via `f`.
+
+**With `Either`.**
+
+`g` acts on `Right a`, `f` runs the loop on `Either x c`. `g ⊗ f` maps
+`Left x` to `Left x` (channel passes through), `Right (Left a)` to
+`Right (Left (g a))` (g on the a-side), and delegates `Right (Right c)`
+to `f`.
+
+Both sides: `g` is a straight wire on the `a` component, `trace f`
+runs its loop on the `c` component. `g` has no feedback path and
+cannot affect when or how the loop exits.
+
+### Axiom 5: Yanking
+
+`swap :: (x, x) -> (x, x)` is the braiding.
+
+**With `(,)`.**
+
+```haskell
+trace swap x
+  = let (a, c) = swap (a, x) in c
+  = let (a, c) = (x, a) in c
+  = x
+  = id x
+```
+
+The lazy knot resolves immediately: `a` is set to `x` from
+`swap (a, x) = (x, a)`, and `c = a = x`. One substitution, no recursion.
+
+**With `Either`.**
+
+`swapEither :: Either a b -> Either b a` maps `Left x → Right x`,
+`Right x → Left x`.
+
+Enter at `Right x`. `swapEither (Right x) = Left x` — loop.
+Re-enter at `Left x`. `swapEither (Left x) = Right x` — exit with `x`.
+
+The while-loop runs exactly two steps. Operationally different from
+`(,)` — a two-step state machine vs an immediate lazy substitution —
+but the same result.
+
+**Why braiding is required.** The other four axioms involve only the
+channel and payload structure — they hold in any monoidal category with
+a trace. Yanking requires a morphism `swap : X ⊗ X → X ⊗ X` that is
+part of a braiding. In a non-braided monoidal category, no such
+morphism is guaranteed to exist, so yanking cannot be stated.
+
+For `(,)` and `Either` in Haskell, both are symmetric monoidal —
+`swap` exists and is involutive — so yanking holds.
+
+## Summary
+
+| Axiom | What it says | Key mechanism |
+|--------|-------------|---------------|
+| Vanishing | Unit channel is a no-op; products nest | Knot with nothing to tie |
+| Sliding | Channel bridge commutes past `f` | Same fixed point either side |
+| Tightening | Payload morphisms pass through | Channel untouched by `h`, `g` |
+| Strength | Independent payload wire is invisible | Disjoint types, no contact |
+| Yanking | Tracing a swap is identity | Requires braiding |
+
+The `(,)` and `Either` instances are operationally dual throughout:
+lazy knot vs while-loop. Every axiom holds for both by the same logical
+structure.
+
+## References
+
+- [Joyal, Street & Verity (1996)](https://doi.org/10.1017/s0305004100074338) — traced monoidal categories
+- [Launchbury, Krstic & Sauerwein (2013)](https://doi.org/10.4204/eptcs.129.9) — hyperfunction axioms
+- [Hasegawa (1997)](https://doi.org/10.1007/978-1-4471-0865-8_7) — Theorem 3.1: cartesian traces = fixpoints
+- [Van der Ploeg & Kiselyov (2014)](https://doi.org/10.1145/2633357.2633360) — Reflection Without Remorse
+- `other/02-a-knot-recovers-fix.md` — how the axioms force the GADT
+- `other/05-no-remorse-once-removed.md` — Mendler case as `viewl`
diff --git a/other/symbols.md b/other/symbols.md
new file mode 100644
--- /dev/null
+++ b/other/symbols.md
@@ -0,0 +1,238 @@
+# Notation
+
+**Summary:** The symbols used throughout the arc and examples. Mathematical
+notation, used as mathematical notation — no apologies to GHC.
+
+---
+
+## The Table
+
+| Symbol | Name | Type | Meaning |
+|--------|------|------|---------|
+| `↑` | lift | `(a → b) → Circuit arr t a b` | embed a plain arrow |
+| `↓` | lower | `Hyper a b → (a → b)` | observe a hyperfunction |
+| `⊙` | compose | `cat b c → cat a b → cat a c` | sequential composition |
+| `⊲` | push | `(a → b) → Hyper a b → Hyper a b` | prepend a plain function |
+| `⥁` | run | `Hyper a a → a` | tie the self-referential knot (recovers fix on lifted arrows) |
+| `∥` | ambient | `braid → Circuit arr t a b → Circuit arr t (t s a) (t s b)` | thread state wire alongside |
+| `↮` | knot | `arr (t a b) (t a c) → Circuit arr t b c` | feedback loop constructor |
+| `↘` | reify | `Circuit arr t x y → arr x y` | interpret to plain arrow |
+| `↪` | trace | `arr (t a b) (t a c) → arr b c` | close the feedback channel |
+| `↩` | untrace | `arr b c → arr (t a b) (t a c)` | open the feedback channel |
+| `⇨` | encode | `Circuit (->) (,) a b → Hyper a b` | initial → final (preserving) |
+| `⇦` | flatten | `Hyper a b → Circuit (->) (,) a b` | final → initial (lossy) |
+| `⇸` | invoke | `Hyper a b → Hyper b a → b` | apply a hyperfunction to its dual |
+| `○` | base | `a → Hyper b a` | constant continuation |
+| `↬` | — | `type ↬ = Hyper` | type-level synonym |
+
+The canonical API uses lowercase names (`lift`, `lower`, `reify`, etc.).
+The symbols are notation — used in proofs, diagrams, and the arc documents
+where the mathematical content should be visible without syntactic noise.
+
+---
+
+## Two Registers
+
+**The initial encoding** (`Circuit`) has visible constructors. Its symbols
+are construction and elimination forms:
+
+```
+↑ f          — constructor: embed f as a Lift
+↮ f          — constructor: embed f as a Knot
+f ⊙ g        — constructor: Compose f g
+↘ c          — eliminator: reify the circuit to a plain arrow
+```
+
+**The final encoding** (`Hyper`) has no constructors — only behaviour.
+Its symbols are observation and composition:
+
+```
+↑ f          — lift f into Hyper (coinductive unrolling)
+↓ h          — observe h by severing the feedback channel
+⥁ h          — run h by feeding its own dual back
+f ⊙ g        — compose: Hyper (\k -> invoke f (g . k))
+```
+
+`⊙` and `↑` appear in both registers with the same meaning — compose and
+lift are the same operation in both encodings. The difference is what
+the type checker sees underneath.
+
+---
+
+## The Six Axioms
+
+Written as we mean them, not as GHC requires them:
+
+```
+axiom 1   (f ⊙ g) ⊙ h  =  f ⊙ (g ⊙ h)               associativity
+axiom 2    f ⊙ ↑ id     =  f  =  ↑ id ⊙ f             identity
+axiom 3    ↑ (f . g)    =  ↑ f ⊙ ↑ g                  lift is a functor
+axiom 4    ⥁ (↑ f)       =  fix f                      run recovers fix of base arrows
+axiom 5    ⊲ f ⊙ ⊲ g    =  ⊲ (f . g)                  push is a homomorphism
+axiom 6    ⥁ ((f ⊲ p) ⊙ q)  =  f (⥁ (q ⊙ p))          feedback / sliding
+```
+
+Axioms 1–3 are the free category. Axiom 4 is the sanity check on lifted arrows
+(run recovers classical fixed points for base arrows). Axiom 5 says push
+respects composition. Axiom 6 is the one that isn't free (it forces Knot).
+
+---
+
+## The Five JSV Axioms
+
+The Joyal–Street–Verity axioms for a traced monoidal category. Channel
+is on the left; payload on the right. `⊗` is the tensor.
+
+```
+vanishing    ↪ (id ⊗ f)       =  f                    unit channel is a no-op
+sliding      ↪ ((id ⊗ g) ⊙ f) =  ↪ (f ⊙ (id ⊗ g))    channel bridge commutes
+tightening   ↪ ((g ⊗ id) ⊙ f ⊙ (h ⊗ id))  =  g ⊙ ↪ f ⊙ h    payload passes through
+strength     ↪ (g ⊗ f)        =  g ⊗ ↪ f              independent wire invisible
+yanking      ↪ swap            =  id                   tracing a swap is identity
+```
+
+For `(,)`, `↪` ties a lazy knot. For `Either`, `↪` runs a while-loop.
+The axioms hold for both by the same logical structure.
+
+---
+
+## The Triangle
+
+The commuting triangle connecting initial and final encodings:
+
+```
+         ⇨
+Circuit ────▶ Hyper
+    \           │
+     \          │ ↓
+      \         ▼
+       ↘──────▶ arr
+```
+
+```
+↓ . ⇨  =  ↘
+```
+
+Mapping a `Circuit` into `Hyper` and then observing gives the same result
+as running the `Circuit` directly. Proved case by case in
+[03-hyper-buries-the-knot.md](03-hyper-buries-the-knot.md).
+
+---
+
+## The Mendler Identity
+
+The operational form of the sliding axiom in `reify`:
+
+```
+↘ (↑ f)           =  f                    faithful embedding
+↘ (↮ k)           =  ↪ k                  trace closes the channel
+↘ (↮ f ⊙ g)       =  ↪ (f . ↩ (↘ g))     Mendler case: g participates inside
+↘ (f ⊙ g)         =  ↘ f . ↘ g            functoriality
+```
+
+The third line is the load-bearing one. Without it, `↘ (↮ f ⊙ g)` would
+reduce to `↪ f . ↘ g` — closing the channel before `g` participates.
+One equation separates the free traced monoidal category from the
+degenerate model.
+
+---
+
+## The Push/Lift Dual
+
+`push` and `(:)` play the same structural role in different carriers:
+
+```
+(:) x . foldr' xs   ≡   push x . foldh' xs
+```
+
+`(:)` attaches to the outside of a list. `push` threads into the inside
+of a `Hyper`, through the continuation channel. Same shape, flipped
+polarity. Both build endofunction chains:
+
+```
+foldr'  :: [a → a] → ([a] → [a])       — Endo([a])
+foldh'  :: [a → a] → (Hyper a a → Hyper a a)   — Endo(Hyper a a)
+```
+
+`push` is not compound in `Hyper` — it is primitive, threading through the
+feedback channel.  The GADT has no direct counterpart; `Compose (Lift f) h`
+(post-composition on `reify`) is the closest analogue but not equivalent.
+
+---
+
+## State Threading
+
+`ambient` (symbol `∥`) threads a state wire through a circuit unchanged.
+The braid argument swaps state past the feedback channel:
+
+```
+∥ braid (↑ f)    =  ↑ (↩ f)            state tags along via untrace
+∥ braid (f ⊙ g)  =  ∥ braid f ⊙ ∥ braid g   state threads both stages
+∥ braid (↮ k)    =  ↮ (dimap braid braid (↩ k))   state slides past knot
+```
+
+The third equation is the sliding axiom wearing circuit clothes: a state
+wire slides past a feedback loop via braiding. This is why `ambient`
+requires an explicit braid argument — the braid is the proof that the
+state and the channel are independent.
+
+---
+
+## Encoding Worked Example
+
+Fibonacci stream via the triangle:
+
+```
+fibs :: Circuit (->) (,) () [Int]
+fibs = ↮ (\(xs, ()) -> (0 : 1 : zipWith (+) xs (drop 1 xs), xs))
+
+-- Run directly:
+↘ fibs ()
+= ↪ (\(xs, ()) -> (0 : 1 : zipWith (+) xs (drop 1 xs), xs)) ()
+= let (xs, ys) = ... in ys      -- lazy knot
+
+-- Run via Hyper:
+↓ (⇨ fibs) ()
+= ↓ (↪ (↑ step)) ()             -- encode (↮ f) = ↪ (↑ f)
+= ... same lazy knot ...         -- triangle: ↓ . ⇨ = ↘
+```
+
+Both paths reach the same stream. The triangle is not just a diagram —
+it is an equality between two ways of running the same program.
+
+---
+
+## Factorial via Either
+
+```
+fac :: Circuit (->) Either (Int, Int) Int
+fac = ↮ step
+  where
+    step (Right (n, acc))  | n <= 1  =  Right acc
+    step (Right (n, acc))            =  Left (n - 1, n * acc)
+    step (Left s)                    =  step (Right s)
+
+↘ fac (5, 1)
+= ↪ step (5, 1)
+= go (Right (5, 1))
+= go (Left (4, 5))
+= go (Left (3, 20))
+= go (Left (2, 60))
+= go (Left (1, 120))
+= 120
+```
+
+`↪` on `Either` is the while-loop. `Left` feeds back; `Right` exits.
+The `↮` constructor is the same as for `(,)` — the tensor choice is what
+changes the operational character.
+
+---
+
+## References
+
+- [01-marks-and-stacks.md](01-marks-and-stacks.md) — the five marks introduced
+- [02-a-knot-recovers-fix.md](02-a-knot-recovers-fix.md) — the Mendler identity derived
+- [03-hyper-buries-the-knot.md](03-hyper-buries-the-knot.md) — the triangle proved
+- [axioms.md](axioms.md) — JSV axioms proved for both tensors
+- [Launchbury, Krstic & Sauerwein (2013)](https://doi.org/10.4204/eptcs.129.9) — original LKS axiom system
+- [Joyal, Street & Verity (1996)](https://doi.org/10.1017/s0305004100074338) — traced monoidal categories
diff --git a/readme.md b/readme.md
new file mode 100644
--- /dev/null
+++ b/readme.md
@@ -0,0 +1,112 @@
+<p align="center"><strong>⟴ circuits</strong></p>
+
+## First-Class Feedback
+
+> The free traced monoidal category is the smallest thing you can add to a
+> category to get feedback. Not a library of combinators — a single GADT and
+> a single coinductive type, a hyperfunction no less, connected by this Galois connection ...
+>
+> ~ What we learned building it
+
+<br>
+
+## ⚙️ Install
+
+```
+(m)cabal build circuits
+```
+
+Compiles on MicroHS & GHC 9.10+ with `base` & `profunctors`
+
+## 📡 Usage
+
+```haskell
+import Circuit
+
+-- Fibonacci via knot-tying
+>>> take 5 (trace (\(fibs, ()) -> (0 : 1 : zipWith (+) fibs (drop 1 fibs), fibs)) () :: [Integer])
+[0,1,1,2,3]
+
+-- Iteration with Either
+>>> let step n = if n < 3 then Left (n + 1) else Right n in trace (either step step) (0 :: Int)
+3
+```
+
+## Representations
+
+`Circuit arr t a b` is the initial, inspectable encoding (a GADT with `Lift`, `Compose`, and `Knot`). `Hyper a b` is the final, coinductive encoding in which the feedback channel is structural in the type. The `Trace` class abstracts the tensor, giving lazy knots via `(,)` or iteration via `Either` (with the convention `Left` feeds back, `Right` exits).
+
+Conversion is given by `reify` and `encode` (and `encodeEither`/`runEither`). The core triangle on observables is `reify . encode = id`.
+
+## 🧭 Pitch
+
+circuits is a rethink of how to interact with a compiler and arrange code
+pipelines — circuits — in ways that are intentional, clear, correct and performant.
+
+Hyper is the same as the Kidney & Wu construction:
+
+```haskell
+newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }
+```
+
+From the paper and surrounding literature, we use the hyperfunction axioms and derive a `Circuit`:
+
+```haskell
+data Circuit arr t a b where
+  Lift    :: arr a b -> Circuit arr t a b
+  Compose :: Circuit arr t b c -> Circuit arr t a b -> Circuit arr t a c
+  Knot    :: arr (t a b) (t a c) -> Circuit arr t b c
+```
+
+This happens to be the initial traced category over a base category and naturally encodes to a Hyper. To be concrete and on the nose, it's a 2-cell bolted on to the free category. Lifting the trace over a category and abstracting the tensor came later.
+
+> Have you used your eyeballs yet and read Bartosz's latest? Original thought is a strong claim and could be awkward.
+>
+> ~ claude ([tank](https://github.com/tonyday567/mg/blob/main/word/tank.md) mode on)
+
+`Circuit` covers functions, compositional paths, and feedback loops. `Hyper` is an efficient final encoding where feedback dissolves into the type structure itself. The `Trace` class (in `Circuit.Traced`) abstracts the tensor, giving polymorphic loop semantics: lazy knots with `(,)` or iteration with `Either`. All braided, cartesian and cocartesian structure lives in `Circuit.Monoidal`.
+
+`other/` traces these ideas from the [Kidney & Wu hyperfunctions](https://doi.org/10.1145/3776649) paper through a narrative arc. `Circuit` is the initial encoding — a GADT
+with visible constructors, interpreted by `reify`. `Hyper` is the final
+encoding — a coinductive type where feedback dissolves into the structure
+itself. The triangle `reify = lower . encode` connects them.
+
+## 📦 Sibling libraries
+
+**circuits-parser** — `Circuit (->) Either f (These a f)` as a parser for a wide variety of f and a.
+
+**circuits-io** — `Circuit (Kleisli IO) Either` as a way to engage with file I/O, sockets, servers, (a)timings & asynchronicity.
+
+**circuits-meter** — circuit measurement and performance.
+
+## 📖 Read
+
+["tracing hyperfunctions"](https://doi.org/10.1145/3776649) — Kidney & Wu (2026). The paper that inspired the core construction. Introduces `Hyper` as a self-dual object in the traced sense and the hyperfunction axioms.
+
+`other/` — the narrative arc (notation, marks-and-stacks, knot, triangle proof, tensors, Mendler case, examples). For the long version.
+
+`examples/` — cards: parsers, pipes, Elgot iteration, delimited continuations. Paste code blocks into `cabal repl`.
+
+## Contributing
+
+We welcome contributions of any persuasion or fancy. New contributors should open an issue and say hi.
+
+AI / LLM policy
+
+LLMs and agents have been used in the development of this library, including category theory, coding, generation, refactoring, documentation and narrative.
+
+what we prefer
+  ⟜ all code must compile, have and pass doctests, and be reviewable.
+  ⟜ if you open a PR, you must be able to explain what the code does and why. "my buddy Grok wrote it" is not an explanation.
+  ⟜ do not submit code you have not read, understood, and tested.
+
+what we do not do
+  ⟜ ban AI tools. they are part of the workflow.
+  ⟜ accept code that fails the same standards we apply to AI contributions.
+
+code is code and coders are going to code.
+
+<br>
+
+[![Hackage](https://img.shields.io/hackage/v/circuits.svg)](https://hackage.haskell.org/package/circuits)
+[![build](https://github.com/tonyday567/circuits/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/tonyday567/circuits/actions/workflows/haskell-ci.yml)
diff --git a/src/Circuit.hs b/src/Circuit.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit.hs
@@ -0,0 +1,143 @@
+-- | Circuit: free traced monoidal categories and hyperfunctions.
+--
+-- == Usage
+--
+-- @
+-- import Circuit
+-- @
+--
+-- === Lazy feedback (knot-tying)
+--
+-- Use the @(,@) tensor to tie a lazy knot. The feedback value and output
+-- are produced simultaneously.
+--
+-- >>> let powers (ns, ()) = (1 : map (*2) ns, take 5 ns)
+-- >>> trace powers () :: [Integer]
+-- [1,2,4,8,16]
+--
+-- === Iteration
+--
+-- Use the 'Either' tensor for loops that terminate.
+--
+-- >>> let step n = if n < 5 then Left (n + 1) else Right n
+-- >>> trace (either step step) (0 :: Int)
+-- 5
+--
+-- === Switching between representations
+--
+-- 'Circuit' is the inspectable GADT form. 'Hyper' is the efficient final
+-- encoding. Convert with 'encode' and 'reify'.
+--
+-- >>> lower (encode (Lift (+1) :: Circuit (->) (,) Int Int)) 41
+-- 42
+--
+-- >>> reify (Knot (\(acc, x) -> (x, acc)) :: Circuit (->) (,) Int Int) 0
+-- 0
+--
+-- == Overview
+--
+-- This library provides two representations of feedback:
+--
+-- * 'Circuit' (in "Circuit.Circuit") — the initial, inspectable GADT encoding.
+-- * 'Hyper' (in "Circuit.Hyper") — the final, coinductive encoding.
+--
+-- The 'Trace' class (in "Circuit.Traced") abstracts the choice of tensor,
+-- currently supporting lazy knots with @(,@) and iteration with 'Either'.
+--
+-- All braided, cartesian, and cocartesian structure, plus the general
+-- 'ambientBy' state-threading combinator, lives in "Circuit.Monoidal".
+--
+-- == Core Concepts
+--
+-- * __Tensor__ (@t@): The bifunctor pairing a feedback value with a payload
+--   inside a 'Knot' (currently @(,@) or 'Either').
+--
+-- * __Feedback value__: The component that travels around the loop (first
+--   parameter of the tensor in a 'Knot').
+--
+-- * __Payload__: The value being transformed and emitted (second parameter
+--   of the tensor).
+--
+-- * __Feedback channel__: The path the feedback value takes when routed back
+--   into the next step.
+module Circuit
+  ( -- * Circuit
+    Circuit (..),
+    Wire,
+    Step,
+    reify,
+
+    -- * Traced
+    Trace (..),
+    cellIO,
+
+    -- * Hyper
+    Hyper (..),
+    lift,
+    lower,
+    base,
+    push,
+    run,
+    encode,
+    encodeEither,
+    runEither,
+    flatten,
+
+    -- * Monoidal
+    Braided (..),
+    ambient,
+    assoc,
+    assoc',
+    seed,
+    absorb,
+    release,
+    coassoc,
+    coassoc',
+    coseed,
+    coabsorbL,
+    coabsorbR,
+    coreleaseL,
+    coreleaseR,
+    ambientBy,
+  )
+where
+
+import Circuit.Circuit
+  ( Circuit (..),
+    Step,
+    Wire,
+    reify,
+  )
+import Circuit.Hyper
+  ( Hyper (..),
+    base,
+    encode,
+    encodeEither,
+    flatten,
+    lift,
+    lower,
+    push,
+    run,
+    runEither,
+  )
+import Circuit.Monoidal
+  ( Braided (..),
+    absorb,
+    ambient,
+    ambientBy,
+    assoc,
+    assoc',
+    coabsorbL,
+    coabsorbR,
+    coassoc,
+    coassoc',
+    coreleaseL,
+    coreleaseR,
+    coseed,
+    release,
+    seed,
+  )
+import Circuit.Traced
+  ( Trace (..),
+    cellIO,
+  )
diff --git a/src/Circuit/Circuit.hs b/src/Circuit/Circuit.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Circuit.hs
@@ -0,0 +1,145 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | The free traced monoidal category.
+--
+-- @Circuit arr t a b@ is the initial encoding of a traced monoidal category
+-- over a base morphism @arr@ with a supplied tensor @t@ for the category. The three constructors encode:
+--
+--   - `Lift`: embedding of a base arrow (strict monoidal functor)
+--   - `Compose`: sequential composition (category structure)
+--   - `Knot`: introduces a feedback channel (trace structure)
+--
+-- For example, a `Circuit (->) (,)` is the initial traced monoidal cartesian category over Haskell functions.
+--
+-- == Core Concepts
+--
+-- * __Tensor__ (@t@): The bifunctor that pairs a feedback value with a payload
+--   inside a 'Knot'. The two tensors provided are @(,)@ (simultaneous / lazy
+--   sharing) and 'Either' (sequential / iteration).
+--
+-- * __Feedback value__: The component that travels around the loop (the first
+--   parameter of the tensor inside a 'Knot').
+--
+-- * __Payload__: The component that is transformed and emitted by the circuit
+--   (the second parameter of the tensor).
+--
+-- * __Feedback channel__: The path the feedback value takes when it is routed
+--   back into the next step of the computation. In a 'Knot' the channel type
+--   is carried by the tensor @t@.
+--
+-- These concepts are independent of any particular base arrow @arr@. They
+-- describe the structure of feedback itself.
+--
+-- The `reify` function interprets any `Circuit` to a plain arrow via
+-- the `Trace` instance on @t@. For encoding into 'Circuit.Hyper', see
+-- 'Circuit.Hyper.encode' and 'Circuit.Hyper.encodeEither'.
+module Circuit.Circuit
+  ( -- * Circuit
+    Circuit (..),
+
+    -- * Type aliases
+    Wire,
+    Step,
+
+    -- * Operators
+    reify,
+  )
+where
+
+import Circuit.Traced (Trace (..))
+import Prelude hiding (id, (.))
+
+#ifdef __GLASGOW_HASKELL__
+import Control.Category
+import Data.Bifunctor
+import Data.Profunctor
+#else
+import Circuit.Classes
+#endif
+
+-- $setup
+-- >>> import Control.Category ((>>>))
+-- >>> import Data.Profunctor (dimap)
+-- >>> import Prelude hiding (id, (.))
+
+-- | The free traced monoidal category over base morphism @arr@ and tensor @t@.
+--
+-- Three constructors:
+--
+--   * 'Lift' — embed a base arrow.
+--   * 'Compose' — sequential composition.
+--   * 'Knot' — feedback loop via the tensor.
+data Circuit arr t a b where
+  -- | Lift embeds a base arrow (strict monoidal functor).
+  --
+  -- >>> reify (Lift (+1) :: Circuit (->) (,) Int Int) 5
+  -- 6
+  Lift :: arr a b -> Circuit arr t a b
+  -- | Compose performs sequential composition (category structure).
+  --
+  -- >>> reify (Lift (+1) >>> Lift (*2) :: Circuit (->) (,) Int Int) 5
+  -- 12
+  Compose :: Circuit arr t b c -> Circuit arr t a b -> Circuit arr t a c
+  -- | Knot ties a feedback loop. The tensor @t@ carries the channel type.
+  --
+  -- >>> reify (Knot (\(acc, x) -> (x, acc)) :: Circuit (->) (,) Int Int) 42
+  -- 42
+  Knot :: arr (t a b) (t a c) -> Circuit arr t b c
+
+-- | A traced circuit over plain functions with the cartesian tensor.
+--
+-- @Wire a b = Circuit (->) (,) a b@
+--
+-- The @(,)@ tensor ties a lazy knot: output and feedback are produced
+-- simultaneously.
+type Wire = Circuit (->) (,)
+
+-- | A traced circuit over plain functions with the cocartesian tensor.
+--
+-- @Step a b = Circuit (->) Either a b@
+--
+-- The @Either@ tensor iterates: @Left@ feeds back (continue),
+-- @Right@ terminates (exit).
+type Step = Circuit (->) Either
+
+instance (Category arr) => Category (Circuit arr t) where
+  id = Lift id
+  (.) = Compose
+
+instance Functor (Circuit (->) t a) where
+  fmap f = Compose (Lift f)
+
+-- | Profunctor instance for Circuit.
+--
+-- Maps over both ends of the arrow. For @Compose@, the map is applied
+-- to the input of the left sub-circuit and the output of the right
+-- sub-circuit, leaving the intermediate type aligned.
+--
+-- >>> reify (dimap (+ 1) (+ 1) (Lift (* 2) :: Circuit (->) (,) Int Int)) 5
+-- 13
+instance (Profunctor arr, Bifunctor t) => Profunctor (Circuit arr t) where
+  dimap f g (Lift h) = Lift (dimap f g h)
+  dimap f g (Compose h k) = Compose (dimap id g h) (dimap f id k)
+  dimap f g (Knot k) = Knot (dimap (second f) (second g) k)
+  lmap f (Lift h) = Lift (lmap f h)
+  lmap f (Compose h k) = Compose (lmap id h) (lmap f k)
+  lmap f (Knot k) = Knot (lmap (second f) k)
+  rmap g (Lift h) = Lift (rmap g h)
+  rmap g (Compose h k) = Compose (rmap g h) (rmap id k)
+  rmap g (Knot k) = Knot (rmap (second g) k)
+
+-- | Interpret a Circuit to a plain arrow.
+--
+-- This is the canonical map out of the free (initial) traced monoidal
+-- category.  The interesting case is when a @Knot@ appears on the left
+-- of a @Compose@: this is exactly where the sliding axiom of traced
+-- monoidal categories is enforced (the Mendler case).
+--
+-- >>> reify (Lift (+1) :: Circuit (->) (,) Int Int) 5
+-- 6
+reify :: (Category arr, Trace arr t) => Circuit arr t x y -> arr x y
+reify (Lift f) = f
+reify (Compose (Knot f) g) = trace (f . untrace (reify g))
+reify (Compose f g) = reify f . reify g
+reify (Knot k) = trace k
diff --git a/src/Circuit/Classes.hs b/src/Circuit/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Classes.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE CPP #-}
+
+-- | On GHC, Category, Bifunctor, and Profunctor come from packages.
+-- On other compilers (e.g. MicroHs), we define them locally.
+module Circuit.Classes where
+
+#ifndef __GLASGOW_HASKELL__
+
+import Prelude hiding (id, (.))
+
+class Category cat where
+  id :: cat a a
+  (.) :: cat b c -> cat a b -> cat a c
+
+instance Category (->) where
+  id x = x
+  (f . g) x = f (g x)
+
+class Bifunctor p where
+  bimap :: (a -> b) -> (c -> d) -> p a c -> p b d
+  first :: (a -> b) -> p a c -> p b c
+  second :: (b -> c) -> p a b -> p a c
+  bimap f g = first f . second g
+  first f = bimap f id
+  second = bimap id
+
+instance Bifunctor (,) where
+  bimap f g (a, b) = (f a, g b)
+
+instance Bifunctor Either where
+  bimap f _ (Left a) = Left (f a)
+  bimap _ g (Right b) = Right (g b)
+
+class Profunctor p where
+  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
+  lmap :: (a -> b) -> p b c -> p a c
+  rmap :: (b -> c) -> p a b -> p a c
+  dimap f g = lmap f . rmap g
+  lmap f = dimap f id
+  rmap = dimap id
+
+#endif
diff --git a/src/Circuit/Hyper.hs b/src/Circuit/Hyper.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Hyper.hs
@@ -0,0 +1,287 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Hyperfunctions: final encoding of traced monoidal categories.
+--
+-- A hyperfunction (following Kidney & Wu) is a value that is completely
+-- defined by its dual: to produce a result of type @b@ you must supply
+-- a continuation of type @Hyper b a@.
+--
+-- 'Hyper' is the /final/ (coinductive) encoding of a traced monoidal
+-- category. Its dual, 'Circuit' (see "Circuit.Circuit"), is the
+-- corresponding /initial/ (inductive) encoding. The feedback channel
+-- is not represented by an extra constructor; it is structural in the
+-- type itself.
+module Circuit.Hyper
+  ( -- * Hyper
+    Hyper (..),
+
+    -- * Construction and elimination
+    lift,
+    lower,
+    base,
+    push,
+    run,
+
+    -- * Encoding
+    encode,
+    encodeEither,
+    runEither,
+    flatten,
+  )
+where
+
+import Circuit.Circuit (Circuit (..), reify)
+import Circuit.Traced (Trace (..))
+import Prelude hiding (id, (.))
+
+#ifdef __GLASGOW_HASKELL__
+import Control.Category
+import Data.Profunctor
+#else
+import Circuit.Classes
+#endif
+
+-- $setup
+-- >>> import Prelude hiding (id, (.))
+-- >>> import Control.Category
+-- >>> import Data.Profunctor
+-- >>> import Circuit.Traced (Trace (..))
+-- >>> import Circuit.Circuit (Circuit (..), reify)
+-- >>> let h = lift (+1) :: Hyper Int Int
+-- >>> let f1 = (*2) :: Int -> Int
+-- >>> let g1 = (+10) :: Int -> Int
+-- >>> let f2 = (+3) :: Int -> Int
+-- >>> let g2 = (*100) :: Int -> Int
+
+-- | A hyperfunction from @a@ to @b@.
+--
+-- A 'Hyper' is completely determined by its dual. To get a @b@ you must
+-- provide a continuation that can itself produce an @a@.
+--
+-- Two small examples:
+--
+-- >>> lower (lift (+1)) 41
+-- 42
+--
+-- >>> run (Hyper $ \k -> invoke k (Hyper $ \_ -> 0) + 1)
+-- 1
+newtype Hyper a b = Hyper
+  { -- | Feed a continuation of type @Hyper b a@ into the hyperfunction.
+    invoke :: Hyper b a -> b
+  }
+
+-- * Construction and elimination
+
+-- | Embed a plain function into a hyperfunction.
+--
+-- This is where the coinductive character of 'Hyper' lives:
+-- @lift f@ creates a hyperfunction by recursively pushing @f@ onto
+-- every future continuation that will ever be supplied.
+--
+-- >>> lower (lift (+1)) 5
+-- 6
+lift :: (a -> b) -> Hyper a b
+lift f = push f (lift f)
+
+-- | Extract a plain function from a hyperfunction.
+--
+-- Supplies the hyperfunction with a constant continuation
+-- (@invoke h (Hyper (const a))@), asking: "what output do you produce
+-- when the feedback channel feeds back the input @a@?"
+--
+-- >>> lower (lift reverse) "hello"
+-- "olleh"
+lower :: Hyper a b -> (a -> b)
+lower h a = invoke h (Hyper (const a))
+
+-- | Ignores the input and returns a constant value.
+--
+-- >>> lower (base 42) undefined
+-- 42
+base :: a -> Hyper b a
+base a = Hyper (const a)
+
+-- | Push a plain function onto a hyperfunction.
+--
+-- The function @f@ is applied to whatever value the hyperfunction
+-- eventually produces. This threads @f@ through the continuation,
+-- enabling feedback-aware composition.
+--
+-- >>> lower (push (+1) (lift (*2))) 5
+-- 6
+push :: (a -> b) -> Hyper a b -> Hyper a b
+push f h = Hyper (\k -> f (invoke k h))
+
+-- | Close the self-referential loop.
+--
+-- @run h@ feeds the hyperfunction back into itself, tying the knot.
+-- This is the fundamental way to eliminate a 'Hyper'.
+--
+-- >>> run (Hyper $ \_ -> 42 :: Int)
+-- 42
+--
+-- >>> run (Hyper $ \h -> invoke h (Hyper $ \_ -> 0) + 1) :: Int
+-- 1
+run :: Hyper a a -> a
+run h = invoke h (Hyper run)
+
+-- * Properties
+
+-- Faithful embedding: observation recovers the original arrow.
+--
+-- prop> \x -> lower (lift (+1)) (x :: Int) == x + 1
+
+-- Functoriality: lift respects composition.
+--
+-- prop> \x -> lower (lift (*2) . lift (+1)) (x :: Int) == (x + 1) * 2
+
+-- * Trace
+
+-- | 'Trace' instance for 'Hyper' with the @(,)@ tensor.
+--
+-- Transcribes the lazy-knot trace from @(->)@ into Hyper's continuation
+-- language. Where @Trace (->) (,)@ can write @let (a, c) = f (a, b) in c@
+-- directly, Hyper must route the self-reference through explicit 'Hyper'
+-- values:
+--
+--   1. @invoke body cont@ calls the body, which will eventually ask @cont@
+--      for an @(a, b)@ — the feedback pair.
+--   2. @cont@ captures @a@ from @body@'s output (@fst pair@) and feeds it
+--      back as the first component of its return. This is the knot: @a@
+--      cycles through @body → pair → cont → body@.
+--   3. @invoke k (Hyper (const (snd pair)))@ converts the output @c@ to a
+--      @b@ for @cont@'s return type — purely type plumbing.
+--
+-- Law: @lower (trace (lift f)) x = trace \@ (->) f x@
+--
+-- >>> import Circuit.Traced (Trace (..))
+-- >>> let body = lift (\(xs, ()) -> (0:xs, take 3 xs))
+-- >>> lower (trace body) ()
+-- [0,0,0]
+instance Trace Hyper (,) where
+  trace body = Hyper $ \k ->
+    let pair = invoke body cont
+        cont = Hyper $ \_ ->
+          let a_val = invoke k (Hyper (const (snd pair)))
+           in (fst pair, a_val)
+     in snd pair
+  untrace = lift . fmap . lower
+
+-- * Encoding Circuit into Hyper
+
+-- | Encode a Circuit into a Hyper. Symbol: @(⇨)@.
+--
+-- This is the unique traced functor from the initial object (Circuit)
+-- to the final object (Hyper), satisfying the commuting triangle
+-- @lower . encode = reify@.
+--
+-- The @Knot@ case uses Hyper's own @Trace (,)@ instance — a coinductive
+-- lazy knot that preserves the feedback structure inside Hyper.
+-- For an Either-loop encoding, see 'encodeEither'.
+--
+-- >>> import Circuit.Circuit (Circuit (..), reify)
+-- >>> lower (encode (Lift (+1) :: Circuit (->) (,) Int Int)) 5
+-- 6
+encode :: Circuit (->) (,) a b -> Hyper a b
+encode (Lift f) = lift f
+encode (Compose f g) = encode f . encode g
+encode (Knot f) = trace (lift f)
+
+-- | Encode an Either-loop as a self-referential Hyper.
+--
+-- Whereas 'encode' handles the @(,)@ tensor using Hyper's own Trace
+-- instance, this preserves the Either-loop state in the function domain.
+-- @Left a@ feeds back; @Right c@ terminates with output.
+--
+-- >>> :{
+-- let step = \case
+--       Right n | n < 3 -> Left (n + 1)
+--       Right n         -> Right n
+--       Left n  | n < 3 -> Left (n + 1)
+--       Left n          -> Right n
+-- :}
+--
+-- >>> runEither step (0 :: Int)
+-- 3
+encodeEither :: (Either a b -> Either a c) -> Hyper (Either a b -> c) (Either a b -> c)
+encodeEither f = h
+  where
+    h =
+      Hyper
+        ( \k s ->
+            case f s of
+              Right c -> c
+              Left a -> invoke k h (Left a)
+        )
+
+-- | Run an 'encodeEither'-encoded circuit from initial input @b@.
+--
+-- @runEither@ is to @encodeEither@ what @run . lift@ is to plain functions:
+-- 'encodeEither' embeds the Either state machine into Hyper, @run@ ties the
+-- self-referential knot, and @Right b@ injects the initial state.
+--
+-- >>> :{
+-- let step = \case
+--       Right n | n < 3 -> Left (n + 1)
+--       Right n         -> Right n
+--       Left n  | n < 3 -> Left (n + 1)
+--       Left n          -> Right n
+-- :}
+--
+-- >>> runEither step (0 :: Int)
+-- 3
+runEither :: (Either a b -> Either a c) -> b -> c
+runEither f b = run (encodeEither f) (Right b)
+
+-- | Flatten a Hyper to a Circuit by observing it.
+--
+-- This is the forgetful map from the final encoding to the initial encoding.
+-- All feedback structure is lost; only the observable behaviour remains.
+--
+-- >>> let h = lift (+ 1)
+-- >>> reify (flatten h) 5
+-- 6
+--
+-- Flatten then encode is not identity — the feedback structure is gone:
+--
+-- >>> let h = lift (+ 1)
+-- >>> lower (encode (flatten h)) 5
+-- 6
+flatten :: Hyper a b -> Circuit (->) (,) a b
+flatten h = Lift (lower h)
+
+-- * Instances
+
+instance Category Hyper where
+  id = lift id
+  f . g = Hyper $ \h -> invoke f (g . h)
+
+-- | 'Profunctor' instance for 'Hyper'.
+--
+-- 'rmap' is not a composition of 'push'; it acts directly on the
+-- hyperfunction's output. 'dimap' routes both input and output
+-- through the continuation structure.
+--
+-- Profunctor identity: dimap id id = id
+--
+-- prop> \x -> lower (dimap id id h) (x :: Int) == x + 1
+--
+-- Profunctor composition: dimap f g . dimap f' g' = dimap (f' . f) (g . g')
+--
+-- prop> \x -> lower (dimap f1 g1 (dimap f2 g2 h)) (x :: Int) == lower (dimap (f2 . f1) (g1 . g2) h) x
+--
+-- lmap f = dimap f id
+--
+-- prop> \x -> lower (lmap ((*2) :: Int -> Int) h) (x :: Int) == lower (dimap ((*2) :: Int -> Int) id h) x
+--
+-- rmap g = dimap id g
+--
+-- prop> \x -> lower (rmap ((*2) :: Int -> Int) h) (x :: Int) == lower (dimap id ((*2) :: Int -> Int) h) x
+instance Profunctor Hyper where
+  dimap f g h = Hyper $ g . invoke h . dimap g f
+  lmap f h = Hyper $ invoke h . rmap f
+  rmap f h = Hyper $ f . invoke h . lmap f
+
+instance Functor (Hyper a) where
+  fmap = rmap
diff --git a/src/Circuit/Monoidal.hs b/src/Circuit/Monoidal.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Monoidal.hs
@@ -0,0 +1,199 @@
+{-# LANGUAGE CPP #-}
+
+-- | Monoidal structure for the tensors used in traced categories.
+--
+-- This module collects the braided, cartesian, and cocartesian structure
+-- over the standard tensors @(,)@ and 'Either', along with the general
+-- 'ambientBy' combinator for threading additional state wires.
+--
+-- The goal is to keep the core 'Circuit' GADT and 'reify' mechanism
+-- independent of these structural details.
+module Circuit.Monoidal
+  ( Braided (..),
+    ambient,
+    assoc,
+    assoc',
+    seed,
+    absorb,
+    release,
+    coassoc,
+    coassoc',
+    coseed,
+    coabsorbL,
+    coabsorbR,
+    coreleaseL,
+    coreleaseR,
+    ambientBy,
+  )
+where
+
+#ifdef __GLASGOW_HASKELL__
+import Data.Profunctor (Profunctor, dimap)
+import Data.Bifunctor (Bifunctor (..))
+#else
+import Circuit.Classes (Profunctor, Bifunctor (..))
+#endif
+
+import Circuit.Circuit (Circuit (..))
+import Circuit.Traced (Trace (..))
+
+-- ===========================================================================
+-- BRAIDING
+-- ===========================================================================
+
+-- | A symmetric braiding for a bifunctor tensor.
+--
+-- The braid swaps a wire past a nested pair:
+--
+-- @
+--   t x (t y z)  ->  t y (t x z)
+-- @
+--
+-- For @(,)@ this is the cartesian slide.  For @Either@ it is the
+-- coproduct slide.  Both are derived from the associator and swap.
+class (Bifunctor t) => Braided t where
+  braid :: t x (t y z) -> t y (t x z)
+
+-- | Cartesian slide: @(x, (y, z)) -> (y, (x, z))@.
+instance Braided (,) where
+  braid (x, (y, z)) = (y, (x, z))
+
+-- | Coproduct slide.
+--
+-- >>> braid (Left "hi" :: Either String (Either Int Bool))
+-- Right (Left "hi")
+instance Braided Either where
+  braid (Left x) = Right (Left x)
+  braid (Right (Left y)) = Left y
+  braid (Right (Right z)) = Right (Right z)
+
+-- | Thread a state wire through a circuit using the canonical braid.
+--
+-- This is 'ambientBy' with the braid supplied by the 'Braided' instance.
+ambient ::
+  (Profunctor arr, Trace arr t, Braided t) =>
+  Circuit arr t a b -> Circuit arr t (t s a) (t s b)
+ambient = ambientBy braid
+
+-- ===========================================================================
+-- CARTESIAN STRUCTURE ((,))
+-- ===========================================================================
+
+-- | Associator: @(a, (b, c)) -> ((a, b), c)@.
+assoc :: (a, (b, c)) -> ((a, b), c)
+assoc (a, (b, c)) = ((a, b), c)
+
+-- | Inverse associator: @((a, b), c) -> (a, (b, c))@.
+assoc' :: ((a, b), c) -> (a, (b, c))
+assoc' ((a, b), c) = (a, (b, c))
+
+-- | Introduce a state wire alongside a payload.
+--
+-- Given an initial state and a payload value, produce a paired value
+-- suitable for feeding into a circuit threaded with 'ambientBy'.
+seed :: s -> a -> (s, a)
+seed s a = (s, a)
+
+-- | Move a value from the payload into the state wire.
+--
+-- @absorb f = first (uncurry f) . assoc@
+absorb :: (t -> s -> s') -> (s, (t, b)) -> (s', b)
+absorb f (s, (t, b)) = (f t s, b)
+
+-- | Move a value from the state wire into the payload.
+--
+-- @release f = assoc' . first f@
+release :: (s -> (s', t)) -> (s, b) -> (s', (t, b))
+release f (s, b) = let (s', t) = f s in (s', (t, b))
+
+-- ===========================================================================
+-- COCARTESIAN STRUCTURE (Either)
+-- ===========================================================================
+
+-- | Coassociator for sums.
+--
+-- >>> coassoc (Left 1 :: Either Int (Either Bool Char))
+-- Left (Left 1)
+coassoc :: Either a (Either b c) -> Either (Either a b) c
+coassoc (Left a) = Left (Left a)
+coassoc (Right (Left b)) = Left (Right b)
+coassoc (Right (Right c)) = Right c
+
+-- | Inverse coassociator.
+--
+-- >>> coassoc' (Left (Left 1) :: Either (Either Int Bool) Char)
+-- Left 1
+coassoc' :: Either (Either a b) c -> Either a (Either b c)
+coassoc' (Left (Left a)) = Left a
+coassoc' (Left (Right b)) = Right (Left b)
+coassoc' (Right c) = Right (Right c)
+
+-- | Tag a state value onto whichever branch of the sum is active.
+--
+-- >>> coseed "st" (Left 42 :: Either Int Char)
+-- Left ("st",42)
+coseed :: s -> Either a b -> Either (s, a) (s, b)
+coseed s = bimap (s,) (s,)
+
+-- | If the left branch is taken, move a value from the payload into the state wire.
+--
+-- >>> coabsorbL (+) (Left (10, (3, 'x')) :: Either (Int, (Int, Char)) Bool)
+-- Left (13,'x')
+coabsorbL :: (t -> s -> s') -> Either (s, (t, a)) b -> Either (s', a) b
+coabsorbL f (Left (s, (t, a))) = Left (f t s, a)
+coabsorbL _ (Right b) = Right b
+
+-- | If the right branch is taken, move a value from the payload into the state wire.
+--
+-- >>> coabsorbR (+) (Right (10, (3, 'x')) :: Either Bool (Int, (Int, Char)))
+-- Right (13,'x')
+coabsorbR :: (t -> s -> s') -> Either a (s, (t, b)) -> Either a (s', b)
+coabsorbR f (Right (s, (t, b))) = Right (f t s, b)
+coabsorbR _ (Left a) = Left a
+
+-- | If the left branch is taken, move a value from the state wire into the payload.
+--
+-- >>> coreleaseL (\s -> (s+1, s*2)) (Left (5, 99) :: Either (Int, Int) Char)
+-- Left (6,(10,99))
+coreleaseL :: (s -> (s', t)) -> Either (s, a) b -> Either (s', (t, a)) b
+coreleaseL f (Left (s, a)) = let (s', t) = f s in Left (s', (t, a))
+coreleaseL _ (Right b) = Right b
+
+-- | If the right branch is taken, move a value from the state wire into the payload.
+--
+-- >>> coreleaseR (\s -> (s+1, s*2)) (Right (5, 99) :: Either Char (Int, Int))
+-- Right (6,(10,99))
+coreleaseR :: (s -> (s', t)) -> Either a (s, b) -> Either a (s', (t, b))
+coreleaseR f (Right (s, b)) = let (s', t) = f s in Right (s', (t, b))
+coreleaseR _ (Left a) = Left a
+
+-- ===========================================================================
+-- GENERAL AMBIENT STATE THREADING
+-- ===========================================================================
+
+-- | Thread a state wire through a Circuit.
+--
+-- 'ambientBy' threads an additional state component alongside a circuit
+-- without the circuit having to mention it. The state wire is braided
+-- past the feedback channel so it travels "ambiently".
+--
+-- The @braid@ function swaps the state wire past the feedback channel:
+-- @t x (t s a) -> t s (t x a)@. For @(,)@, this is
+-- @\\(x, (s, a)) -> (s, (x, a))@.
+--
+-- >>> import Circuit.Circuit (Circuit(..), reify)
+-- >>> let braid (x, (s, a)) = (s, (x, a))
+-- >>> Circuit.Circuit.reify (ambientBy braid (Lift (+1) :: Circuit (->) (,) Int Int)) ("st", 5)
+-- ("st",6)
+--
+-- >>> let step (xs, ()) = (0 : xs, take 3 xs)
+-- >>> Circuit.Circuit.reify (ambientBy braid (Knot step)) ("st", ())
+-- ("st",[0,0,0])
+ambientBy ::
+  (Profunctor arr, Trace arr t) =>
+  (forall x y z. t x (t y z) -> t y (t x z)) ->
+  Circuit arr t a b ->
+  Circuit arr t (t s a) (t s b)
+ambientBy _br (Lift f) = Lift (untrace f)
+ambientBy br (Compose f g) = Compose (ambientBy br f) (ambientBy br g)
+ambientBy br (Knot k) = Knot (dimap br br (untrace k))
diff --git a/src/Circuit/Traced.hs b/src/Circuit/Traced.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Traced.hs
@@ -0,0 +1,390 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+#ifdef __GLASGOW_HASKELL__
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+#endif
+
+-- | Close and open feedback loops in a monoidal category.
+--
+-- A 'Trace' instance for a tensor @t@ specifies how to thread a value
+-- through a feedback channel:
+--
+--   * 'trace' closes the channel — eliminates the tensor and produces
+--     a plain morphism. This is where the loop semantics live.
+--
+--   * 'untrace' opens the channel — lifts a plain morphism into the
+--     tensor, leaving the feedback value untouched.
+--
+-- The trace laws (traced monoidal category axioms):
+--
+-- 1. __Naturality (tightening)__. Morphisms that don't touch the traced
+--    wire pass through freely.
+--
+--      @trace (untrace f . g . untrace h) = f . trace g . h@
+--
+-- 2. __Dinaturality (sliding)__. A morphism on the traced wire can slide
+--    from one side of the trace to the other.
+--
+--      @trace (g . untrace f) = trace (untrace f . g)@
+--
+-- 3. __Vanishing__.
+--
+--      * Unit: @trace (untrace f) = f@
+--      * Tensor: @trace (trace g) = trace (assoc . g . assoc')@
+--
+-- 4. __Yanking__. Tracing a swap is identity.
+--
+--      @trace swap = id@
+--
+-- And for 'trace' and 'untrace' specifically: @'trace' . 'untrace' = 'id'@.
+-- 'untrace' is a section of 'trace'; round-tripping through
+-- @'untrace' . 'trace'@ only recovers morphisms that were already of the
+-- form @'untrace' f@.
+--
+-- Two tensor semantics are provided, corresponding to the standard
+-- traced monoidal structures:
+--
+-- [@(,)@] A single lazy recursive binding.  @trace f b@ produces
+-- @let (a, c) = f (a, b) in c@ — the feedback value @a@ and the
+-- output @c@ are co-defined.  This is cyclic sharing, not iteration:
+-- the body executes once with a self-referential channel.
+-- Only works in a lazy setting — the feedback value is a self-referential
+-- thunk.  In a strict language this binding is circular and divergent.
+--
+-- [@Either@] A while-loop.  @Left a@ feeds back into another iteration;
+-- @Right c@ terminates.  The loop runs until a 'Right' is produced.
+--
+-- For effectful arrows, both tensors lift to 'Kleisli' @m@:
+--
+--   * @'MonadFix' m => 'Trace' ('Kleisli' m) (,)@ ties the lazy knot
+--     via 'mfix'.
+--
+--   * @'Monad' m => 'Trace' ('Kleisli' m) 'Either'@ iterates via
+--     plain recursion.  For 'IO' specifically, an overlapping instance
+--     uses GHC's delimited-continuation primops ('prompt#', 'control0#')
+--     for constant stack space.
+--
+-- /References:/
+--
+--   * Hasegawa (1997) — cartesian (cyclic-sharing) vs computational
+--     (iterative) traces.  The @(,)@/@Either@ distinction.
+--
+--   * Kidney & Wu (2026) — hyperfunctions, producer-consumer pattern.
+--
+--   * Joyal, Street & Verity (1996) — traced monoidal categories.
+module Circuit.Traced
+  ( Trace (..),
+    cellIO,
+  )
+where
+
+#ifdef __GLASGOW_HASKELL__
+import Control.Arrow (Kleisli (..))
+import Control.Monad.Fix (MonadFix, mfix)
+import Data.IORef
+import GHC.Exts (PromptTag#, control0#, newPromptTag#, prompt#)
+import GHC.IO (IO (..))
+#endif
+
+-- $setup
+-- >>> import Control.Arrow (Kleisli (..), second)
+-- >>> import Control.Category ((>>>))
+-- >>> import Data.Either (fromRight)
+-- >>> import Circuit.Traced
+
+-- | A trace over a morphism @arr@ and tensor @t@.
+--
+-- @trace@ closes the feedback loop, eliminating the tensor channel.
+-- @untrace@ opens the loop, lifting a plain morphism into the tensor.
+class Trace arr t where
+  trace :: arr (t a b) (t a c) -> arr b c
+  untrace :: arr b c -> arr (t a b) (t a c)
+
+-- * Cartesian tensor — lazy knot
+
+-- | The cartesian trace ties a lazy knot: the feedback value @a@ and
+-- output @c@ are produced simultaneously in a single recursive binding.
+--
+-- Only works in a lazy setting — the feedback value is a self-referential
+-- thunk.  In a strict language this binding is circular and divergent.
+-- Haskell's lazy evaluation makes cyclic sharing possible without
+-- mutation or explicit suspension primitives.
+--
+-- >>> :{
+-- let powers (ns, ()) =
+--       (1 : map (*2) ns, take 5 ns)
+-- :}
+--
+-- >>> trace powers () :: [Integer]
+-- [1,2,4,8,16]
+--
+-- >>> trace (\(acc, x) -> (acc, x + 1)) 5
+-- 6
+--
+-- Vanishing (a): tracing over the unit does nothing.
+--
+-- Note: using @()@ as the channel type hits a GHC black-hole detection
+-- because @()@ has only one constructor. We test with 'Int' as the
+-- channel instead — the channel value is unconstrained, so the trace
+-- degenerates to plain function application.
+--
+-- >>> let f (x, a) = (x, a + 1)
+-- >>> trace f 5
+-- 6
+--
+-- prop> \n -> trace ((\(x, a) -> (x, a + n)) :: ((Int, Int) -> (Int, Int))) (0 :: Int) == (n :: Int)
+--
+-- Yanking: tracing a swap is the identity.
+--
+-- >>> let swap (x, y) = (y, x)
+-- >>> trace swap 42
+-- 42
+--
+-- prop> \x -> trace ((\(a, b) -> (b, a)) :: ((Int, Int) -> (Int, Int))) (x :: Int) == x
+--
+-- Tightening: payload morphisms pass freely through the trace.
+--
+-- >>> let f (x, a) = (x, a)
+-- >>> trace (second (+1) . f . second (*2)) 5
+-- 11
+--
+-- prop> \x -> trace (second ((+1) :: Int -> Int) . (id :: ((Int, Int) -> (Int, Int))) . second ((*2) :: Int -> Int)) (x :: Int) == x * 2 + 1
+--
+-- Sliding: a morphism on the channel slides from one side to the other.
+--
+-- >>> let swap (x, y) = (y, x)
+-- >>> trace (second (+1) . swap) 5
+-- 6
+--
+-- >>> trace (swap . second (+1)) 5
+-- 6
+--
+-- prop> \x -> trace (second ((+1) :: Int -> Int) . ((\(a, b) -> (b, a)) :: ((Int, Int) -> (Int, Int)))) (x :: Int) == trace (((\(a, b) -> (b, a)) :: ((Int, Int) -> (Int, Int))) . second ((+1) :: Int -> Int)) x
+--
+-- Strength: an independent payload wire is invisible to the trace.
+--
+-- >>> let f (x, c) = (x, c + 1)
+-- >>> let g (x, (a, c)) = (x', (a * 2, d)) where (x', d) = f (x, c)
+-- >>> trace g (3, 5)
+-- (6,6)
+--
+-- prop> \a c -> trace ((\(x, (p, q)) -> (x, (p + a, q + 1))) :: ((Int, (Int, Int)) -> (Int, (Int, Int)))) (0 :: Int, c :: Int) == (a :: Int, c + 1)
+instance Trace (->) (,) where
+  trace f b = let (a, c) = f (a, b) in c
+  untrace = fmap
+
+-- * Either tensor — iteration
+
+-- | The Either trace iterates: 'Left' feeds back (continue), 'Right'
+-- terminates (exit). A compact, under-appreciated pattern for loops in Haskell.
+--
+-- >>> :{
+-- let fac (n, acc) | n <= 1    = Right acc
+--                  | otherwise = Left (n - 1, n * acc)
+-- :}
+--
+-- >>> trace (either fac fac) (5, 1 :: Int)
+-- 120
+--
+-- >>> :{
+-- let countdown = \case
+--       Left n | n > 0 -> Left (n - 1)
+--              | otherwise -> Right n
+--       Right n | n > 0 -> Left (n - 1)
+--               | otherwise -> Right n
+-- :}
+--
+-- >>> trace countdown (3 :: Int)
+-- 0
+--
+-- Vanishing (a): tracing over the unit does nothing.
+--
+-- >>> let f = Right . (+1) . fromRight undefined
+-- >>> trace f 5
+-- 6
+--
+-- prop> \n -> trace ((Right . (+ n) . fromRight (undefined :: Int)) :: (Either () Int -> Either () Int)) (0 :: Int) == (n :: Int)
+--
+-- Yanking: tracing a swap is the identity.
+--
+-- >>> :{
+-- let swapEither (Left x)  = Right x
+--     swapEither (Right x) = Left x
+-- :}
+--
+-- >>> trace swapEither 42
+-- 42
+--
+-- prop> \x -> trace ((\e -> case e of Left a -> Right a; Right a -> Left a) :: (Either Int Int -> Either Int Int)) (x :: Int) == x
+--
+-- Tightening: payload morphisms pass freely through the trace.
+--
+-- >>> let f = fmap ((+1) :: Int -> Int) . fmap ((*2) :: Int -> Int)
+-- >>> trace (f :: Either () Int -> Either () Int) 5
+-- 11
+--
+-- prop> \x -> trace (fmap ((+1) :: Int -> Int) . fmap ((*2) :: Int -> Int) :: Either () Int -> Either () Int) (x :: Int) == x * 2 + 1
+instance Trace (->) Either where
+  trace f b = go (Right b)
+    where
+      go x = case f x of
+        Right c -> c
+        Left a -> go (Left a)
+  untrace = fmap
+
+#ifdef __GLASGOW_HASKELL__
+
+-- * Kleisli m (,) — lazy knot via MonadFix
+
+-- | Trace for 'Kleisli' @m@ with the cartesian tensor, requiring @'MonadFix' m@.
+--
+-- The lazy knot is tied via 'mfix'. The feedback channel is lazy in the
+-- recursive binding — the body must not force the feedback value before
+-- producing it, or 'mfix' will diverge (just as the pure @(,)@ trace
+-- black-holes on strict fields).
+--
+-- >>> :{
+-- let fibs = Kleisli $ \(fibs, ()) ->
+--       pure (0 : 1 : zipWith (+) fibs (drop 1 fibs), take 3 fibs)
+-- :}
+--
+-- >>> runKleisli (trace fibs) ()
+-- [0,1,1]
+instance MonadFix m => Trace (Kleisli m) (,) where
+  trace (Kleisli f) =
+    Kleisli
+      ( \b -> do
+          (_, c) <- mfix $ \ ~(s, _) -> f (s, b)
+          pure c
+      )
+
+  untrace (Kleisli f) =
+    Kleisli
+      ( \(a, b) -> do
+          c <- f b
+          pure (a, c)
+      )
+
+-- * Kleisli m Either — iteration for any Monad
+
+-- | Trace for 'Kleisli' @m@ with the 'Either' tensor, for any @'Monad' m@.
+--
+-- Iterates by feeding 'Left' back into the step function until a 'Right'
+-- is produced. Uses plain recursion — builds stack proportional to
+-- iteration count.
+--
+-- >>> :{
+-- let countTo target = Kleisli $ \case
+--       Left n | n < target -> pure (Left (n + 1))
+--              | otherwise  -> pure (Right n)
+--       Right ()            -> pure (Left 0)
+-- :}
+--
+-- >>> runKleisli (trace (countTo (3 :: Int))) ()
+-- 3
+--
+-- This instance is @OVERLAPPABLE@: the IO-specific instance below takes
+-- priority for 'IO', providing constant-stack iteration via delimited
+-- continuations.
+instance {-# OVERLAPPABLE #-} Monad m => Trace (Kleisli m) Either where
+  trace (Kleisli f) =
+    Kleisli $ \b -> go (Right b)
+      where
+        go x = f x >>= \case
+          Right c -> pure c
+          Left a -> go (Left a)
+
+  untrace (Kleisli f) =
+    Kleisli $ \case
+      Left a -> pure (Left a)
+      Right b -> Right <$> f b
+
+-- * Kleisli IO Either — delimited continuations (constant stack)
+
+-- | GHC delimited-continuation primops.
+data PromptTag a = PromptTag (PromptTag# a)
+
+-- | Create a new prompt tag for delimited continuations.
+newPromptTag :: IO (PromptTag a)
+newPromptTag =
+  IO
+    ( \s ->
+        case newPromptTag# s of
+          (# s', t #) -> (# s', PromptTag t #)
+    )
+
+-- | Run an IO computation under a prompt boundary.
+prompt :: PromptTag a -> IO a -> IO a
+prompt (PromptTag t) (IO m) = IO (prompt# t m)
+
+-- | Captures the continuation up to the nearest prompt with the matching tag.
+control0 :: forall a b. PromptTag a -> ((IO b -> IO a) -> IO a) -> IO b
+control0 (PromptTag t) f = IO (control0# t arg)
+  where
+    arg f# s = case f (\(IO x) -> IO (f# x)) of IO m -> m s
+
+-- | Trace for 'Kleisli' 'IO' with 'Either' tensor.
+--
+-- Each iteration re-establishes the prompt boundary. When @control0@
+-- fires on @Left a@, it captures the continuation, wraps it around
+-- the next loop step, and jumps back to the prompt — constant stack.
+--
+-- >>> :{
+-- let exit42 = Kleisli $ \case
+--       Right () -> pure (Right (42 :: Int))
+-- :}
+--
+-- >>> runKleisli (trace exit42) ()
+-- 42
+instance {-# OVERLAPPING #-} Trace (Kleisli IO) Either where
+  trace (Kleisli body) =
+    Kleisli
+      ( \initial -> do
+          tag <- newPromptTag
+          let go x =
+                prompt tag $
+                  body x
+                    >>= ( \case
+                            Right c -> pure c
+                            Left a -> control0 tag (\k -> k (go (Left a)))
+                        )
+          go (Right initial)
+      )
+
+  untrace (Kleisli f) =
+    Kleisli
+      ( \case
+          Left a -> pure (Left a)
+          Right b -> Right <$> f b
+      )
+
+-- * Stateful stages via IORef
+
+-- | Create a stateful 'Kleisli' 'IO' arrow backed by 'IORef'.
+--
+-- Allocates a mutable reference once, then each invocation reads the
+-- current state, applies the transfer function, writes the new state
+-- back, and returns the output. The 'IORef' is hidden inside the
+-- arrow — callers see a pure @Kleisli IO a b@.
+--
+-- This breaks the circular dependency that 'MonadFix' requires for
+-- the 'Trace' @(,)@ instance: the feedback value is stored in the
+-- mutable cell rather than being self-referential. Strict accumulators
+-- (counters, frequency tables, running sums) work without diverging.
+cellIO
+  :: s
+  -- ^ initial state
+  -> (s -> a -> IO (s, b))
+  -- ^ transfer: current state and input yield next state and output
+  -> IO (Kleisli IO a b)
+cellIO s0 step = do
+  ref <- newIORef s0
+  pure $
+    Kleisli $ \a -> do
+      s <- readIORef ref
+      (s', b) <- step s a
+      writeIORef ref s'
+      pure b
+
+#endif