On Thu, Mar 19, 2009 at 12:40 PM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
Now, do assemblies over a tpca A have binary coproducts? If A contains a type which resembles the booleans, we can do it. But I don't see how to do it in general. It's probably a trick involving higher-order functions.
Following a (private) suggestion by Thomas Streicher, a possible candidate for a TPCA A such that Asm(A) does not have coproducts would be the TPCA whose types are lattices and monotone maps (take countable lattices if you like to worry about size). Note that taking algebraic lattices won't do because those are injective and so they'll allow us to define if-then-else by continuoulsy extending the interesting part of if-then-else (I hope someone will understand what I am saying). Also, I do not see at the moment whether we get coproducts for the TPCA of total continuous functionals over the real numbers. More precisely, let A be the finite type hierachy over the real numbers, as generated in some super- or sub-ccc of topological spaces that contains the reals. Another candidate is the "syntactic" TPCA generated by the simply typed lambda-calculus (with products) over a base type. Perhaps there is a syntactic theorem which tells us that this TPCA does not have "weak" coproducts (which is what is needed to get coproducts at the level of assemblies). Best regards, Andrej