# Explicit substitution in type theory

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!

• What are values? Closed terms? Dec 16, 2020 at 16:23
• @AndrásKovács Yes.
– Fred
Dec 16, 2020 at 16:29
• I would say yes, since the judgements $A(\gamma) : Type$ and $a(\gamma):A(\gamma)$ presuppose $\Gamma\vdash A:Type$ and $Gamma\vdash a:A$? Jan 7, 2021 at 13:43