Considering the "type" $\Pi x:A.\Pi y:B(x).Type$
I'm still trying to wrap my head around introducing type theories by means of LF. Suppose I declare the following constants:
$A:Type, \\ B:(El(A))Type$ and the necessary constants for the pi-type. And suppose I want to consider (in the object type theory) a family of types which depends on $x:A$ and $y:B(x)$. So I want a family $f$ such that $f(x,y):Type$ for $x:A$ and $y:B(x)$. Then this $f$ must have type
$$\Pi x:A.\Pi y:B(x).Type$$One thing that confuses me is that the above thing wouldn't be a type, and I'm having a hard time understanding what needs to be done to be able to consider such things. (Or whether it's not reasonable to consider this at all.) I suppose in LF, it would be possible to prove that $(x:El(A))(y:El(B(x)))Type$ is a kind in context ($A:Type, B:(El(A))Type$). But if so, how would this justify considering such "higher-order type" in the object theory?
I think this question is somewhat related to my previous question about Calculus of Constructions. I believe in CoC, it would be possible to derive $\Pi x:A.\Pi y:B(x).\ast : \square$ in some context. Do we need to introduce a "super-type" that contains $Type$ in order to be able to consider object of type $\Pi x:A.\Pi y:B(x).Type$? But if we impose a supertype containing $Type$, it's not clear how it would be compatible with LF, since all universes in the object type theory are of type $Type$, so $Type$ shouldn't have any supertypes as far as I understand.
1 answer
$\newcommand{\Type}{\mathsf{Type}}$ $\newcommand{\El}{\mathsf{El}}$ $\newcommand{\U}{\mathsf{U}}$ $\newcommand{\T}{\mathsf{T}}$
You would not add a supertype to $\Type$, because $\Type$ is not part of the object theory. It is the meta-theoretic object that classifies (all) the types of your object theory.
If you want to be able to internalize certain families as first-class entities, this is often done via having universes within the object theory. So, for a la Tarski universes, you add: $$\U : \Type$$ $$\T : (\El(\U))\Type$$ Along with codes in $\El(\U)$ and a specification of how $\T$ decodes them. Then, you have: $$\Pi x:A. \Pi y : B(x). \U : \Type$$ So you can have an $f$ with that type inside your theory, and it can act similarly to the families definable in LF. Essentially, $\U$ and $\T$ reflect some of the structure of $\Type$ and $\El$ into the object theory. Of course, $\U$ and $\T$ themselves cannot (consistently) be reflected within themselves, which often leads to a hierarchy of universes $\U_n$ and $\T_n$, each of which classify previous universes. All of these sit within $\Type$ in LF, though.
0 comment threads
0 comment threads