re: it's a long one about inductive definition universe levels

I installed Coq and tried it out and indeed the parameters can be anything, even types larger than the inductive type's universe itself. So that's that then, I'll fix my rules

it's a long one about inductive definition universe levels

I'm suddenly having trouble thinking about how my universe levels work... I think this is correct?

I've looked at some references and Coq's manual is the only one that says that the constructor's type's sort has to be the sort of the inductive type overall. So if I have a constructor like:

`c: B -> C -> D -> X p a`

And I have

`B -> C -> D -> X p a: Type_i`

Then that means that:

`A`

,`B`

,`C`

's types are all at most`Type_i`

- X's type is something like
`P -> A -> Type_i`

But the thing is that this doesn't quite tell me what the sorts of `P`

and `A`

are, so I'm not sure if `X`

's type should have sort `Type_{i+1}`

But in the constructor's type, the index `a`

comes from some combination of the arguments `B`

, `C`

, `D`

, and *those* have sort `Type_i`

, so surely `A`

must also have sort `Type_i`

... right?

But not the parameters... Those could be anything...

Show thread

What if I add a Prop hierarchy without actually adding any rules for proof irrelevance lol

It'll just be hanging out there nbd

You can make it impredicative or proof irrelevant if you like

I made it slightly better by using \Gamma and \Delta in places where there were ... but it's still ungood

Show thread

Back to envs, the Type Checking with Universes paper uses Θ and Ψ, but the thing I want is decidedly *not* an env, so maybe I should avoid those

That leaves Ξ Φ Ω

I find that there's a camp of people who like to use M N for terms and A B for types, and then another camp who like e for terms and \tau for types, and yet another who like t for terms ans T for types, and then the rest just mix and match from those

let. ramble

I think it's because the *type* of the fixpoint cannot use the fixpoint itself (which would be really weird), only the body, and let expressions need the assignment available to correctly check the *type* of the body

I have a feeling that a fixpoint whose type refers to the fixpoint itself is one of those Very Dependent Functions that some NuPRL paper references

let. ramble

Why don't the premises of fixpoint typing need to have the definition of the fixpoint in the environment during typing?

let. ramble

I like let definitions very much but the thing that has bothered me is that it a) it doesn't fit into the grand scheme of form/intro/elim/comp rules, and b) it affects the shape of the environment

I think it's a very profound thing, that what goes into the environment must differ due to just a new term, but the logic or math people probably have figured out what it means in the proof theory sense

In any case, it's rather underutilized, given that only the let rule uses them

Anyway it's 1:30 am and I've decided to add parameters back in because a) I know how to not have ugly substitutions everywhere now and b) the fewer conventions of yore I go against the better... for now

- pronouns
- he/him

- public acc
- @ionathanch

- website
- https://ionathan.ch

- birdsite
- https://twitter.com/ionathanch

Admin

Jon(athan)? | ionchy [jɑːnt͡ʃi] 🏳️🌈

MSc student in CS doing PL things 🇨🇦

@ionathanch on most places 🐦

PoGo: 8336 6654 0984

#WaterDrinker 💧

I have been blessed with admin powers on this instance and I will do my best not to muck things up

pfp: https://picrew.me/share?cd=6rKy0AQ4I3

header: https://doi.org/10.1145/2578855.2537850

Joined Oct 2020