![]() |
![]() |
![]() A coherent account of geometricityAdd to your list(s) Download to your calendar using vCal
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:Note that ex-directory lists are not shown. |
Other listsSpeech Recognition by Synthesis Seminars Physics and Astronomy Colloquia Molecular and Medical Physics Seminar SeriesOther talks[Seminar]: Two easy three-body problems Non-Newtonian fluid injection into an otherwise Newtonian boundary layer [Friday seminar]: Irradiated brown dwarfs in the desert Seminar The percolating cluster is invisible to image recognition with deep learning Towards Efficient and Robust Data-Driven Optimization |