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

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.

$$(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.

• Thanks! I'm not sure if I understand how the argument "the rule for dependent products expects a kind for the domain" is applied to see that the original expression isn't well-formed. If you're talking about the first rule in fig. 9.2, then I can't see how it's applicable. But I played around with inference rules and to me it looks like we must have $(El(A))Type$ instead of $(A)Type$ because it wouldn't be possible to deduce $\Gamma, A:Type \vdash (A)Type \textbf{ kind}$, whereas it is possible to deduce $\Gamma, A:Type \vdash (El(A))Type \textbf{ kind}$.
– user1048887
Commented Mar 27, 2023 at 15:24