# Derivability of Vector in pure calculus of constructions

I am learning pure type systems to better understand functional (and general) programming.

My question arises mainly from the two facts:

1. It is known that we can define (co)inductive types in pure System-Fw (see Recursive types for free).

2. At the same time, it is known that we cannot come up with an inductive encoding that would allow us to derive the induction principle in $$\lambda P2$$ (see Induction Is Not Derivable in Second Order Dependent Type Theory).

My question is: is it true that we cannot define an (inhabited) dependent inductive type (e.g Vector from Idris)

data Vect : Nat -> Type -> Type where
Nil  : Vect Z a
Cons : a -> Vect k a -> Vect (S k) a


and pattern match on it similarly to pattern matching on Sum types in (1) in a pure type system such as Calculus of Constructions?

Note though that even the recursion principle that's derivable in source 2, is weaker than the recursion principle that would be definable in a type theory with a universe hierarchy of more than one universe. That's because the encoding only allows computing elements of small types by recursion. For instance, the lambda-encoding does not allow a recursively defined Bool -> Set function, where Bool : Set and Set itself is in some larger universe.