[TYPES] How to code interesting examples in λC

[Beta Ziliani]

Hi,

In a course I'm teaching, I wanted to show the Calculus of Constructions
(a.k.a. λC) prior to jumping to the Calculus of Inductive Constructions
(CIC). However, I find myself unable to code any interesting example. In
particular, I wasn't able to Church-encode a vector, a list with *n*
elements, whose *n* is defined in the type. Or, more primitively, the
equality type. Someone knows if this is possible to do, or send me pointers
at where such problem is discussed?

Thanks,
Beta