[Ur] Ur and full dependent types system

[Alexander Gryzlov]

Hello guys,

I've recently started studying type theory hoping to use it for my
computational biology thesis. I'm quite interested in its practical
applications and Ur as an example of such.

Can anyone tell where in the lambda cube falls Ur's type system? I
understand that it is not a fully dependently typed system, but what's
missing? Type-level unions maybe?

Alex