Newest at the top
| 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 |
| 2025-02-24 22:58:33 +0100 | <EvanR> | Int is a type, Maybe Int is a type |
| 2025-02-24 22:58:14 +0100 | <ncf> | yes, universes of types are the things that can be impredicative or not |
| 2025-02-24 22:57:59 +0100 | <EvanR> | is that right |
| 2025-02-24 22:57:54 +0100 | <EvanR> | so you're talking about universes of types |
| 2025-02-24 22:57:46 +0100 | <EvanR> | but the word Sets earlier was plural |
| 2025-02-24 22:57:20 +0100 | <EvanR> | not stuff like 1, 3, 4, 7 |
| 2025-02-24 22:57:06 +0100 | <ncf> | that's a type |
| 2025-02-24 22:57:06 +0100 | <EvanR> | but going back, you're saying the elements are actually stuff like Int |
| 2025-02-24 22:56:44 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-02-24 22:56:43 +0100 | <EvanR> | a family of types ? |