Can we form a finite set of well typed calculus of construction terms such that any closed term can be built up from them (plus the type of large types) using only application?
I conjecture that the following four combinators suffice:
- P : T
- ∏ = λx:P. λy:(x→P). (∀a:x. ya)
- S = λx:P. λy:P. λz:P. (λa:(z→y→x). λb:(z→y). λc:z. ac(bc))
- K = λx:P. λy:P. (λa:x. λb:y. x)
(You would also need to have the above three combinators with P replaced by T, I think.)
For example, the type of m→n is ∏m(K P m n) (for closed terms m:P and n:P).