I'm trying to understand dependent types in CoC and I am having trouble finding examples that are actually carried out in CoC, specifically without inductive types or pattern matching. The most commonly used example of a dependent type seems to be that of vectors (seen as lists with a fixed number of elements), so I'm trying to write it as follows. I start with the Church encoding of naturals: $$ \textit{N} := \forall t ^ * . (t \to t) \to t \to t \\ \textit{Z} := \lambda t ^ * . \lambda s ^ {t \to t} . \lambda z ^ t . z \\ \textit{S} := \lambda p ^ N . \lambda t ^ * . \lambda s ^ {t \to t} . \lambda z ^ t . (s \ (p \ t \ s \ z)) \\ $$ For the first method, I have the following: $$ \textit{Vec} := \lambda \alpha ^ * . \lambda p ^ N . \forall t ^ {N \to *} . \forall n ^ {(t \ Z)} . \forall c ^ {\forall q ^ N . \alpha \to (t \ q) \to (t \ (S \ q))} . (t \ p) \\ \textit{Nil} := \lambda \alpha ^ * . \lambda t ^ {N \to *} . \lambda n ^ {(t \ Z)} . \lambda c ^ {\forall q ^ N . \alpha \to (t \ q) \to (t \ (S \ q))} . n \\ \textit{Cons} := \lambda \alpha ^ * . \lambda p ^ N . \lambda e ^ \alpha . \lambda r ^ {(\textit{Vec} \ \alpha \ p)} . \lambda t ^ {N \to *} . \lambda n ^ {(t \ Z)} . \lambda c ^ {\forall q ^ N . \alpha \to (t \ q) \to (t \ (S \ q))} . (c \ p \ e \ (r \ t \ n \ c)) \\ \textit{Nil} : \forall \alpha ^ * . (\textit{Vec} \ \alpha \ Z) \\ \textit{Cons} : \forall \alpha ^ * . \forall p ^ N . \alpha \to (\textit{Vec} \ \alpha \ p) \to (\textit{Vec} \ \alpha \ (S \ p)) \\ $$ This seems to work, which is already progress from the first version of my question. The part that I don't like with this solution is that for $Cons$ I need to provide both the input vector $v$ and its length $p$ even though the length is already implicit in $v$. Is there a way around that, or this is the best we can do?
Another idea would be to define $Vec$ using a polymorphic type constructor in its signature: $$ \textit{Vec} := \lambda \alpha ^ * . \forall t ^ {* \to *} . \forall u ^ * . u \to (\forall v ^ * . \alpha \to v \to (t \ v)) \to ? \\ \textit{Nil} := \lambda \alpha ^ * . \lambda t ^ {* \to *} . \lambda u ^ * . \lambda n ^ u . \lambda c ^ {\forall v ^ * . \alpha \to v \to (t \ v)} . n \\ \textit{Cons} := \lambda \alpha ^ * . \lambda e ^ \alpha . \lambda r ^ T . \lambda t ^ {* \to *} . \lambda u ^ * . \lambda n ^ u . \lambda c ^ {\forall u ^ * . \alpha \to v \to (t \ v)} . (c \ ? \ a \ (r \ t \ u \ n \ c)) \\ $$ But in this case it is not clear how to complete the definitions of $Vec$ and $Cons$. Also the signatures have become a lot more complicated and the natural number dependency is no longer visible (I suspect it can be added somehow via naturals defined over $\square$ instead of $*$).
