lude

commit 6b985a5de3d4d311a1bb4b3e9e76d5fd738e3def
parent 73dc78e72ebf1529cfc6fcab70e199a679274774
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed, 30 Sep 2026 10:51:00 -0700

Todo: add slop on zap (functor-functor interactions)

Diffstat:
A
Todo/Zap.slop.md
 | 
57
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++

1 file changed, 57 insertions(+), 0 deletions(-)
diff --git a/Todo/Zap.slop.md b/Todo/Zap.slop.md
@@ -0,0 +1,57 @@
+## Summary
+
+**1. Your construction.** Take `L ⊣ R` with `L : V → C` and `C` copowered.
+* `zap : R x ⊙ L y → y ⊙ x`, built as `ε ∘ L(strength of R ∘ σ) ∘ (strength of L)⁻¹`, is correct.
+* The map you didn't recognize is `R`'s strength, which every V-functor between copowered categories has.
+* As a V-left adjoint, `L` preserves copowers. So `L ≅ – ⊙ c` and `R ≅ C(c, –)` with `c = L I`, and `zap` reduces to `y ⊙ ε_x` up to reshuffling.
+
+**2. Symmetry.**
+* It is essential for your signature. With `L = R = Id`, `zap` becomes a natural map `x ⊗ y → y ⊗ x`, and `Set^M` with Day convolution (`M` non-commutative) has no such map.
+* The symmetry-free form is `L(y ⊗ R x) ≅ y ⊙ L R x → y ⊙ x`: the counit with a spectator.
+* Your form is preferable because it composes. Its output has the same shape as its input, so zaps stack layerwise.
+
+**3. State/Store.** With `T = RL` and `W = LR`, the pairing `T y ⊙ W x → y ⊙ x` is `zap` applied twice: outer layers first, then inner.
+
+**4. Further generalization.** Any symmetric monoidal `D` acting on `C`, with `L : D → C` strong, works the same way. Examples include `f^* ⊣ f_*` and extension ⊣ restriction of scalars. Without an action of `D` on `C`, `zap` has no type.
+
+**5. Intuition.** Decategorifying step by step:
+* **Groups:** cancellation, `(x c⁻¹)(y c) = y x`.
+* **Residuated monoids:** an inequality, e.g. `⌊x/c⌋·(y·c) ≤ y·x`.
+* **Linear algebra:** tensor contraction via `c* ⊗ c → k`.
+
+**6. Day-convolution view.**
+* `Zap f g ≅ Hom(f ⋆ g, Id)`, so `zap` is an evaluation map, like `V* ⊗ V → k`.
+* The universal partner is `Co g = [g, Id]_⋆`. This gives `Co L ≅ R` and `Co Store ≅ State`.
+* Composition and Day convolution form a duoidal structure, which is where the laws come from.
+
+**7. Final formulation.** It covers adjunctions and the monad/comonad pairs they generate, and uses only standard concepts.
+* **For an adjunction:** `zap` is the adjoint transpose of `R`'s strength, which is exactly Kmett's `zapWithAdjunction`. By Yoneda, `Zap(R, L) ≅ Nat(LR, Id)`, with `zap` corresponding to `ε`. So `zap` is the counit repackaged, and naturality is its only law.
+* **For the generated monad/comonad:** in Katsumata–Rivas–Uustalu's monoidal category of interaction laws, `L ⊣ R` lifts to a duality between `(R, L, zap)` and `(L, R, zapʳᵉᵛ)`.
+  * The unit is `(η, ε)` and the counit is `(ε, η)`.
+  * The induced monoid `X ⊗ X*` is the State/Store pairing `(RL, LR, zap∘zap)`.
+  * Its laws come for free: `ψ(η⊗1) = 1⊗ε` and `ψ(μ⊗1) = ψ∘ψ∘(1⊗δ)`.
+* **In short:** `zap` is to the adjunction as the State/Store pairing is to the monad `RL`.
+
+## Key references
+* **Katsumata, Rivas, Uustalu, "Interaction Laws of Monads and Comonads" (LICS 2020).** This is the central formal treatment. Monad-comonad interaction laws are monoid objects in the category of functor-functor interaction laws, and functor-functor interaction laws are Chu spaces over endofunctors with Day convolution.
+* **McDermott, Rivas, Uustalu, "Sweedler Theory of Monads" (FoSSaCS 2022).** Places interaction laws in Sweedler theory for duoidal categories.
+* **Uustalu–Voorneveld (APLAS 2020); Uustalu, "Stateful Runners" (MFPS 2015); Ahman–Bauer, "Runners in Action" (ESOP 2020).** These cover the runners and comodels side.
+* **Kmett:**
+  * `Control.Functor.Zap` in category-extras, where `Zap` is described as dual functors.
+  * `zapWithAdjunction` in `adjunctions`.
+  * "Monads from Comonads" and `Control.Monad.Co`.
+* **Piponi, "Cofree meets Free" (2014).** A pairing of f and g lifts to a pairing of Cofree f and Free g.
+* **Freeman, "Comonads as Spaces" (2016).** UI components as a comonad, a monad, and a pairing between them.
+* **Hinze, "Monads from Comonads, Comonads from Monads".** Every adjunction L ⊣ R induces an adjunction −R ⊣ −L.
+
+Sources:
+- [Interaction Laws of Monads and Comonads (arXiv)](https://arxiv.org/abs/1912.13477)
+- [Sweedler Theory of Monads](https://dylanm.org/)
+- [Algebraic and Coalgebraic Perspectives on Interaction Laws](https://link.springer.com/chapter/10.1007/978-3-030-64437-6_10)
+- [Runners in action](https://arxiv.org/abs/1910.11629)
+- [Control.Functor.Zap](https://hackage.haskell.org/package/category-extras-0.53.1/docs/Control-Functor-Zap.html)
+- [Data.Functor.Adjunction](https://hackage.haskell.org/package/adjunctions-4.3/docs/src/Data-Functor-Adjunction.html)
+- [Control.Monad.Co](https://hackage.haskell.org/package/kan-extensions-5/docs/Control-Monad-Co.html)
+- [Cofree meets Free](http://blog.sigfpe.com/2014/05/cofree-meets-free.html)
+- [Comonads as Spaces](https://blog.functorial.com/posts/2016-08-07-Comonads-As-Spaces.html)
+- [Hinze, Monads from Comonads](https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/28/slides/ralf.pdf)