Zap.slop.md (4842B)
1 ## Summary 2 3 **1. Your construction.** Take `L ⊣ R` with `L : V → C` and `C` copowered. 4 * `zap : R x ⊙ L y → y ⊙ x`, built as `ε ∘ L(strength of R ∘ σ) ∘ (strength of L)⁻¹`, is correct. 5 * The map you didn't recognize is `R`'s strength, which every V-functor between copowered categories has. 6 * 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. 7 8 **2. Symmetry.** 9 * 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. 10 * The symmetry-free form is `L(y ⊗ R x) ≅ y ⊙ L R x → y ⊙ x`: the counit with a spectator. 11 * Your form is preferable because it composes. Its output has the same shape as its input, so zaps stack layerwise. 12 13 **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. 14 15 **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. 16 17 **5. Intuition.** Decategorifying step by step: 18 * **Groups:** cancellation, `(x c⁻¹)(y c) = y x`. 19 * **Residuated monoids:** an inequality, e.g. `⌊x/c⌋·(y·c) ≤ y·x`. 20 * **Linear algebra:** tensor contraction via `c* ⊗ c → k`. 21 22 **6. Day-convolution view.** 23 * `Zap f g ≅ Hom(f ⋆ g, Id)`, so `zap` is an evaluation map, like `V* ⊗ V → k`. 24 * The universal partner is `Co g = [g, Id]_⋆`. This gives `Co L ≅ R` and `Co Store ≅ State`. 25 * Composition and Day convolution form a duoidal structure, which is where the laws come from. 26 27 **7. Final formulation.** It covers adjunctions and the monad/comonad pairs they generate, and uses only standard concepts. 28 * **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. 29 * **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ʳᵉᵛ)`. 30 * The unit is `(η, ε)` and the counit is `(ε, η)`. 31 * The induced monoid `X ⊗ X*` is the State/Store pairing `(RL, LR, zap∘zap)`. 32 * Its laws come for free: `ψ(η⊗1) = 1⊗ε` and `ψ(μ⊗1) = ψ∘ψ∘(1⊗δ)`. 33 * **In short:** `zap` is to the adjunction as the State/Store pairing is to the monad `RL`. 34 35 ## Key references 36 * **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. 37 * **McDermott, Rivas, Uustalu, "Sweedler Theory of Monads" (FoSSaCS 2022).** Places interaction laws in Sweedler theory for duoidal categories. 38 * **Uustalu–Voorneveld (APLAS 2020); Uustalu, "Stateful Runners" (MFPS 2015); Ahman–Bauer, "Runners in Action" (ESOP 2020).** These cover the runners and comodels side. 39 * **Kmett:** 40 * `Control.Functor.Zap` in category-extras, where `Zap` is described as dual functors. 41 * `zapWithAdjunction` in `adjunctions`. 42 * "Monads from Comonads" and `Control.Monad.Co`. 43 * **Piponi, "Cofree meets Free" (2014).** A pairing of f and g lifts to a pairing of Cofree f and Free g. 44 * **Freeman, "Comonads as Spaces" (2016).** UI components as a comonad, a monad, and a pairing between them. 45 * **Hinze, "Monads from Comonads, Comonads from Monads".** Every adjunction L ⊣ R induces an adjunction −R ⊣ −L. 46 47 Sources: 48 - [Interaction Laws of Monads and Comonads (arXiv)](https://arxiv.org/abs/1912.13477) 49 - [Sweedler Theory of Monads](https://dylanm.org/) 50 - [Algebraic and Coalgebraic Perspectives on Interaction Laws](https://link.springer.com/chapter/10.1007/978-3-030-64437-6_10) 51 - [Runners in action](https://arxiv.org/abs/1910.11629) 52 - [Control.Functor.Zap](https://hackage.haskell.org/package/category-extras-0.53.1/docs/Control-Functor-Zap.html) 53 - [Data.Functor.Adjunction](https://hackage.haskell.org/package/adjunctions-4.3/docs/src/Data-Functor-Adjunction.html) 54 - [Control.Monad.Co](https://hackage.haskell.org/package/kan-extensions-5/docs/Control-Monad-Co.html) 55 - [Cofree meets Free](http://blog.sigfpe.com/2014/05/cofree-meets-free.html) 56 - [Comonads as Spaces](https://blog.functorial.com/posts/2016-08-07-Comonads-As-Spaces.html) 57 - [Hinze, Monads from Comonads](https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/28/slides/ralf.pdf)