Newest at the top
| 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 |
| 2025-02-24 12:19:43 +0100 | <euouae> | Wait, so Coq has N type universes? I thought the top of the lambda cube is CoC and Barendregt's paper says it only needs types and kinds |
| 2025-02-24 12:18:53 +0100 | random-jellyfish | (~developer@user/random-jellyfish) random-jellyfish |
| 2025-02-24 12:18:35 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 12:16:46 +0100 | <ncf> | "kind" isn't really a thing separate from type; it is in haskell because it has type erasure |
| 2025-02-24 12:16:29 +0100 | <ncf> | type theory is best learned by forgetting about haskell |
| 2025-02-24 12:15:59 +0100 | <ncf> | you need such a thing if you want every type to have a type, since Type : Type is inconsistent |
| 2025-02-24 12:15:36 +0100 | <ncf> | coq also has a countable hierarchy Type i |
| 2025-02-24 12:15:35 +0100 | <euouae> | Haskell having the deficiency that you can't directly play with kinds like you do with types, which is all I can say, I can't put it more succinctly, I need to study more |
| 2025-02-24 12:14:52 +0100 | <euouae> | It seems that both Haskell and Coq stop at 2, types and kinds, and it's good enough, especially in Coq you can formalize a ton of Math |
| 2025-02-24 12:14:18 +0100 | <euouae> | what is the significance of those? |
| 2025-02-24 12:14:08 +0100 | <ncf> | right the hott book uses a countable hierarchy |
| 2025-02-24 12:13:57 +0100 | <euouae> | but e.g. in the HoTT book in the Appendix the type universes are presented as U_1, U_2, ... and I think those are types, kinds, higher kinds, etc |
| 2025-02-24 12:13:51 +0100 | <ncf> | or do you mean universe levels? this is one of the choices you can make; you can have a MLTT with no universes, or one universe, or a countable hierarchy of universes, or crazier things |
| 2025-02-24 12:13:34 +0100 | <euouae> | I'm doing personal "research" so there's no fixed order/set of papers/articles I'm reading |
| 2025-02-24 12:13:03 +0100 | <ncf> | euouae: i think that might depend on how you present the syntax and what you mean by "order". i don't think the answer is very significant |
| 2025-02-24 12:10:45 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) (Ping timeout: 248 seconds) |
| 2025-02-24 12:09:51 +0100 | ethantwardy | (user@user/ethantwardy) (Ping timeout: 246 seconds) |
| 2025-02-24 12:08:49 +0100 | <euouae> | jackdk: thanks for the links, I will check them out. I can at least say I've seen the diagram of the first video before |
| 2025-02-24 12:08:27 +0100 | <euouae> | I don't quite grasp the significance of that. also last question I promise. thank you |