Communities

Writing
Writing
Codidact Meta
Codidact Meta
The Great Outdoors
The Great Outdoors
Photography & Video
Photography & Video
Scientific Speculation
Scientific Speculation
Cooking
Cooking
Electrical Engineering
Electrical Engineering
Judaism
Judaism
Languages & Linguistics
Languages & Linguistics
Software Development
Software Development
Mathematics
Mathematics
Christianity
Christianity
Code Golf
Code Golf
Music
Music
Physics
Physics
Linux Systems
Linux Systems
Power Users
Power Users
Tabletop RPGs
Tabletop RPGs
tag:snake search within a tag
answers:0 unanswered questions
user:xxxx search by author id
score:0.5 posts with 0.5+ score
"snake oil" exact phrase
votes:4 posts with 4+ votes
created:<1w created < 1 week ago
post_type:xxxx type of post
Search help
Notifications
Mark all as read See all your notifications »
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?
You might want to add some details to your flag.
Why should this post be closed?

0 comment threads

0 answers

Sign up to answer this question »

This community is part of the Codidact network. We have other communities too — take a look!

You can also join us in chat!

Want to advertise this community? Use our templates!

Like what we're doing? Support us! Donate