### Communities

tag:snake search within a tag
user:xxxx search by author id
score:0.5 posts with 0.5+ score
"snake oil" exact phrase
created:<1w created < 1 week ago
post_type:xxxx type of post
Q&A

# Defining the two universes from Calculus of Constructions in LF

+1
−0

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).

Why does this post require moderator attention?