This question is mostly for the realizabilitologists on the list. Let A be a PCA. The category of assemblies (or pers) over A has finite coproducts because any PCA contains true, false, and if-then-else. Let now A be a typed PCA (TPCA), according to John Longley. This means we have a non-empty set of types, operations * and -> on types (not necessarily freely generating the types). For each type t we have a set of values A_t. We require the K and S combinators to exist, as well as pairing and projections. We do NOT require that there be a boolean type, or a type of natural numbers. Some examples of TPCAs: - finite sets, with * and -> interpreted as cartesian product and exponential - Goedel's T - countably-based algebraic lattices - any PCA A where the type structure is then trivial and A_t = A. Assemblies over a TPCA are formed like the usual assemblies, except we have to specify underlying types. An assembly (S,t,|=) is a set S with a type t and a realizability relation |= between S and A_t. 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. Andrej
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
participants (1)
-
Andrej Bauer