5
$\begingroup$

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!

$\endgroup$
3
  • $\begingroup$ What are values? Closed terms? $\endgroup$ Dec 16, 2020 at 16:23
  • $\begingroup$ @AndrásKovács Yes. $\endgroup$
    – Fred
    Dec 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$
    – Couchy
    Jan 7, 2021 at 13:43

0

You must log in to answer this question.

Browse other questions tagged .