λ(t : Type) → < t : t >.t