### 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

# Considering the "type" $\Pi x:A.\Pi y:B(x).Type$

+1
−0

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.

Why does this post require moderator attention?
Why should this post be closed? 