Newest at the top
| 2026-06-29 02:47:19 +0000 | ft | (~ft@p508dbc65.dip0.t-ipconnect.de) ft |
| 2026-06-29 02:46:27 +0000 | ft | (~ft@p3e9bcfda.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2026-06-29 02:41:26 +0000 | ft | (~ft@p3e9bcfda.dip0.t-ipconnect.de) ft |
| 2026-06-29 02:39:30 +0000 | ft | (~ft@p3e9bcc42.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2026-06-29 02:37:51 +0000 | schuelermine | (~Thunderbi@user/schuelermine) (Ping timeout: 252 seconds) |
| 2026-06-29 02:35:58 +0000 | <monochrom> | I think no. I forgot what I used. |
| 2026-06-29 02:29:59 +0000 | td_ | (~td@i53870922.versanet.de) |
| 2026-06-29 02:28:04 +0000 | td_ | (~td@i53870910.versanet.de) (Ping timeout: 252 seconds) |
| 2026-06-29 02:24:44 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-29 02:20:18 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 265 seconds) |
| 2026-06-29 02:15:30 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-29 01:48:55 +0000 | ft | (~ft@p3e9bcc42.dip0.t-ipconnect.de) ft |
| 2026-06-29 01:47:26 +0000 | ft | (~ft@p3e9bccce.dip0.t-ipconnect.de) (Ping timeout: 265 seconds) |
| 2026-06-29 01:18:08 +0000 | xff0x_ | (~xff0x@2405:6580:b080:900:2b7:99fc:bbb9:7b1b) (Ping timeout: 244 seconds) |
| 2026-06-29 01:17:56 +0000 | Everything | (~Everythin@static.208.206.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2026-06-29 01:12:56 +0000 | <schuelermine> | so is the adjoint Two ⊢ Id? |
| 2026-06-29 01:06:52 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: dnvln) |
| 2026-06-29 01:06:25 +0000 | czan | (~czan@user/mange) czan |
| 2026-06-29 00:58:08 +0000 | vgtw | (~vgtw@user/vgtw) vgtw |
| 2026-06-29 00:55:37 +0000 | vgtw | (~vgtw@user/vgtw) (Ping timeout: 276 seconds) |
| 2026-06-29 00:44:07 +0000 | mikess | (~sam@S010664777dafd303.cg.shawcable.net) (Ping timeout: 265 seconds) |
| 2026-06-29 00:34:48 +0000 | ttybitnik | (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 2026-06-29 00:33:03 +0000 | finsternis | (~X@23.226.237.192) finsternis |
| 2026-06-29 00:26:17 +0000 | xff0x | (~xff0x@2405:6580:b080:900:f87a:2927:c6fc:9f80) (Ping timeout: 248 seconds) |
| 2026-06-29 00:24:56 +0000 | xff0x_ | (~xff0x@2405:6580:b080:900:2b7:99fc:bbb9:7b1b) |
| 2026-06-29 00:07:09 +0000 | <monochrom> | Err, Two is the diagonal functor itself heh. |
| 2026-06-28 23:52:51 +0000 | weary-traveler | (~user@user/user363627) (Ping timeout: 252 seconds) |
| 2026-06-28 23:50:46 +0000 | acidjnk | (~acidjnk@p200300d6e74def721d5abc156f9177ce.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2026-06-28 23:50:44 +0000 | acidjnk_new3 | (~acidjnk@p200300d6e74def721d5abc156f9177ce.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-06-28 23:50:14 +0000 | user363627 | (~user@user/user363627) user363627 |
| 2026-06-28 23:47:04 +0000 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) youngfrog |
| 2026-06-28 23:45:15 +0000 | <EvanR> | Functor + ContraFunctor was the one that requires triviality |
| 2026-06-28 23:44:40 +0000 | <schuelermine> | I see |
| 2026-06-28 23:44:20 +0000 | <EvanR> | it's both |
| 2026-06-28 23:43:27 +0000 | <monochrom> | Perhaps it's both. |
| 2026-06-28 23:43:09 +0000 | <monochrom> | (That was what I spent one hour on. To obtain a formula for join, I factored Two, then used the well-known formula from the factoring.) |
| 2026-06-28 23:42:37 +0000 | <schuelermine> | monochrom: I thought Stream was a comonad |
| 2026-06-28 23:41:49 +0000 | <monochrom> | There is a pun/irony in this. Every monad can be factored as the composition of a pair of adjoint functors. If you do this to Two or Stream, the corresponding "diagonal functor" shows up. |
| 2026-06-28 23:38:34 +0000 | <monochrom> | To be sure, the slick way is, just like (a,a) being Bool->a, Stream a is Natural->a. |
| 2026-06-28 23:36:15 +0000 | <monochrom> | haha |
| 2026-06-28 23:35:56 +0000 | <EvanR> | yeah but (b,x) is also a diagonal see xD (one that the infinite matrix doesn't have) |
| 2026-06-28 23:35:29 +0000 | <monochrom> | Analogously, if you write (a,b) and (x,y) on two rows and see a 2x2 matrix, (a,y) is the diagonal. |
| 2026-06-28 23:34:28 +0000 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Ping timeout: 256 seconds) |
| 2026-06-28 23:34:14 +0000 | <monochrom> | Or rather, the two identity laws want join to take the diagonal. |
| 2026-06-28 23:33:42 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2026-06-28 23:33:39 +0000 | <monochrom> | Stream (Stream a) is a infinite matrix. join will want its diagonal. |
| 2026-06-28 23:33:15 +0000 | <monochrom> | Now generalize to "data Stream a = S a (Stream a)"! |
| 2026-06-28 23:31:31 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 245 seconds) |
| 2026-06-28 23:30:35 +0000 | <EvanR> | (A,B) is the type which keeps on giving |
| 2026-06-28 23:29:42 +0000 | <monochrom> | :) |