Newest at the top
| 2024-11-07 13:39:12 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-11-07 13:32:01 +0100 | <Inst> | just a strong lax monoidal functor, what's the problem? ツ |
| 2024-11-07 13:31:28 +0100 | <Inst> | didn't figure out on my own to compartmentalize them into left and right identity |
| 2024-11-07 13:31:14 +0100 | <Inst> | thanks leary |
| 2024-11-07 13:30:26 +0100 | <Leary> | Inst: Identity === /left/ identity; Interchange === /symmetry/ of identity (hence /right/ identity). Homomorphism is redundant, following from parametricity. |
| 2024-11-07 13:29:23 +0100 | longlongdouble | (~longlongd@117.234.149.253) |
| 2024-11-07 13:27:59 +0100 | longlongdouble | (~longlongd@2409:40d4:4052:dbab:1989:242:cab1:419a) (Ping timeout: 260 seconds) |
| 2024-11-07 13:24:39 +0100 | CoolMa7 | (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) CoolMa7 |
| 2024-11-07 13:18:33 +0100 | longlongdouble | (~longlongd@2409:40d4:4052:dbab:1989:242:cab1:419a) |
| 2024-11-07 13:18:06 +0100 | <Inst> | composition -> associativity of monoids, other three laws = identity quality of pure |
| 2024-11-07 13:17:27 +0100 | longlongdouble | (~longlongd@117.234.149.253) (Read error: Connection reset by peer) |
| 2024-11-07 13:17:23 +0100 | <Inst> | don't ask to ask, applicative laws? |
| 2024-11-07 13:17:17 +0100 | Inst | (~Inst@user/Inst) Inst |
| 2024-11-07 13:04:43 +0100 | longlongdouble | (~longlongd@117.234.149.253) |
| 2024-11-07 13:02:11 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2024-11-07 13:01:37 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 2024-11-07 13:00:04 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-11-07 12:59:40 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 12:56:24 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-11-07 12:54:50 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-11-07 12:52:21 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2024-11-07 12:52:21 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2024-11-07 12:52:11 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 260 seconds) |
| 2024-11-07 12:47:12 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2024-11-07 12:42:38 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 12:38:53 +0100 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-11-07 12:37:07 +0100 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-11-07 12:32:05 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2024-11-07 12:31:22 +0100 | pavonia | (~user@user/siracusa) (Read error: Connection reset by peer) |
| 2024-11-07 12:30:53 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 2024-11-07 12:27:21 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) alexherbo2 |
| 2024-11-07 12:25:58 +0100 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2024-11-07 12:23:47 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 12:20:53 +0100 | Digitteknohippie | Digit |
| 2024-11-07 12:13:11 +0100 | xff0x | (~xff0x@2405:6580:b080:900:759a:e3d6:c0c3:b78a) |
| 2024-11-07 12:11:28 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-11-07 12:10:02 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 2024-11-07 12:05:04 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2024-11-07 12:00:42 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2024-11-07 11:57:35 +0100 | Digit | (~user@user/digit) (Ping timeout: 255 seconds) |
| 2024-11-07 11:57:31 +0100 | Digitteknohippie | (~user@user/digit) Digit |
| 2024-11-07 11:53:24 +0100 | mulk | (~mulk@pd95146e9.dip0.t-ipconnect.de) mulk |
| 2024-11-07 11:53:02 +0100 | mulk | (~mulk@pd95146e9.dip0.t-ipconnect.de) (Quit: ZNC - http://znc.in) |
| 2024-11-07 11:52:06 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 11:49:56 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-11-07 11:46:28 +0100 | tomsmeding | doesn't know much about idris |
| 2024-11-07 11:46:17 +0100 | <kuribas> | idris has a proof search algorithm, but it's also fragile. |
| 2024-11-07 11:45:23 +0100 | <tomsmeding> | agda-presburger can do it but it's doubly-exponential so it runs out of memory once you have 8 variables in your formula |
| 2024-11-07 11:44:58 +0100 | <tomsmeding> | and for inequalities, well, you're on your own with the basic lemmas |
| 2024-11-07 11:44:49 +0100 | <tomsmeding> | there is an integer _equality_ solver in agda-stdlib, but you have to explicitly write out the equality that you want it to solve |