Newest at the top
| 2025-02-24 13:43:51 +0100 | cheater_ | cheater |
| 2025-02-24 13:43:45 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 244 seconds) |
| 2025-02-24 13:43:24 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 13:41:36 +0100 | cheater_ | (~Username@user/cheater) cheater |
| 2025-02-24 13:39:13 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-02-24 13:37:52 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 13:23:08 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 13:19:28 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-02-24 13:19:09 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) jespada |
| 2025-02-24 13:18:49 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 13:16:50 +0100 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2025-02-24 13:11:33 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
| 2025-02-24 13:09:49 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-02-24 13:07:09 +0100 | ethantwardy | (user@user/ethantwardy) ethantwardy |
| 2025-02-24 13:07:03 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 13:04:18 +0100 | ash3en | (~Thunderbi@89.246.174.164) (Client Quit) |
| 2025-02-24 13:04:14 +0100 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2025-02-24 13:01:02 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-02-24 12:57:45 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds) |
| 2025-02-24 12:53:41 +0100 | random-jellyfish | (~developer@user/random-jellyfish) (Remote host closed the connection) |
| 2025-02-24 12:51:43 +0100 | nwoob | (~nikhilkau@user/nwoob) nwoob |
| 2025-02-24 12:50:59 +0100 | nwoob | (~nikhilkau@user/nwoob) () |
| 2025-02-24 12:50:49 +0100 | nwoob | (~nikhilkau@user/nwoob) nwoob |
| 2025-02-24 12:49:19 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 12:47:18 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) (Client Quit) |
| 2025-02-24 12:46:39 +0100 | euouae | (~euouae@user/euouae) () |
| 2025-02-24 12:46:12 +0100 | <euouae> | thank you! |
| 2025-02-24 12:46:10 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-02-24 12:44:11 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) jespada |
| 2025-02-24 12:41:03 +0100 | <ncf> | (the I stands for Inductive) |
| 2025-02-24 12:40:33 +0100 | <ncf> | euouae: to answer an earlier question, coq's type theory is *based* on CC but also extends it with many features. i think a better approximation is what people call "CICω", which is a pure type system with a hierarchy of ω sorts |
| 2025-02-24 12:37:13 +0100 | <euouae> | got it, I will look into those two then. thanks everyone! |
| 2025-02-24 12:34:49 +0100 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 2025-02-24 12:34:25 +0100 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-02-24 12:30:34 +0100 | <ncf> | these lecture notes are also very nicely written https://www.danielgratzer.com/courses/type-theory-s-2024/lecture-notes.pdf |
| 2025-02-24 12:30:10 +0100 | <ncf> | tough question. i think the hott book is actually a decent introduction but not everyone might agree |
| 2025-02-24 12:26:23 +0100 | <euouae> | I came across the lambda cube from some reddit post, it stayed with me (marketing? lambda cube ... cool name, there's a picture of a cube) |
| 2025-02-24 12:25:48 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 12:25:42 +0100 | <euouae> | I am confident with deeper math, but I don't know what to look at |
| 2025-02-24 12:25:19 +0100 | <euouae> | More down to earth, ncf, how should I learn some type theory? |
| 2025-02-24 12:23:57 +0100 | <ski> | (but if you want to look more into toposes, which doesn't exactly deal with type theory, more plain logic from a categorical perspective, i'd suggest starting with "Conceptual Mathematics: a first introduction to categories" by William F. Lawvere,Stephen Schanuel, first) |
| 2025-02-24 12:23:18 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 276 seconds) |
| 2025-02-24 12:23:16 +0100 | <ncf> | i have found that the lambda cube is 1. what most people trying to learn type theory end up looking at because of wikipedia and 2. not a very useful thing to think about and not something type theorists ever talk about |
| 2025-02-24 12:23:07 +0100 | <euouae> | so when you're saying to experss dtt, do you mean that fibrations are used to formalize type theory in category theory? because that sounds different from having categories provide the semantics |
| 2025-02-24 12:22:41 +0100 | <ski> | i was simultaneously looking up "Elementary Categories, Elementary Toposes" by Colin McLarty, which talks a bit about categorical logic, and internal language in a cartesian closed category |
| 2025-02-24 12:22:23 +0100 | <ski> | er .. no, sorry |
| 2025-02-24 12:21:19 +0100 | <euouae> | ski is that the right TOC? |
| 2025-02-24 12:20:18 +0100 | <euouae> | type theory is dizzying. so many different theories |
| 2025-02-24 12:20:14 +0100 | <ski> | euouae : "Categorical Logic and Type Theory" by Bart Jacobs in 1999 (<https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html>,TOC <https://www.gbv.de/dms/ilmenau/toc/119524279.PDF>) talks about using "fibrations" in category theory to express dependent type theory, categorically |
| 2025-02-24 12:19:52 +0100 | <euouae> | and I thought the calculus of constructions is what Coq uses |