Here is an extremely neat definition of dependent lenses I've never seen before, as kleisli morphisms of the extension (ie. the equivalence of categories from containers to polynomial functors) considered as some exotic kind of generalised monad
julesh
@julesh.mathstodon.xyz.ap.brid.gy
301 followers 0 following 1.8K posts
Applied Compositional Thinking 🌉 bridged from ⁂ mathstodon.xyz/@julesh, follow @ap.brid.gy to interact
![pd : (PDMove * PDMove) -> Bool
pd = extract $ CalcWith $
|~ ((PDMove * PDMove) :- Bool)
<~ (PDMove :- Bool) // (PDMove :- Bool)
... and
<~ Game (PDMove :- Nat) // Game (PDMove :- Nat)
... select {c = PDMove :- Nat} (argmax [C, D]) ~//~ select {c = PDMove :- Nat} (argmax [C, D])
<~ Game ((PDMove :- Nat) // (PDMove :- Nat))
... nash {c = PDMove :- Nat, d = PDMove :- Nat}
<~ Game End
... mapGame {c = (PDMove :- Nat) // (PDMove :- Nat)} (costate pdPayoffs)
<~ End
... runGame](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:sueerx3lvdeq7q424rvbd6l7/bafkreiafn7ixh6nsuqafze3csvs4d23wyseryixeundqiylstore3ogb5e)
