Newest at the top
| 2025-02-24 23:15:58 +0100 | <EvanR> | is the precedence of Type _ really less than addition there |
| 2025-02-24 23:14:52 +0100 | <monochrom> | Bad habit from Coq I guess. You just write "Type" and it means "Type n" where n is inferred from context. So you write "Type : Type" and it is nothing paradoxical, it is inferred to be "Type n : Type n+1" |
| 2025-02-24 23:14:24 +0100 | <tomsmeding> | but if the answer to that question is "it's in U", then you might as well just destroy all Un with n >= 1, because you'll never need them, and then U = U0 because there's only one universe |
| 2025-02-24 23:14:07 +0100 | Ekho | (~Ekho@user/ekho) Ekho |
| 2025-02-24 23:13:39 +0100 | tromp | (~textual@2a02:a210:cba:8500:6ddc:c1a9:bc13:1391) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-02-24 23:13:36 +0100 | <tomsmeding> | for example U0 |
| 2025-02-24 23:13:31 +0100 | <EvanR> | shoot |
| 2025-02-24 23:13:25 +0100 | <tomsmeding> | I meant U for any Un |
| 2025-02-24 23:13:20 +0100 | <tomsmeding> | sorry |
| 2025-02-24 23:13:15 +0100 | <EvanR> | which I guess is renaming of the same thing |
| 2025-02-24 23:13:04 +0100 | <EvanR> | this second part would be easier to follow if you didn't switch from U to U0 suddenly |
| 2025-02-24 23:11:31 +0100 | <tomsmeding> | if I remember correctly, in the end, the difference is "is Π (A : U) Maybe A in U, or in U⁺?" If it's in U, then there is only one universe: all type formers just take stuff in U and the result lives in U. If it's _not_ in U, then Maybe Int will live in U0, but `Π (A : U0) Maybe A` will live in U1 because quantifying over something in U0 puts you in U0⁺ = U1 |
| 2025-02-24 23:11:03 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 2025-02-24 23:10:54 +0100 | <EvanR> | or if I can't get to the end without mentioning the universe U that I'm trying to make, it is impredicative |
| 2025-02-24 23:10:50 +0100 | Guest87 | (~Guest87@pool-98-116-140-206.nycmny.fios.verizon.net) (Client Quit) |
| 2025-02-24 23:10:36 +0100 | <EvanR> | is it like, in the course of defining a universe I first list self contained inhabitants and at the end, I say U is this thing consisting of all of the above. (a predicative presentation) |
| 2025-02-24 23:10:22 +0100 | Guest87 | (~Guest87@pool-98-116-140-206.nycmny.fios.verizon.net) |
| 2025-02-24 23:09:08 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 23:08:49 +0100 | <EvanR> | if anywhere |
| 2025-02-24 23:08:46 +0100 | <EvanR> | or where the whole type at hand lives |
| 2025-02-24 23:08:36 +0100 | <EvanR> | which universe U could be |
| 2025-02-24 23:08:30 +0100 | <ncf> | which is which what |
| 2025-02-24 23:07:53 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-02-24 23:07:49 +0100 | <EvanR> | and syntax is all there is! |
| 2025-02-24 23:07:41 +0100 | <EvanR> | but the syntax isn't forthcoming on which is which |
| 2025-02-24 23:07:23 +0100 | <EvanR> | something to do with pi types based on U |
| 2025-02-24 23:06:45 +0100 | <EvanR> | beyond that I'm still not sure how xD |
| 2025-02-24 23:06:34 +0100 | <EvanR> | (the first universe) |
| 2025-02-24 23:06:27 +0100 | <EvanR> | I see that Set is impredicative or predicative will bear on "what is in U anyway" |
| 2025-02-24 23:06:24 +0100 | tomsmeding | doesn't actually know what I'm talking about here |
| 2025-02-24 23:04:58 +0100 | <ncf> | https://coq.inria.fr/doc/v8.15/refman/language/cic.html#the-calculus-of-inductive-constructions-wi… |
| 2025-02-24 23:04:56 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 23:04:36 +0100 | <ncf> | its other one :) |
| 2025-02-24 23:04:26 +0100 | <tomsmeding> | isn't that Prop? |
| 2025-02-24 23:04:12 +0100 | <ncf> | i called it Set at first because that's how Coq calls its impredicative universe iirc |
| 2025-02-24 23:04:04 +0100 | <EvanR> | Set = U |
| 2025-02-24 23:03:40 +0100 | <ncf> | well both Set and U are what i'm calling the first universe |
| 2025-02-24 23:03:37 +0100 | <EvanR> | originally i thought Set was a category |
| 2025-02-24 23:03:06 +0100 | <EvanR> | ok your last explanation made sense, the U vs U+ thing, with the capital pi, so what does "Set is impredicative / predicative" have to do with that |
| 2025-02-24 23:02:08 +0100 | <ncf> | in haskell this lives in U (as does every type) so haskell has an impredicative universe in this sense (in fact it has Type : Type which is even stronger (and inconsistent)) |
| 2025-02-24 23:01:16 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 23:00:53 +0100 | <ncf> | that type would be written Π (A : U) Maybe A in type theory, and the question is whether this is an element of U or U⁺, where U⁺ is the successor universe of U |
| 2025-02-24 23:00:23 +0100 | <EvanR> | I retract the question then |
| 2025-02-24 23:00:16 +0100 | <EvanR> | ok |
| 2025-02-24 23:00:10 +0100 | <ncf> | impredicativity can be understood syntactically |
| 2025-02-24 22:59:43 +0100 | <EvanR> | but what are the semantics |
| 2025-02-24 22:59:28 +0100 | <EvanR> | forall a . Maybe a is syntactically a type, in haskell |
| 2025-02-24 22:59:10 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2025-02-24 22:59:10 +0100 | <ncf> | yeah there's no size issues there |
| 2025-02-24 22:58:49 +0100 | <EvanR> | it's not quantifying at all right so that's not applicable |