Newest at the top
| 2024-10-07 07:12:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 07:09:19 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:07:51 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:05:15 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-10-07 07:05:03 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 07:03:35 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 07:03:33 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2024-10-07 07:01:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 06:59:00 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 06:57:31 +0200 | youthlic | (~Thunderbi@user/youthlic) (Client Quit) |
| 2024-10-07 06:57:25 +0200 | myNameIs | (~user4561@user/myNameIs) (Ping timeout: 256 seconds) |
| 2024-10-07 06:57:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:54:50 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 06:53:21 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 06:46:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-10-07 06:45:39 +0200 | myNameIs | (~user4561@user/myNameIs) myNameIs |
| 2024-10-07 06:45:39 +0200 | myNameIs | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Changing host) |
| 2024-10-07 06:44:56 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 06:42:44 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 06:41:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:40:54 +0200 | <haskellbridge> | <Bowuigi> Oh wait the HoTT book may say something about W types lemme check |
| 2024-10-07 06:40:39 +0200 | <haskellbridge> | <Bowuigi> Yeah, lots of smart people there. Had a question about positivity and negativity of universes, they solved it fairly quickly and directed everyone with a similar question to other stuff that I yet don't understand |
| 2024-10-07 06:37:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> i haven't gone on there yet did not know it existed |
| 2024-10-07 06:37:48 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: ah good point, ty |
| 2024-10-07 06:37:04 +0200 | <haskellbridge> | <thirdofmay18081814goya> concretely wellfounded tree only implies that, given any chain of elements, that chain terminates. but it doesn't state anything about how many chains there can be |
| 2024-10-07 06:37:03 +0200 | <haskellbridge> | <Bowuigi> Btw this question is probably suitable for the HoTT Zulip |
| 2024-10-07 06:36:50 +0200 | <haskellbridge> | <Bowuigi> I do not understand this topic enough yet lol, lemme learn how this works first |
| 2024-10-07 06:36:29 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:f5b0:cd1b:e895:cf8a) (Ping timeout: 252 seconds) |
| 2024-10-07 06:35:44 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: even in classical logic i think we get that wellfounded trees can be infinitely wide |
| 2024-10-07 06:35:23 +0200 | <haskellbridge> | <Bowuigi> The "constructiveness" is what seems to make the trees possibly infinitely wide |
| 2024-10-07 06:35:01 +0200 | user4561 | myNameIs |
| 2024-10-07 06:34:29 +0200 | user4561 | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) |
| 2024-10-07 06:33:26 +0200 | <haskellbridge> | <thirdofmay18081814goya> we want wellfoundedness |
| 2024-10-07 06:33:16 +0200 | <haskellbridge> | <thirdofmay18081814goya> or a subset |
| 2024-10-07 06:33:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> because that make the tree = N |
| 2024-10-07 06:32:55 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm i think we do not want well-order |
| 2024-10-07 06:31:43 +0200 | <haskellbridge> | <Bowuigi> So W-types are supposed to be a constructive counterpart to sets with a well founded irreflexive total order |
| 2024-10-07 06:30:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 06:28:28 +0200 | <haskellbridge> | <Bowuigi> https://ncatlab.org/nlab/show/well-order assumes classical reasoning a lot lmao |
| 2024-10-07 06:27:51 +0200 | michalz | (~michalz@185.246.207.217) |
| 2024-10-07 06:26:33 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: totally ordered tree is just N |
| 2024-10-07 06:26:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:25:48 +0200 | <haskellbridge> | <Bowuigi> Not sure why can the trees be infinitely wide if the relation is a total order with a minimum element |
| 2024-10-07 06:25:43 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah wellordered trees are less structured than wellfounded trees, only the latter must have finite chains |
| 2024-10-07 06:24:13 +0200 | <haskellbridge> | <thirdofmay18081814goya> i'm not 100% how this translates to wellfoundedness |
| 2024-10-07 06:23:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> uh i meant wellfounded |
| 2024-10-07 06:23:04 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-10-07 06:22:19 +0200 | user4561 | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Quit: Client closed) |
| 2024-10-07 06:22:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> so it works for induction but i'm trying to get at computable traversal |
| 2024-10-07 06:21:46 +0200 | <haskellbridge> | <Bowuigi> Oh yeah forgot about that |