Newest at the top
| 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 ? |
| 2025-02-24 22:56:12 +0100 | <EvanR> | I don't know how to comprehend forall a . Maybe a |
| 2025-02-24 22:55:53 +0100 | <tomsmeding> | Int is a set. Maybe Int is a set. Is `forall a. Maybe a` a set? |
| 2025-02-24 22:55:46 +0100 | <EvanR> | and the element is doing quantification somehow |
| 2025-02-24 22:55:45 +0100 | <ncf> | the elements/terms/inhabitants of a universe are types |
| 2025-02-24 22:55:39 +0100 | <EvanR> | So you have some sets, and now we're talking about elements |
| 2025-02-24 22:55:20 +0100 | <EvanR> | "Sets can contain elements that quantify ..." |
| 2025-02-24 22:55:13 +0100 | <tomsmeding> | EvanR: the "quantify" is essential there |
| 2025-02-24 22:55:01 +0100 | <ncf> | Set is just a universe here |
| 2025-02-24 22:54:53 +0100 | <ncf> | huh |
| 2025-02-24 22:54:26 +0100 | <EvanR> | like in set theory? |
| 2025-02-24 22:54:20 +0100 | <EvanR> | the elements of sets are sets? |
| 2025-02-24 22:54:19 +0100 | <ncf> | https://dl.acm.org/doi/pdf/10.1145/3209108.3209130 section 2 has a definition |