Newest at the top
| 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 |
| 2025-02-24 12:08:11 +0100 | <euouae> | I know for the lambda cube only two sorts are used, types and kinds, say |
| 2025-02-24 12:07:43 +0100 | <euouae> | Does MLTT have sorts of order N? Or just 2? |
| 2025-02-24 12:06:21 +0100 | <ncf> | every model of MLTT is a locally cartesian closed category because that's the structure you need to interpret the basic features of a type theory; but the models may also have more structure to account for the other features |
| 2025-02-24 12:05:36 +0100 | <ncf> | they don't |
| 2025-02-24 12:03:02 +0100 | <euouae> | is it like a common core? |
| 2025-02-24 12:02:56 +0100 | <euouae> | Then how come they all have the same CCC models? |
| 2025-02-24 12:02:45 +0100 | <ncf> | multiple; there are several choices you can make and features you can add |
| 2025-02-24 12:00:20 +0100 | fp1 | fp |
| 2025-02-24 12:00:19 +0100 | fp | (~Thunderbi@130.233.70.89) (Ping timeout: 260 seconds) |
| 2025-02-24 12:00:14 +0100 | <euouae> | and is that a single theory or multiple? |
| 2025-02-24 12:00:01 +0100 | <ncf> | nlab usually means martin-löf type theory |
| 2025-02-24 11:59:42 +0100 | <euouae> | e.g. the lambda cube has several, not just CoC at the top |
| 2025-02-24 11:59:33 +0100 | <euouae> | I see. What is meant by dependent type theory? This is another naive question. I know what a dependent type is vaguely, but I don't think there's a single "theory", that's why I'm asking |
| 2025-02-24 11:58:41 +0100 | <ncf> | yes |
| 2025-02-24 11:57:52 +0100 | fp1 | (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) fp |
| 2025-02-24 11:57:37 +0100 | <euouae> | I mean *those certain* categories that are specified |
| 2025-02-24 11:56:40 +0100 | <euouae> | ncf: when that link says categories provide the semantics, does it mean that categories are models for type theories? |
| 2025-02-24 11:56:29 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |