A coherent account of geometricity

Add to your list(s) Download to your calendar using vCal

• Steve Vickers
• Tuesday 21 July 2015, 12:00-13:00
• CS 217.

If you have a question about this talk, please contact Neel Krishnaswami.

I shall present a coherence issue that arises on the trail of fibrewise topology, or a dependent type theory of spaces (always point-free). The results can be applied to space constructions such as powerlocales (hyperspaces) and valuation locales. At a certain point the treatment is impredicative, but I conjecture that this can be circumvented.

In topos theory, internal spaces and reindexing along continuous maps (geometric morphisms) are equivalent to bundles and pullback; and if a map is viewed as a generalized point then the bundle pullback is a generalized fibre. From the point of view of dependent types, we are therefore interested in “geometric” constructions of spaces, which are preserved – up to isomorphism – by reindexing and hence work fibrewise. The present work provides sufficient conditions for the coherence of those isomorphisms.

The first part of the argument is predicative, and depends on a careful analysis of the known techniques of working geometrically on presentations of spaces (or formal topologies). It uses the essentially algebraic theory of arithmetic universes as framework for presenting each space construction in a uniform, generic way, instantiated over any base by substitution.

The second part is still impredicative, and requires a condition that the construction should, on morphisms between presentations, preserve the property of inducing a homeomorphism between the spaces.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.