Explicit substitution in type theory

200 Views Asked by At

I have a basic question about the use of explicit substitution in Martin-Löf's type theory. The question originates from the reading of Tasistro's and Sommaruga's works on related topics. The basic idea is the following. Let $\Gamma$ denote a context. We define $\gamma$ as an assignment of values to the variables in $\Gamma$ and write $\gamma:\Gamma$ to denote the relation. Then we have the following rules/interpretations for hypothetical judgments $\Gamma\vdash A:\textsf{Type}$ and $\Gamma\vdash a:A$. $$\frac{\Gamma\vdash A:\textsf{Type}\quad\vdash\gamma:\Gamma}{\vdash A(\gamma):\textsf{Type}},\quad\quad\quad\frac{\Gamma\vdash a:A\quad\vdash\gamma:\Gamma}{\vdash a(\gamma):A(\gamma)}$$ My question is: are the two inference rules reversible? That is, can we have the following rules? $$\frac{\vdash\gamma:\Gamma\quad\vdash A(\gamma):\textsf{Type}}{\Gamma\vdash A:\textsf{Type}},\quad\quad\quad\frac{\vdash\gamma:\Gamma\quad\vdash a(\gamma):A(\gamma)}{\Gamma\vdash a:A}$$ Thanks in advance!