Newest at the top
| 2025-02-06 04:35:29 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-06 04:34:32 +0100 | euleritian | (~euleritia@77.23.250.232) |
| 2025-02-06 04:33:18 +0100 | agent314 | (~quassel@79.127.222.205) agent314 |
| 2025-02-06 04:33:12 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-02-06 04:32:58 +0100 | <haskellbridge> | <Bowuigi> The HoTT book (chapter 9) has something really similar to this "type-theoretic category theory book" idea I'm looking for, any other recommendations? |
| 2025-02-06 04:32:28 +0100 | anpad | (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-02-06 04:30:42 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-06 04:29:10 +0100 | <haskellbridge> | <Bowuigi> I assume the syntax is the issue here, because the standard one has somewhat odd conventions and syntax sugar. I think that having a typechecker to play with the concepts would make a difference too (I've been looking into Cubical stuff and cooltt is probably what I'm looking for in that regard) |
| 2025-02-06 04:25:39 +0100 | <haskellbridge> | <Bowuigi> Anyway, any books on category theory using type-theoretic syntax? I got through a ton of introductions and books and still couldn't wrap my head around anything more complex than a limit/colimit |
| 2025-02-06 04:24:14 +0100 | anpad | (~pandeyan@user/anpad) anpad |
| 2025-02-06 04:24:09 +0100 | <haskellbridge> | <Bowuigi> r-sta didn't give enough context, but I guess a zipper kinda fixes the issues. I don't really know what they were referring to |
| 2025-02-06 04:23:18 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 2025-02-06 04:22:46 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-02-06 04:19:45 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-06 04:19:38 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 2025-02-06 04:18:39 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2025-02-06 04:18:28 +0100 | anpad | (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-02-06 04:13:31 +0100 | tavare | (~tavare@user/tavare) tavare |
| 2025-02-06 04:11:29 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-06 04:08:55 +0100 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
| 2025-02-06 04:05:14 +0100 | anpad | (~pandeyan@user/anpad) anpad |
| 2025-02-06 04:01:28 +0100 | anpad | (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-02-06 04:01:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-02-06 04:01:06 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-02-06 03:55:38 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-06 03:54:47 +0100 | sarna | (~sarna@d168-237.icpnet.pl) sarna |
| 2025-02-06 03:54:30 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-02-06 03:52:48 +0100 | r-sta | (~r-sta@sgyl-37-b2-v4wan-168528-cust2421.vm6.cable.virginm.net) (Quit: Client closed) |
| 2025-02-06 03:52:47 +0100 | <r-sta> | argh! people talk here in indirects. despite spacetime developments. very rude. |
| 2025-02-06 03:52:04 +0100 | Inst__ | (~Inst__@2601:6c1:786:fb0:b0d9:e54c:aa23:7982) (Client Quit) |
| 2025-02-06 03:51:56 +0100 | <Inst__> | "Axiomatic Method and Category Theory", Andrei Rodin, awesome |
| 2025-02-06 03:51:52 +0100 | <r-sta> | anyone!? |
| 2025-02-06 03:51:49 +0100 | <r-sta> | makes sense? |
| 2025-02-06 03:51:42 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 276 seconds) |
| 2025-02-06 03:51:40 +0100 | <r-sta> | "if not, you just get a cursor" |
| 2025-02-06 03:51:34 +0100 | <r-sta> | "if the nother type is the same as the first, this supports recursion and leads to traversability" |
| 2025-02-06 03:51:23 +0100 | Inst__ | (~Inst__@2601:6c1:786:fb0:b0d9:e54c:aa23:7982) |
| 2025-02-06 03:51:16 +0100 | <r-sta> | "i can deconstruct your type into a value, some structure data, and another type with the rest of the data" |
| 2025-02-06 03:51:03 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-02-06 03:50:28 +0100 | <r-sta> | previously had, geti+seti = traversable, but now have only this in a special case where the deconstructed thing is the same type as the thing you deconstructed. |
| 2025-02-06 03:50:02 +0100 | <r-sta> | the best i can come up with is that, the view is not returning the type for the thing deconstructed, as the thing not-deconstructed. this means you cant go on to continually apply the deconstruction. ie, through a non, type equality, that the geti,seti paradigm is abstracted over, to settings where repeated deconstruction might not occur |
| 2025-02-06 03:49:59 +0100 | anpad | (~pandeyan@user/anpad) anpad |
| 2025-02-06 03:48:33 +0100 | <r-sta> | assuming i now have to come up with this... any suggestions? |
| 2025-02-06 03:47:52 +0100 | <r-sta> | and i dont have a type abstraction which supports this |
| 2025-02-06 03:47:51 +0100 | <r-sta> | its like "no, you view only one element" |
| 2025-02-06 03:47:32 +0100 | <r-sta> | which comes from just wanting to recurse as usual |
| 2025-02-06 03:47:18 +0100 | <r-sta> | and you have to not try to do that |
| 2025-02-06 03:47:17 +0100 | <r-sta> | "how do you expect me to deconstruct the square with the corner missing!! oh no!!" |
| 2025-02-06 03:47:05 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-06 03:46:39 +0100 | <r-sta> | something like "things that can be piecewise deconstructed, by repeated deconstruction. vs things that only support one view" |