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!
$\begingroup$
$\endgroup$
3
-
$\begingroup$ What are values? Closed terms? $\endgroup$– András KovácsDec 16, 2020 at 16:23
-
$\begingroup$ @AndrásKovács Yes. $\endgroup$– FredDec 16, 2020 at 16:29
-
1$\begingroup$ 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$? $\endgroup$– CouchyJan 7, 2021 at 13:43
Add a comment
|