Defining the two universes from Calculus of Constructions in LF
Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes are from here.
LF is a simple type system with terms of the following forms: $$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$ where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.
(Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)
It has these judgements and these and these inference rules.
In the logical framework, there is a special kind $\textbf{Type}$, each of whose objects $A$ generates a kind $El(A)$. When specifying a type theory in LF, $\textbf{Type}$ corresponds to the conceptual universe of types of the type theory to be specified, and for any type $A$, i.e., any object of kind $\textbf{Type}$, kind $El(A)$ corresponds to the collection of objects of type $A$.
I was wondering how we could specify something like the Calculus of Constructions (or something close to it) in this LF? At the very least we should have two "things", $\ast$ and $\square$, such that $\ast: \square$. Sometimes $\ast$ is referred to as the type of all types (which I interpret as a universe of level zero), and $\square$ as the type of all kinds (which I interpret as a universe of level one). This note talks about defining universes in LF. To match its notation, let $U_0 = \ast, U_1 = \square$. Then, as suggested on page 3, we need to introduce constants
$$U_0 : \textbf{Type}, \ T_0: (U_0)\textbf{Type}, \ u_0: U_1, \ U_1:\textbf{Type}, T_1: (U_1)\textbf{Type}, $$ and assert the computation rule $T_1(u_0)=U_0 : \textbf{Type}$
Is this how it's done? But I never used $El(A)$ here, is it not needed for universe specification? I mean, $El$ corresponds to $T_0$, as noted in this answer, but if we can just introduce a constant named $T_0$ (and $T_1$), do we not need $El$ at all? In fact, it seems $T_0$ not used at all (unlike $T_1$ which is used in the assertion $T_1(u_0)=U_0 : \textbf{Type}$). But then I don't understand the purpose of adding $El(A)$ in the list of admissible terms of LF...
Further, this answer also says that $U_0$ corresponds to $\textbf{Type}$, does this mean that we should have $U_0=\textbf{Type}$ instead of $U_0=\ast$? (Maybe this is not a good question, but I just want to show which aspects made me confused.)
Lastly, this may be a topic for a separate question (feel free to ignore it in this question, I can ask about that separately), but there are 2 or 4 variations for most inference rules in CoC. Here's a picture from the book "Type theory and formal proof"; each of $s_1, s_2, $ and $s$ can be either $\ast$ or $\square$. How do inference rules in LF account for all these variations (assuming that we know how to introduce pi and lambdas - this is done here)? After introducing the constants for pi and lambda, and declaring appropriate computation rules, I thought only one set of inference rules will follow from LF's inference rulles (and that one set will correspond to $s_1=s_2=\ast$ as far as I understand).
0 answers
2 comment threads