BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY: A coherent account of geometricity - Steve Vicker
s
DTSTART:20150721T110000Z
DTEND:20150721T120000Z
UID:TALK1769AT
URL:/talk/index/1769
DESCRIPTION:I shall present a coherence issue that arises on t
he trail of fibrewise\ntopology\, or a dependent t
ype theory of spaces (always point-free). The\nres
ults can be applied to space constructions such as
powerlocales\n(hyperspaces) and valuation locales
. At a certain point the treatment is\nimpredicati
ve\, but I conjecture that this can be circumvente
d.\n\nIn topos theory\, internal spaces and reinde
xing along continuous maps\n(geometric morphisms)
are equivalent to bundles and pullback\; and if a\
nmap is viewed as a generalized point then the bun
dle pullback is a\ngeneralized fibre. From the poi
nt of view of dependent types\, we are\ntherefore
interested in "geometric" constructions of spaces\
, which are\npreserved - up to isomorphism - by re
indexing and hence work fibrewise.\nThe present wo
rk provides sufficient conditions for the coherenc
e of\nthose isomorphisms.\n\nThe first part of the
argument is predicative\, and depends on a carefu
l\nanalysis of the known techniques of working geo
metrically on\npresentations of spaces (or formal
topologies). It uses the essentially\nalgebraic th
eory of arithmetic universes as framework for pres
enting\neach space construction in a uniform\, gen
eric way\, instantiated over any\nbase by substitu
tion.\n\nThe second part is still impredicative\,
and requires a condition that\nthe construction sh
ould\, on morphisms between presentations\, preser
ve\nthe property of inducing a homeomorphism betwe
en the spaces.\n\n
LOCATION:CS 217
CONTACT:Neel Krishnaswami
END:VEVENT
END:VCALENDAR