BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:Sketches for arithmetic universes - Dr Steve Vicke
rs (School of Computer Science\, University of Bir
mingham)
DTSTART:20160518T120000Z
DTEND:20160518T130000Z
UID:TALK2054AT
URL:/talk/index/2054
DESCRIPTION:Grothendieck says toposes are generalized topologi
cal spaces. Then any geometric theory T can be und
erstood as a space\, the points being the models o
f T\, and then the topos is its classifying topos
S[T]. A map from T_1 to T_2 is a geometric morphis
m from S[T_1] to S[T_2]\, and the universal proper
ty of classifying toposes says this is equivalent
to a model of T_2 in S[T_1]. This means that\, in
the context of a generic model of T_1\, and using
the geometric maths of colimits and finite limits\
, we construct a model of T_2: hence to describe a
map we use the points very explicitly\, despite t
his being a point-free approach\, and continuity r
elies on the geometricity of the construction.\n\n
In many ways that is a successful logical approach
to topology\, but it is hard to make a formal sys
tem for it because of the infinitary disjunctions
and coproducts that are needed\, for instance for
real analysis. The available infinities are suppli
ed externally as the objects of a chosen base topo
s S by which the whole programme is parameterized.
Long ago I conjectured that Joyal's Arithmetic Un
iverses (AUs)\, pretoposes with parametrized list
objects\, might supply enough internal infinities
(e.g. a natural numbers object) to be a finitary s
ubstitute\, with no dependence on choice of base S
\, that is good enough in practice.\n\nIn this tal
k I outline a 2-category Con that is intended to b
e the category of generalized spaces in these AU t
erms. I have a first draft of a detailed paper tha
t I am now polishing up for submission. Each objec
t T describes a geometric theory\, and presents by
universal algebra an AU AU that stands in for
S[T]. Con embeds fully and faithfully in the 2-cat
egory of AUs and strict AU-functors.\n\n* I adapt
the ideas of sketch theory to apply to AUs: princi
pally\, this introduces list objects. The category
of sketches and sketch homomorphisms maps functor
ially to AUs\, T |-> AU. This is not yet full o
r faithful - the homomorphisms are too syntax-boun
d.\n* In general\, sketches provide the ability to
declare equality between objects in an undesirabl
e way. I define "extensions" of sketches\, in whic
h limits\, colimits and list objects are introduce
d fresh in a definitional way\, and then "contexts
"\, extensions of the empty sketch. Any non-strict
model of a context (these are needed for the sema
ntics) has a unique isomorphism with a strict mode
l (needed for the universal algebraic syntax).\n*
We now have a finitary category Con_hom of context
s and sketch homomorphisms.\n* For a map from T_1
to T_2 we need to interpret T_2 in "stuff derived
uniquely from T_1". An "equivalence extension" of
T_1 is an extension in which the new ingredients a
re already known to exist\, and uniquely.\n* "Obje
ct equalities" deal with the situation where the s
ame construction is applied twice to the the same
data\, so the two copies are equal in any strict m
odel.\n* Con is a localization of (Con_hom)^op. It
takes object equalities to actual equalities\, an
d makes equivalence extensions invertible. It is e
ntirely finitary.\n* Con has finite pie-limits (pr
oduct\, inserter\, equifier)\, and strict pullback
s of extension maps.\n
LOCATION:CS 217
CONTACT:Uday Reddy
END:VEVENT
END:VCALENDAR