6 Jul
1994
6 Jul
'94
6:25 p.m.
I would like to make ``a point of an empty set'' and say that Friedman's completeness theorem for typed lambda calculus (with appropriate changes) implies the completeness result for free cartesian closed categories (as mentioned in a recent posting of Alex Simpson) provided that one proves first that in a free ccc all objects have a global support. One way to do that is to prove the confluence for the appropriate system of reductions. Some of the recent papers were dealing with these reductions. One can see that the completeness holds even when the free ccc has also free arrows among freely generated types. Djordje Cubric