Newest at the top
| 2025-02-24 21:37:41 +0100 | byte | (~mu@user/byte) byte |
| 2025-02-24 21:36:22 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 21:36:17 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-02-24 21:35:29 +0100 | byte | (~mu@user/byte) (Ping timeout: 260 seconds) |
| 2025-02-24 21:32:07 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 21:31:21 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 21:26:29 +0100 | ThePenguin | (~ThePengui@cust-95-80-24-166.csbnet.se) ThePenguin |
| 2025-02-24 21:25:39 +0100 | ThePenguin | (~ThePengui@cust-95-80-24-166.csbnet.se) (Quit: Ping timeout (120 seconds)) |
| 2025-02-24 21:24:35 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-02-24 21:24:13 +0100 | euleritian | (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-02-24 21:21:17 +0100 | hgolden | (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) hgolden |
| 2025-02-24 21:20:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-02-24 21:19:33 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 2025-02-24 21:18:42 +0100 | hgolden | (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) (Remote host closed the connection) |
| 2025-02-24 21:13:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 21:12:33 +0100 | michalz | (~michalz@185.246.207.218) (Remote host closed the connection) |
| 2025-02-24 21:12:10 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-02-24 21:11:05 +0100 | peterbecich1 | peterbecich |
| 2025-02-24 21:10:43 +0100 | kuribas | (~user@2a02:1810:2825:6000:f4c8:b5d5:3a82:9bab) (Remote host closed the connection) |
| 2025-02-24 21:08:47 +0100 | peterbecich1 | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-02-24 21:07:27 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-02-24 21:04:46 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 21:00:45 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-02-24 21:00:02 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-02-24 20:59:41 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:58:24 +0100 | zungi | (~tory@user/andrewchawk) (Ping timeout: 264 seconds) |
| 2025-02-24 20:58:00 +0100 | <ncf> | impredicative encodings are just so weird |
| 2025-02-24 20:52:58 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 272 seconds) |
| 2025-02-24 20:51:32 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-02-24 20:50:31 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-02-24 20:50:30 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 20:48:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 20:47:09 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 246 seconds) |
| 2025-02-24 20:46:03 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 20:43:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:42:00 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 20:40:04 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 260 seconds) |
| 2025-02-24 20:38:59 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-02-24 20:36:05 +0100 | <EvanR> | Agda = U1, U2, U3, ... U_top1, U_top2, Utop3, ... |
| 2025-02-24 20:33:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-02-24 20:33:23 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 20:28:18 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds) |
| 2025-02-24 20:28:10 +0100 | <haskellbridge> | <Bowuigi> Agda has a hierarchy of top universes, but you can't use level polymorphism on them |
| 2025-02-24 20:28:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:27:15 +0100 | <haskellbridge> | <Bowuigi> EvanR Well, it depends on the kind of top universe, if it is truly the top, it must have type in type or similar. If it isn't, then it belongs to an inaccessible universe. I think it would be sound in the second case (not on the first tho) |
| 2025-02-24 20:21:54 +0100 | plitter | (~plitter@user/plitter) plitter |
| 2025-02-24 20:20:05 +0100 | plitter | (~plitter@user/plitter) (Ping timeout: 252 seconds) |
| 2025-02-24 20:18:28 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-02-24 20:17:37 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-02-24 20:17:10 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |