Pratt's construction

Pratt's construction

[categories]

Date: Wed, 30 Jul 1997 16:30:49 -0400
From: Michael Barr <barr@triples.math.mcgill.ca>

Since Vaughan insists on doing these things in terms of matrices and
we benighted mathematicians insist on thinking in terms of pairings,
I thought it might be helpful to describe what he did in those
terms.  First off, he erred in writing Chu instead of chu.  So it is
the separated extensional part.  I will describe it for chu(Set,2),
since nothing much changes for other values of K except you get more
dinats.  

I will describe three types of objects.  If A = (A_1,A_2) is an
object, I will say that A_1 is the set of points and A_2 the set of
states and treat A_2 as a set of subsets of A_1.  I will say that A
is type I if there is a point in no state AND if the empty set is a
state.  I will say that A is of type II if there is a point in every
state and if the whole of A_1 is a state.  These would appear to be
quite different, but they are exchanged by the non-trivial
automorphism of 2, which means they have the same properties.  All
remaining objects will be of type III.  The first observation is
that the type is invariant under formation of A -o A.  That is, A -o
A has the same type as A.  Second, if A and B are of different
types, then at least one of Hom(A,B) and Hom(B,A) is empty.  This
implies that if there is a map A --> B, then B -o A can only be
(0,1) or (0,0) (0 is the empty set).  That is is either initial or a
quotient of the initial object.  In either case, it has at most one
arrow to any other object and any diagram starting with it
commutes.  The result of this is that any naturality condition that
involves objects of different types is automatic.  Either there is
no map A --> B to test or there is one and the diagram is
automatically commutative.  For an object of type I, there is a zero
map that takes every point to the (unique!) point not in any state
and takes every state to the empty state.  This is natural
restricted to the type I objects and there is a similar 0 map for
type II's.  Now there are at least four dinatural endomorphisms of
the functor that takes A and B to A -o B.  They are all the identity
on type III objects and can be either the identity or the 0 map on
type I and the same on type II.

Michael