Slight contradiction between sections A.2.1 and A.2.2

[VincentSe]

The end of section A.2.1 says

It is a meta-theoretic property of the system that if x 1 :A 1 , . . . , x n :A n |-- b : B is derivable, then the context ( x 1 :A 1 , . . . , x n :A n ) must be well-formed; thus ctx- EXT does not need to hypothesize well- formedness of the context to the left of x n .

However section A.2.2 starts with rule Vble which has such a well-formed context hypothesis.

[guillaumebrunerie]

The sentence you quoted only says that the rule ctx-EXT does not need to hypothesize well-formedness of the context, it doesn’t say anything about other rules like Vble. I don’t see any contradiction here.

[VincentSe]

@guillaumebrunerie Why not remove the ctx hypothesis from rule Vble too ?

[guillaumebrunerie]

Because then the meta-theoretic property quoted above wouldn’t hold anymore. The reason it can be removed from the ctx-EXT rule is that there is another premise there whose context is the one that needs to be well-formed.

[VincentSe]

Then I think what you just said should be added at the end of section A.2.1.

Besides, this looks like an optimization that allows a HoTT compiler to type-check faster (less hypotheses to check). Pedagogically it might be less confusing to add those ctx hypotheses everywhere, even though they are sometimes redundant.

[mikeshulman]

These are quite deep waters that I think we don't want to wade very far into, nor is it worth trying to make a big change to the appendix now even if we all agreed that some other choices would have been a bit better. The purpose of the appendix is just to give some rigorous grounding of the theory for readers who insist on it.

It might be worth clarifying the sentence in question a bit, if we could think of a way to do that with a small change.

[VincentSe]

@mikeshulman How about this

In all hypotheses of all inference rules, contexts are always assumed to be well-formed. We could formalize this by adding ctx hypotheses everywhere. But first it would be tedious to read, and second it is enough to assume those ctx at the most basic rules such as Vble, then we can prove meta-theoretically that ctx's hold everywhere else.

[mikeshulman]

I don't think that's acceptable since it changes the meaning of the mathematics. Currently, contexts are not assumed to be well-formed in the premises (unless explicitly stated, as with Vble).

[cangiuli]

I don't really see a problem with the current sentence -- removing the ctx premise from Vble would require the converse of the stipulated metatheoretic property (i.e., if Gamma |- a : A is derivable then Gamma ctx).

If we wanted to elaborate, we could say something like (this is rough):

We arrange as a meta-theoretic property of the system that [...] must be well-formed, by requiring well-formedness of the context only at the leaves of a derivation (such as in the Vble rule). As a result, in the ctx-EXT rule, we can safely omit the hypothesis that the context x1,...,x{n-1} is well-formed.

[DanGrayson]

I don't really see a problem with the current sentence -- removing the ctx premise from Vble would require the converse of the stipulated metatheoretic property (i.e., if Gamma |- a : A is derivable then Gamma ctx).

I think not. The real problem is that if you remove the single premise from Vble, then it has no premises at all, and you can derive senseless things, such as x:3 |- x:3 .

[DanGrayson]

Because then the meta-theoretic property quoted above wouldn’t hold anymore. The reason it can be removed from the ctx-EXT rule is that there is another premise there whose context is the one that needs to be well-formed.

I think you meant that the metatheoretic property could not be applied here, not that it wouldn't hold.

[cangiuli]

I think not. The real problem is that if you remove the single premise from Vble, then it has no premises at all, and you can derive senseless things, such as x:3 |- x:3 .

Yes, of course you can't arrange for that converse statement to hold if you remove the hypothesis of Vble. I was suggesting why one might think that the sentence in question would imply that the hypothesis of Vble can be removed.

While I'm here, I just want to note for @VincentSe that proof assistants (generally) don't actually build derivations like the ones in A.2, so this doesn't impact actual efficiency. Nevertheless I argue against adding "Gamma ctx" hypotheses everywhere for the reason that it would obfuscate what is intended as a readable summary of the theory in question. A better option might be to globally insist that the judgment ranges only over contexts, but as Mike has said, we don't want to make big changes to the presentation.

[VincentSe]

@cangiuli

A better option might be to globally insist that the judgment ranges only over contexts

Did you mean all judgments range only on well-formed contexts ? That is indeed what I propose.

[cangiuli]

Did you mean all judgments range only on well-formed contexts ? That is indeed what I propose.

Yes, the "meta-type" of each judgment would be that Gamma is required to be a context. Then Dan Grayson's example of using Vble to conclude x:3 |- x:3 would be ungrammatical without the need for the ctx hypothesis.

However, @mikeshulman thinks that this is too big a change to make in the first edition, and I agree. So, given the current presentation, do you still find the passage in question confusing? Does a fix like my earlier suggestion clarify it?

[VincentSe]

@cangiuli My problem is answered since I know what you have in mind now. The passage is still confusing for someone who didn't read this github discussion. When you fix this is your decision, I don't mind.

[cangiuli]

@VincentSe Do you think that a local fix like the following clarifies the situation?

We arrange as a meta-theoretic property of the system that [...] must be well-formed, by requiring well-formedness of the context only at the leaves of a derivation (such as in the Vble rule). As a result, in the ctx-EXT rule, we can safely omit the hypothesis that the context x1,...,x{n-1} is well-formed.

[VincentSe]

@cangiuli Yes, sounds good.

[DanGrayson]

@cangiuli -- that sounds confusing to me. (I assume you're replacing the parenthesized sentence here:

).

