# Specifying Calculus of Constructions (or something similar) 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 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)?