Re: Assemblies without coproducts?

Re: Assemblies without coproducts?

[Andrej Bauer]

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

Assemblies without coproducts?

[Andrej Bauer]

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