gistfile1.txt

<mietek> moobar: https://twitter.com/valeriadepaiva/status/1119238128668012544
<mietek> > I definitely do NOT like idempotent monads or comonads. c'mon "possibly possible" is much weaker than "possible". sure, they're equiprovable, but not equivalent! see discussion in sec 8 of On an Intuitionistic Modal Logic, Bierman dePaiva
<mietek> dolio: ^^
<mietek> tomjack: ^^
<mietek> https://twitter.com/valeriadepaiva/status/1119254122719350784
<mietek> > Let me say it again: why I don't like idempotent (co-)monads. the point of doing it categorically, instead of using traditional oset models, is to have equiprovable, but not isomorphic types/propositions, if desired, correct?
<mietek> i’m a bit confused
* joomy has quit (Quit: My MacBook has gone to sleep. ZZZzzz…)
* joomy (~joomy@nat-oitwireless-outside-vapornet3-140-180-248-48.princeton.edu) has joined
* joomy has quit (Client Quit)
<mietek> sclv: maybe you could explain? :)
<tomjack> maybe dePaiva noticed the Fibrational Framework talk abstract https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html ?
<tomjack> actually though the S4 [] there is not idempotent in this sense because FF took care to preserve Pfenning's similar strange inclination
<tomjack> or, well, I didn't think so, but I guess I never worked out the details and they don't actually say -- they just say that [](A x B) is not the same as []A x []B
* freeman42x (~freeman42@2a02:8084:e81:9580:45d8:640f:f1bb:50ed) has joined
* xkapastel (uid17782@gateway/web/irccloud.com/x-pywxckfblmppuqdk) has joined
<sclv> mietek: i think she's responding to a mention of idempotent monads i gave on a different thread!
<sclv> (she's not good at twitter UI)
<sclv> in particular I don't think that the constructions in the linked video are idempotent
<mietek> yeah, twitter ui can get in the sea
<sclv> but that said she's talked a lot in the past about her frustration
<mietek> but what i’m wondering most about is the distinction she’s making between "equiprovable" and "equivalent" or "isomorphic"
<sclv> that category theory can give an account of basically one family of notions of modality
<sclv> but logicians have a ton more that we don't have a clue about
<sclv> i'm not sure exactly what she's getting at with that quote either
<sclv> like i wouldn't think that's the "point" of doing it categorically
<sclv> honestly i don't even know why one would use ordered set models and not poset models
<mietek> Fish are fascinated with floating objects.
<mietek> oops, wrong window
<mietek> :D
<sclv> i remember these slides from her some years back that give some sense of her thinking: https://www.slideshare.net/valeria.depaiva/intuitionistic
* joomy (~joomy@nat-oitwireless-outside-vapornet3-140-180-248-48.princeton.edu) has joined
* joomy has quit (Client Quit)
<pgiarrusso> mietek: she's talking about proof relevance I think. If f: A -> B, g: B -> A, but f and g aren't inverses, then A and B are equiprovable but not isomorphic
<pgiarrusso> (or, f and g don't prove an isomorphism)
<pgiarrusso> 6:56 PM <sclv> like i wouldn't think that's the "point" of doing it categorically
<mietek> pgiarrusso: okay, that would make sense
<pgiarrusso> sclv: maybe her point is that the above example is impossible if the category of types/propositions and functions is a poset?
<sclv> pgiarrusso: i see, so she's saying categories give you one more level of "upto" than posets, so let you distinguish more things
<sclv> and then if you add idempotence then you just throw that away again
<pgiarrusso> haven't read her book, but that's my simplest guess
<sclv> her paper you mean?
<pgiarrusso> possibly — the cited thing (Sec. 8 of ...)
<pgiarrusso> and indeed, idempotence makes Box A and Box (Box A) actually isomorphic (tho it shouldn't make the whole category into a poset?)
<sclv> yeah, in that she points out that two different reductions of [][][]x have different proof trees
<pgiarrusso> s/reductions/deductions/ ?
<sclv> yeah, slipping between programming and logic :-)
<pgiarrusso> ack
<tomjack> even if [] is idempotent, more things might be distinguished in []A than in A, when A != []B
* wrengr_away is now known as wrengr
* silver has quit (Ping timeout: 246 seconds)
* silver ([email protected]) has joined
<pie_> I'm watching https://www.youtube.com/watch?v=73mnPBLL_20 (a talk about porting Nix/Nixpkgs to macosx), apparently macos has something like linux's seccomp capabilities "but with a nicer frontend" involving a TinyScheme dsl
<pie_> https://youtu.be/73mnPBLL_20?t=1806
* arjen-jonathan ([email protected]) has joined
* pie_ (~pie_@unaffiliated/pie-/x-0787662) has left ("Leaving")
* pie_ (~pie_@unaffiliated/pie-/x-0787662) has joined
* aarvar ([email protected]) has joined
<pgiarrusso> TIL modalities can satisfy monad laws *and finally started using it*
<pgiarrusso> Goal: classify Iris modalities as monads, comonads, applicatives and what else
* arjen-jonathan has quit (Ping timeout: 255 seconds)
* silver has quit (Read error: Connection reset by peer)
* wrengr is now known as wrengr_away
* freeman42y (~freeman42@2a02:8084:e81:9580:45d8:640f:f1bb:50ed) has joined
* xkapastel has quit (Quit: Connection closed for inactivity)
* freeman42x has quit (Ping timeout: 258 seconds)
<dolio> If it's not idempotent, why even call it a modality instead of just a (co)monad?
* MarcelineVQ has changed the topic to: -XDependentTypes | If it's not idempotent, why even call it a modality instead of just a (co)monad? | https://github.com/dpndnt/library
<dolio> I guess there's one answer I can think of, but I also don't know why not having idempotence would be 'the point'.
<dolio> Idempotence is an interesting property for a (co)monad to have.
<dolio> Even if you're keeping track of more stuff than propositions allow.
* m0rphism has quit (Ping timeout: 250 seconds)
<tomjack> I wonder what the monad is, in these models of S4 with non-idempotent []
<mietek> why would there necessarily be a monad
<mietek> unless you mean “what custom flavour of monad”
* johnw (~johnw@haskell/developer/johnw) has joined
* Solonarv ([email protected]) has joined