Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$

Question

Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are given here.

Intuitively, as far as I understand, this inhabitant should have the form $\lambda x:A.\lambda y:B(x). P(x,y)$ for some $P: A\to B(x)\to \ast$. (If this is not right, let me know.)

Formally, I got to this point. So I proved that $\lambda y:B(x). P(x,y) : \Pi y:B(x).\ast$ in a certain context. But then I cannot abstract over $x:A$ because the "flag" (assumption) $P:A\to B(x)\to \ast$ doesn't let me do so. And I cannot move this flag before the flag "$x:A$" because I must assume $x:A$ before assuming $P: A\to B(x) \to \ast$ since $B(x)$ depends on $x:A$. What should I do in this situation?

Answer 1

Since you are asking to find any inhabitant, how about $\lambda (x : A). \lambda y : B(x). A$?

In other words, we take $P := \lambda (u : A) . \lambda (v : B u) . A$. It looks like part of your problem is that you want somehow to use an unspecified $P$.