Newest at the top
| 2025-02-24 22:47:03 +0100 | <lyxia> | it means that types of the form "forall A : Set..." are not sets. Sets cannot contain elements that quantify over the universe of sets. |
| 2025-02-24 22:45:53 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 22:45:16 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 2025-02-24 22:40:33 +0100 | <EvanR> | what does "Set is impredicative" mean |
| 2025-02-24 22:38:46 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 22:37:59 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-02-24 22:35:02 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 22:34:45 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 265 seconds) |
| 2025-02-24 22:30:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 22:27:45 +0100 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 2025-02-24 22:25:41 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 22:23:39 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 2025-02-24 22:22:51 +0100 | <ncf> | i know you can make sense of impredicative encodings via abstract nonsense like "if Set is impredicative then the category of sets is large-complete so the limit of the identity functor gives an initial algebra for every functor" but like... that's what i mean by weird |
| 2025-02-24 22:21:55 +0100 | <ncf> | category theory makes normal inductive types make even more sense |
| 2025-02-24 22:21:50 +0100 | Square | (~Square@user/square) (Ping timeout: 252 seconds) |
| 2025-02-24 22:20:22 +0100 | <haskellbridge> | <Bowuigi> Hinze's Generic Programming with Adjunctions illustrates this perspective quite well, with more advanced examples found in the HoTT blog |
| 2025-02-24 22:19:32 +0100 | <haskellbridge> | <Bowuigi> They are, but Category Theory makes them make sense I guess |
| 2025-02-24 22:19:13 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-02-24 22:19:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-02-24 22:18:51 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 22:14:44 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds) |
| 2025-02-24 22:14:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 22:13:27 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) justsomeguy |
| 2025-02-24 22:07:53 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 22:05:35 +0100 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 2025-02-24 22:04:43 +0100 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-02-24 22:02:55 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 21:58:00 +0100 | jespada | (~jespada@r167-61-39-77.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-02-24 21:52:52 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 2025-02-24 21:52:32 +0100 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
| 2025-02-24 21:51:47 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 21:51:29 +0100 | hsw_ | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) hsw |
| 2025-02-24 21:48:21 +0100 | zungi | (~tory@user/andrewchawk) andrewchawk |
| 2025-02-24 21:47:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 21:42:44 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-02-24 21:42:01 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 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) |