Derivability of `Vector` in pure calculus of constructions

Question

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?

Answer 1

Source 1 does not say anything about deriving the induction principle for inductive types, it's only about non-dependent recursion. Source 2 says that deriving the induction principle is not possible. So there's no conflict between the the two.

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.

This source derives induction for lambda-encoded data, using some additional assumptions (function extensionality, impredicative identity type). But even here the small-elimination restriction that I mentioned is still present, which limits the usability quite a bit.