Introducing a dependent function in the metalanguage without pi-types
Consider the metalanguage where there are two forms of judgments:
- $\text{kind}(K)$, asserting that $K$ is a kind
- $k\in K$, asserting that $k$ is a thing of kind $K$
The family of kinds is defined as follows:
- $\text{kind}(\text{Context})$
- $\text{kind}(\text{type}(\Gamma))$ for every $\Gamma\in \text{Context}$
- $\text{kind}(\text{term}(\Gamma,A))$ for every $\Gamma\in \text{Context}$ and $A\in \text{type}(\Gamma)$
So for example if there are declarations $\frac{}{\Gamma\vdash \text{valid}}$ and $\frac{}{\Gamma\vdash U \text{ type}}$ in the object theory (where the judgment $\Gamma\vdash \text{valid}$ is a judgment of the object theory stating that $\Gamma$ is a valid context), the corresponding declarations in the metalanguage would be written as $\Gamma\in \text{Context}$ and $U\in \text{type}(\Gamma)$.
Now if I have the judgment $\frac{\Gamma\vdash A:U}{\Gamma\vdash \text{El}(A) \text{ type}}$ in the object theory, I suppose in order to declare $\text{El}$ in the metalanguage, I have to introduce a new form of judgment, namely if $\text{kind}(K)$ and $\text{kind}(K')$ then $\text{kind}(K\to K')$. With this form of judgment, I can declare $\text{El}\in \text{term}(\Gamma, U)\to \text{type}(\Gamma)$.
Now suppose I have a judgment like $\frac{\Gamma\vdash A:U\quad \Gamma \vdash a:\text{El}(A)}{\Gamma\vdash T(a):B}$. How do I declare $T$ in the metalanguage? In this case, unlike $\text{El}$, $T$ is dependent. I cannot just write $T\in \text{term}(\Gamma,U)\to \text{term}(\Gamma, \text{El}(A)) \to \text{term}(\Gamma,B)$. The first thing, $\text{term}(\Gamma,U)$, should depend on $A$ somehow. But I don't know how to implement this in the metalanguage. One could think of introducing another notation for pi-types in the metalanguage, but it would require context extensions (because the definition of pi-types requires context extensions, and I think any analog of pi-types would require them too), and there is no notion of context extension in the metalanguage. In the metalanguage we only have assertions of the form $k\in K$ and $\text{kind}(K)$. So how to implement what I want, i.e., how to introduce $T$ in the metalanguage?
0 answers
0 comment threads