1
$\begingroup$

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:

enter image description here

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.

$\endgroup$

1 Answer 1

0
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ 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}$. $\endgroup$
    – user1048887
    Commented Mar 27, 2023 at 15:24

You must log in to answer this question.