Establishing $\Gamma, A: Type \vdash (A)Type\ \textbf{kind}$ in LF

Question

This is a follow-up to my previous question. Consider the same LF as in that question:

LF is a simple type system with terms of the following forms: $$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$ where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.

(Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)

There are five forms of judgements in LF:

And then he gives rules for infering judgements in LF (one and two).

Suppose we introduce the constant $\Sigma$: $$\Sigma: (A:Type)(B:(A)Type)Type$$

Originally I wanted to deduce the following inference rule: $$\dfrac{\Gamma \vdash A \ type \qquad \Gamma, x:A \vdash B \ type}{\Gamma \vdash \Sigma x:A.B \ type}$$ from the rules provided in LF, but then I realized that what I did was in fact an attempt to prove that $(A:Type)(B:(A)Type)Type$ is a kind (which I believe should be the case). Here's my attempt to prove this:

I started with the following (it follows from the first rule in "Dependent product kinds" and the first rule in "The kind type" here):

$$\dfrac{\Gamma \vdash Type\ \textbf{kind} \qquad \Gamma, A:Type \vdash (B: (A)Type)Type \ \textbf{kind}}{\Gamma \vdash (A:Type)(B:(A)Type)Type \ \textbf{kind}}$$

Now I need to prove that $\Gamma, A:Type \vdash (B: (A)Type)Type \ \textbf{kind}$. So I need to deduce the following:

$$\dfrac{\Gamma, A: Type \vdash (A)Type\ \textbf{kind} \qquad \Gamma, A:Type, B:(A)Type \vdash Type \ \textbf{kind}}{\Gamma, A:Type \vdash (B: (A)Type)Type \ \textbf{kind}}$$

Now I need to prove both

$\Gamma, A: Type \vdash (A)Type\ \textbf{kind}$

and

$\Gamma, A:Type, B:(A)Type \vdash Type \ \textbf{kind}$.

But I don't see how to prove either of these things. For example, to prove the former, I believe I need to establish the following:

$$\dfrac{\Gamma \vdash A\ \textbf{kind} \qquad \Gamma, x:A \vdash Type \ \textbf{kind}}{\Gamma, A:Type \vdash (A)Type \ \textbf{kind}}$$ but I don't know why $\Gamma \vdash A\ \textbf{kind}$ would be the case, and proving that $\Gamma, x:A \vdash Type \ \textbf{kind}$ would require some kind of weakening rule, which I can't see in the list of rules of LF. So how do I proceed?

P.S. As I mentioned, my original goal was to prove the sigma type introduction rule, but I guess I should create a separate question for that. For now I can't see how that can be proved, and I don't believe the work I did above is directly relevant, but if that is not so, let me know.

Answer 1

$(A:Type)(B:(A)Type)Type$ isn't well-formed according to the rules you posted. The following works instead: $(A:Type)(B:(El(A))Type)Type$. The rule for dependent products expects a kind for the domain. $A : Type$ is not $\mathbf{kind}$, only $El(A)$ is.

For $\Gamma, A:Type, B:(A)Type \vdash Type \ \textbf{kind}$, first we need to analogously fix the context to

$$\Gamma, A:Type, B:(El(A))Type \vdash Type \ \textbf{kind}$$

Now the rule from figure 9.2 applies which says that $\Gamma \vdash Type\,\mathbf{kind}$ for any valid $\Gamma$.

Weakening is not needed here, but it should be assumed somewhere, because otherwise the system doesn't quite work.