# Type equivalence in $\lambda\underline\omega$ under lambda abstraction

I'm going through "Type Theory and Formal Proof" by Nederpelt and Geuvers and just trying to play around with $$\lambda\underline\omega$$ after reading the chapter on it to better grasp the material. The text is a bit vague on some formalities, so I have a couple of questions.

Consider the term $$t = \lambda x : ((\lambda \alpha : *. \alpha) nat). x$$ (assuming $$nat : *$$ is in context). Can type-level abstractions and applications be used like this under lambda abstraction type annotations? So, is $$t$$ a valid term?

If it is, then clearly its type is $$(\lambda \alpha : *. \alpha) nat \rightarrow (\lambda \alpha : *. \alpha) nat$$, which is $$\beta$$-equivalent to $$nat \rightarrow nat$$. But how does $$t$$ relate to $$\lambda x:nat.x$$? In other words, can $$\beta$$-reduction be done under the lambda abstraction type annotation?

• What do $nat$ and $*$ denote here? – Berci Dec 26 '18 at 2:34
• $nat$ is some type of the kind $*$, and $*$ is, well, the kind of usual types (the ones you'd also encounter in STLC). – 0xd34df00d Dec 26 '18 at 2:36
• Ah, so you want a 'varying type' or some, i.e. a lambda expression for the type part (after the colon). I think it has another formalism on that part (maybe 'dependent types') and lambda expressions are only for terms.. But I'm not a lambda calculus expert.. – Berci Dec 26 '18 at 3:24
• Yep, that's types dependent on types (basically STLC lifted to the type level). – 0xd34df00d Dec 26 '18 at 4:25