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 kinds, $\ast$ and $\square$, such that $\ast: \square$; and my understanding is that in CoC, $\square$ can be regarded as a universe which contains the type $\ast$. This note talks about defining universes in LF, and to define the universe $\square$, apparently we should declare at least the following constants:
$$\square : \textbf{Type},\ T_{\square}: (El(\square))\textbf{Type}$$
(I'm not sure about the other constants from that note -- here we have only one universe, and there they have an infinite family of nested universes). Then, as far as I understand, we need to introduce a constant $a:El(\square)$ and make an assertion rule $T_\square(a)=\ast$.
I feel very unconfident with this argument. Is that really how it's done? Or did I mess something up? (I'm sure I did.)
Also, 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)?
