simplyfying some inference rules by removing unnecessary contexts

[danielgerigk]

No description provided.

[danielgerigk]

"simplyfying" -> "simplifying"

[cangiuli]

This is incorrect.

As discussed in A.2.2, the rules are set up in such a way that weakening is admissible; if you do not phrase the rules in an arbitrary context, then it is impossible to, for example, construct an object of type Pi x:A. U_i because this requires x:A |- U_i : U_j and U_i is only a type in the empty context.

[danielgerigk]

Oh yes, I see. I didn't realize that those ( - Wkg_1 and Wkg_2 - ) aren't proper inference rules, but only admissible ones.
But actually, wouldn't it be more convenient to make them proper inference rules?

[mikeshulman]

@cangiuli doesn't mean that these rules are admissible; what's admissible is weakening (adding a new variable to the context). Removing the arbitrary context from these rules would make weakening no longer admissible.

[danielgerigk]

Yes; by "I didn't realize that those aren't proper inference rules, but ...", I did mean Wkg_1 and Wkg_2.

[mikeshulman]

There are good reasons for weakening to be admissible, but you need a type theorist to explain them (i.e. not me), and this isn't the best place for such a conversation; perhaps hott-cafe.