I would like to announce that the draft of my paper "On Free CCC" is available from ftp triples.math.mcgill.ca. The paper contains a proof of the following: Theorem: Let C be a free cartesian closed category. Then there exists a faithful structure preserving functor F:C->Set. Isn't this just the H. Friedman's completeness result for the typed lambda calculus? NO. One has also to show that in the free cartesian closed category all the arrows into the terminal object are epi. We prove the result using Mints' reductions (but with a repaired proof). Along the way we conclude also that: Mints reductions are weakly normalizing, the strategy being: first do all eta-like expansions (with the restrictions) and then beta-like reductions. To get the file (if you can read ps files) do: ftp triples.math.mcgill.ca Name: anonymous Password: "your e-mail address"
cd pub/cubric binary get frccc.ps quit
If you can't read ps files there are also frccc.dvi and frccc.tex (which needs Barr's diagram.tex macros and they are at the same ftp site except under pub/texmacros). In case of any problems I'll gladly send you a copy by regular mail. Any comments are welcome. Djordje Cubric ==============================================================================