[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
