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.
0 answers
0 comment threads