Newest at the top
| 2025-02-24 23:23:58 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 23:23:20 +0100 | <EvanR> | parenthesized by braces, braced by brackets, and bracketed by parentheses |
| 2025-02-24 23:22:54 +0100 | <monochrom> | I guess Coq's is like "Type @{...}" so it is parenthesized, by curry braces. |
| 2025-02-24 23:19:47 +0100 | <monochrom> | But you would need the parens in Lean. :) |
| 2025-02-24 23:19:43 +0100 | <ncf> | average coq documentation experience |
| 2025-02-24 23:19:38 +0100 | <ncf> | there seems to be syntax for specifying levels explicitly but i can't tell how it works https://coq.inria.fr/doc/V8.18.0/refman/language/core/sorts.html#sorts |
| 2025-02-24 23:19:26 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-02-24 23:19:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 23:18:01 +0100 | <monochrom> | Coq does not allow you to write "Type n" or "Type (n+1)". It only lets you write "Type" and it infers the level. |
| 2025-02-24 23:17:28 +0100 | <EvanR> | do you need the parens in Coq |
| 2025-02-24 23:16:59 +0100 | <EvanR> | lol |
| 2025-02-24 23:16:56 +0100 | <EvanR> | now I won't know |
| 2025-02-24 23:16:41 +0100 | <monochrom> | "Type n : Type (n+1)" |
| 2025-02-24 23:16:34 +0100 | <monochrom> | :( |
| 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 |