1. When I read "we can safely omit the hypothesis that the context x1,...,x{n-1} is well-formed", I look in the rule for the hypothesis mentioned and it's not there. It's already been omitted! Maybe say instead: "our omission of a hypothesis that the context x1,...,x{n-1} is well-formed is safe".

2. I read "we arrange as a meta-theoretic property of the system" and wonder whether we did actually arrange it, or did it just turn out that way.

3. I read "requiring well-formedness of the context only at the leaves of a derivation" and wonder what you could mean. The leaves of a derivation are those nodes without parents, and thus they come from rules without premises, such as ctx-EMP, but that rule has no premises, so it doesn't "require" anything.

4. When I read "we can safely omit the hypothesis that the context x1,...,x{n-1} is well-formed", I wonder why anyone would regard it as "safer" if that hypothesis were added. How does one perceive a danger from its absence? (This confusion applies also to the existing text.) The rule is:

   

   Since it looks totally logical, it's hard to perceive any danger at all.

[VincentSe]

@DanGrayson @cangiuli Honestly, the easiest way to put it is getting rid of this ctx judgment. It is a simple syntactic check, not a judgment. Just define it by a trivial grammar as you define lambda-terms at the beginning of section A.1.

[DanGrayson]

No, the context judgment is just as complicated as any other judgment, and cannot be done syntactically, because the type expressions in it have to be valid types. An example of an invalid context that looks syntactically okay is ( X : U_0, Y : U_0 , x : X, y : Y, e : x =_X y ) ctx. (Here =_X is my attempt to represent the subscript for an identity type.)

[VincentSe]

@DanGrayson You are right. The 3 judgments type, equality and context are defined together by mutual recursion, which makes them difficult to understand. The details of the mutual recursion are given by the inference rules, so the meaning of rule ctx-EXT depends on rule Vble, which is given after. That's probably why all inference rules of a type system are usually presented on a single page, to insist that their definition makes an indivisible block. Then in rule ctx-EXT I would add the extra hypothesis ( x 1 :A 1 , . . . , x n-1 :A n-1 ) ctx. Although redundant in the global mutual recursion, it clarifies the intention.

[DanGrayson]

I don't see how the addition of that premise would clarify the intention, since the context ( x 1 :A 1 , . . . , x n-1 :A n-1 ) appears already in the premise x 1 :A 1 , . . . , x n-1 :A n-1 |- x n : A n, and by appearing there, it gives every impression to the reader that it is well-formed.

Maybe instead you should be arguing for separate (redundant) rules like the following rules, which reassure the reader that initial segments of judgments are judgments, too, and would reinforce and perhaps engender the impression I claimed in the first paragraph:

   (Γ,x:X) ctx
   ---------
   Γ ctx

   Γ ⊢ a : A
   ---------
   Γ ctx

   Γ ⊢ a ≡ b : A
   ---------
   Γ ⊢ a : A

   Γ ⊢ a ≡ b : A
   ---------
   Γ ⊢ b : A

Or simply state them as meta-theoretic properties, which I suspect they are.

[cangiuli]

@DanGrayson We shouldn't add these as rules, but indeed these are (should be) admissible. Also, if you have any suggestions for clarifying that passage, please suggest away!

[DanGrayson]

Okay, here's my suggestion. Replace the indicated text:

with: "The two rules allow contexts to be built up one step at a time. To add a new variable and its type to a valid context, it suffices to derive a judgment that some expression is a well-formed element of some universe. That expression can then be appended to the context, to the right of a colon, along with a new variable that is thereby declared to represent an element of that type."

I think that would be more to the point, since discussing a premise that we might have included, but didn't, seems pointless.

[cangiuli]

That text sounds good to me, but now I'm confused about what is actually confusing about the current text. I guess you're proposing two things: (1) completely excise the discussion about admissibility, and (2) explain the context rules? Was anyone confused about what the context rules meant?

[mikeshulman]

Yes, the proposed new paragraph seems unnecessary to me as well, and even potentially confusing -- in the second sentence it's not immediately clear to me that "some expression" and "its type" are the same.

I don't think it is pointless to discuss a premise that we might have included but didn't, because readers may wonder at its absence.

[mikeshulman]

How about this as a replacement for the current parenthetical (probably as a new separate paragraph):

It is a meta-theoretic fact that whenever any judgment in context Γ is derivable, so is the judgment "Γ ctx". The premises of all the rules are chosen to include just enough well-formedness hypotheses to make this fact provable, but no more. For instance, it is not necessary for ctx-EXT to hypothesize well-formedness of x_1:A_1,...,x_{n-1}:A_{n-1} as that will follow from the derivability of its premise, but it is necessary for the Vbl rule in the next section to hypothesize well-formedness of its context. This choice is only one of the many possible ways to formulate a type theory precisely, but a detailed investigation of such issues is beyond the scope of this appendix.

[VincentSe]

@mikeshulman Yes, I agree with this.

[cangiuli]

@mikeshulman Looks great to me, and thanks for adding the remark that other choices are possible! :) Tiny remarks:

• We spelled it Vble, not Vbl.
• Are you saying "meta-theoretic fact" to avoid the word "meta-theorem"?
• Is it obvious what "judgment in context Γ" means? We only have two such judgments (no "type" judgment) so we could just spell it out.

[DanGrayson]

Mike's proposal looks good to me.

[mikeshulman]

Thanks everyone, I will make a PR. @cangiuli yes I was avoiding "meta-theorem" since we don't use that phrase anywhere else. I think I'll change it to "meta-theoretic property" since that's the same phrase used in the current version.