Newest at the top
| 2024-10-07 07:23:47 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 07:20:25 +0200 | <haskellbridge> | <Bowuigi> So if every "B(a)" corresponds to a type with a finite amount of constructors (like an n-Set or "Fin n"), every node must have a finite amount of branches, thus becoming finitely wide and fully traversable in a finite amount of steps |
| 2024-10-07 07:19:50 +0200 | <haskellbridge> | <thirdofmay18081814goya> am reading |
| 2024-10-07 07:18:02 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:c0b2:cecc:790e:8587) |
| 2024-10-07 07:17:55 +0200 | <haskellbridge> | <Bowuigi> Quoting, "The W type "W (a : A) B(a)" can thus be thought of as the type of well-founded trees, where nodes are labeled by elements of "A" and each node labeled by "a : A" has "B(a)"-many branches" |
| 2024-10-07 07:17:21 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-10-07 07:17:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 07:15:34 +0200 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya It has an entire section on them (5.3), short answer, if you have a W type "W (a : A) B(a)" you just have to make every result of "B(a)" a finite type |
| 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 |