Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 4585 4586 4587 4588 4589 4590 4591 4592 4593 4594 4595 .. 5022
— 502,152 events total
2021-04-25 02:13:23 <ski> ⌜c⌝ is the unique ⌜x⌝ satisfying ⌜P x⌝)
2021-04-25 02:13:35 <ski> anyway ..
2021-04-25 02:13:46 <ski> ⌜⌞ε⌟ (F A)⌝ ∘ ⌜F (⌞η⌟ A)⌝ = ⌜F A⌝
2021-04-25 02:13:55 <ski> ⌜U M⌝ = ⌜U (⌞ε⌟ M)⌝ ∘ ⌜⌞η⌟ (U M)⌝
2021-04-25 02:14:16 <ski> or, more pointlessly
2021-04-25 02:14:26 → ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta)
2021-04-25 02:14:27 <ski> ⌜⌞ε⌟ ∘ F⌝ ∘ ⌜F ∘ ⌞η⌟⌝ = ⌜F⌝
2021-04-25 02:14:33 <ski> ⌜U⌝ = ⌜U ∘ ⌞ε⌟⌝ ∘ ⌜⌞η⌟ ∘ U⌝
2021-04-25 02:14:35 <ski> shachaf ^
2021-04-25 02:15:28 → shailangsa joins (~shailangs@host86-186-132-95.range86-186.btcentralplus.com)
2021-04-25 02:16:36 <ski> (one composition here is "vertical", the other is "horizontal" .. i've never been able to memorize which means which, of those terms)
2021-04-25 02:16:46 <shachaf> Oh, that was for me?
2021-04-25 02:16:55 <ski> last couple of lines, yes
2021-04-25 02:17:20 <shachaf> ski: I could never remember which was which until I realized those terms come from attaching string diagrams to each other horizontally and vertically.
2021-04-25 02:17:36 <shachaf> Or at least I assume they do. That's how I remember it, anyway.
2021-04-25 02:18:41 <ski> string diagrams, as in the catsters <https://www.youtube.com/watch?v=USYRDDZ9yEc&list=PLlGXNwjYhXYxKVa67r0pKuYufECy713bv&index=36>, i presume ?
2021-04-25 02:18:55 × ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 252 seconds)
2021-04-25 02:19:10 <shachaf> Yes, that style of string diagram.
2021-04-25 02:19:38 <ski> (rewatching that, to check in which way they orient stuff)
2021-04-25 02:19:50 <shachaf> Oh, I don't remember which way they orient things either.
2021-04-25 02:20:06 <shachaf> The main thing I try to do is to make my string diagrams line up with my indx notation.
2021-04-25 02:20:29 <ski> i mean, the "vertical" vs. "horizontal", would depend on whether they tend to write the arrows left-right or up-down
2021-04-25 02:20:51 <shachaf> Oh, sure, that much I do remember.
2021-04-25 02:21:01 <shachaf> Anyway, since I write "T_a^b" for a thing with input a and output b, I draw the outputs at the top and the inputs at the bottom.
2021-04-25 02:21:35 <ski> (which is one reason why i don't really like such terminology. and ditto for "left/right adjoint", "left/right inverse", &c.)
2021-04-25 02:21:51 <shachaf> Yes. Probably the Galois connection terms "lower/upper adjoint" are better.
2021-04-25 02:22:15 <shachaf> Hmm, I mean, because of the preorder, not because of low/high as in down/up.
2021-04-25 02:22:50 <ski> which would be which, in that terminology ?
2021-04-25 02:23:41 <shachaf> The left adjoint would be called lower.
2021-04-25 02:24:03 <shachaf> Looking at https://en.wikipedia.org/wiki/Galois_connection#Definitions
2021-04-25 02:24:04 <ski> if ⌜F⌝ goes to ⌜𝒞⌝ from ⌜𝒟⌝, and ⌜U⌝ goes to ⌜𝒟⌝ from ⌜𝒞⌝, which is upper and which is lower ?
2021-04-25 02:24:11 <ski> mhm
2021-04-25 02:24:43 <shachaf> Am I supposed to figure out which is which because you called one of them U?
2021-04-25 02:24:47 <ski> i guess they're focusing on the target / codomain side of the functors
2021-04-25 02:25:19 <ski> oh, sorry, i should've said that ⌜F⌝ would traditionally be called the left adjoint of ⌜U⌝
2021-04-25 02:25:33 <shachaf> Then F would be called the lower adjoint.
2021-04-25 02:25:43 <ski> right, ok
2021-04-25 02:25:56 <shachaf> Right, focusing on the codomain side, as you said.
2021-04-25 02:26:59 <ski> (which is rather easy to reach for, with a pointful formulation)
2021-04-25 02:28:18 <ski> hm, i suppose with antitone Galois connections, you'd get two flavors of them
2021-04-25 02:29:55 × falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
2021-04-25 02:31:02 × carlomagno quits (~cararell@148.87.23.7) (Quit: Leaving.)
2021-04-25 02:33:33 × mikoto-chan quits (~anass@gateway/tor-sasl/mikoto-chan) (Ping timeout: 240 seconds)
2021-04-25 02:34:52 × theDon quits (~td@94.134.91.143) (Ping timeout: 252 seconds)
2021-04-25 02:36:50 → theDon joins (~td@94.134.91.236)
2021-04-25 02:41:22 → FinnElija joins (~finn_elij@gateway/tor-sasl/finnelija/x-67402716)
2021-04-25 02:41:22 finn_elija is now known as Guest37713
2021-04-25 02:41:22 FinnElija is now known as finn_elija
2021-04-25 02:41:32 × rekahsoft quits (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Remote host closed the connection)
2021-04-25 02:41:55 → rekahsoft joins (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com)
2021-04-25 02:43:57 × Guest37713 quits (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) (Ping timeout: 240 seconds)
2021-04-25 02:44:03 × rekahsoft quits (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Remote host closed the connection)
2021-04-25 02:44:23 → rekahsoft joins (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com)
2021-04-25 02:47:14 × urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna)
2021-04-25 02:47:35 → Guest6509 joins (~laudiacay@67.176.215.84)
2021-04-25 02:51:08 → ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta)
2021-04-25 02:51:56 × Guest6509 quits (~laudiacay@67.176.215.84) (Ping timeout: 246 seconds)
2021-04-25 02:54:07 × mmfood quits (~mmfood@185.176.246.69) (Ping timeout: 252 seconds)
2021-04-25 02:55:26 × ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 246 seconds)
2021-04-25 02:59:00 × Sheilong quits (uid293653@gateway/web/irccloud.com/x-hxduuckhynlbsgsf) ()
2021-04-25 03:03:22 → ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net)
2021-04-25 03:03:40 ← seven_three parts (~user@pool-96-233-64-53.bstnma.fios.verizon.net) ("ERC (IRC client for Emacs 27.2)")
2021-04-25 03:07:52 × ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Ping timeout: 252 seconds)
2021-04-25 03:09:59 × nicholasbulka quits (~nicholasb@2601:900:4301:da0:5440:6bb8:f181:7832) (Remote host closed the connection)
2021-04-25 03:10:21 → nicholasbulka joins (~nicholasb@2601:900:4301:da0:58e6:3a0a:96a:ca2c)
2021-04-25 03:10:50 × nicholasbulka quits (~nicholasb@2601:900:4301:da0:58e6:3a0a:96a:ca2c) (Remote host closed the connection)
2021-04-25 03:11:10 → DTZUZU_ joins (~DTZUZO@207.81.119.43)
2021-04-25 03:11:30 → nicholasbulka joins (~nicholasb@2601:900:4301:da0:58e6:3a0a:96a:ca2c)
2021-04-25 03:12:54 → hexfive joins (~hexfive@50.35.83.177)
2021-04-25 03:13:22 × DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Ping timeout: 252 seconds)
2021-04-25 03:13:55 × rekahsoft quits (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Ping timeout: 252 seconds)
2021-04-25 03:16:55 × Tario quits (~Tario@201.192.165.173) (Ping timeout: 265 seconds)
2021-04-25 03:20:09 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2021-04-25 03:20:11 × nicholasbulka quits (~nicholasb@2601:900:4301:da0:58e6:3a0a:96a:ca2c) (Ping timeout: 250 seconds)
2021-04-25 03:22:22 → ddellacosta joins (~ddellacos@86.106.143.34)
2021-04-25 03:23:43 → Guest6509 joins (~laudiacay@67.176.215.84)
2021-04-25 03:25:37 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds)
2021-04-25 03:26:32 × ddellacosta quits (~ddellacos@86.106.143.34) (Ping timeout: 240 seconds)
2021-04-25 03:28:11 × Guest6509 quits (~laudiacay@67.176.215.84) (Ping timeout: 240 seconds)
2021-04-25 03:31:29 → falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net)
2021-04-25 03:33:38 → drbean_ joins (~drbean@TC210-63-209-152.static.apol.com.tw)
2021-04-25 03:35:53 → Tario joins (~Tario@201.192.165.173)
2021-04-25 03:41:12 × stree quits (~stree@68.36.8.116) (Ping timeout: 240 seconds)
2021-04-25 03:49:14 × siraben quits (sirabenmat@gateway/shell/matrix.org/x-vprvjmvshzjzwaie) (Changing host)
2021-04-25 03:49:14 → siraben joins (sirabenmat@unaffiliated/siraben)
2021-04-25 03:49:14 × siraben quits (sirabenmat@unaffiliated/siraben) (Changing host)
2021-04-25 03:49:14 → siraben joins (sirabenmat@gateway/shell/matrix.org/x-vprvjmvshzjzwaie)
2021-04-25 03:49:40 × falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
2021-04-25 03:52:14 → anandprabhu joins (~anandprab@94.203.71.143)
2021-04-25 03:52:57 → DTZUZU joins (~DTZUZO@205.ip-149-56-132.net)
2021-04-25 03:54:07 → ddellacosta joins (~ddellacos@86.106.143.216)
2021-04-25 03:54:51 → stree joins (~stree@68.36.8.116)
2021-04-25 03:55:12 × DTZUZU_ quits (~DTZUZO@207.81.119.43) (Ping timeout: 240 seconds)
2021-04-25 03:59:01 × ddellacosta quits (~ddellacos@86.106.143.216) (Ping timeout: 252 seconds)
2021-04-25 03:59:44 <zzz> i am having trouble using a package due to unresolved dependencies. the package is diagrams and the problematic dependency is base. how do we solve this?
2021-04-25 04:04:16 → Rudd0 joins (~Rudd0@185.189.115.103)
2021-04-25 04:05:07 × erisco quits (~erisco@d24-57-249-233.home.cgocable.net) (Read error: Connection reset by peer)
2021-04-25 04:06:39 × dpl_ quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 245 seconds)
2021-04-25 04:08:32 × jao quits (~jao@pdpc/supporter/professional/jao) (Ping timeout: 240 seconds)
2021-04-25 04:09:15 <zzz> https://paste.jrvieira.com/1619323742808
←Prev  Next→
Page 1 .. 4585 4586 4587 4588 4589 4590 4591 4592 4593 4594 4595 .. 5022

All times are in UTC.