Abstract
The paper uses structures in Con, the author's 2-category of sketches for arithmetic universes (AUs), to provide constructive, base-independent results for Grothendieck toposes (bounded S-toposes) as generalized spaces.
The main result is to show how an extension map U : T1→ T0 can be viewed as a bundle, transforming base points (models of T0 in any elementary topos S with nno) to fibres (generalized spaces over S).
Features of the work include analysis of strictness of models, using properties of the objects of Con; the use of Gray tensor products to relate syntactic transformation of models by 1-cells in Con and semantic transformations by non-strict AU-functors; and the use of 2-fibrations to index over a 2-category of base toposes S.
The main result is to show how an extension map U : T1→ T0 can be viewed as a bundle, transforming base points (models of T0 in any elementary topos S with nno) to fibres (generalized spaces over S).
Features of the work include analysis of strictness of models, using properties of the objects of Con; the use of Gray tensor products to relate syntactic transformation of models by 1-cells in Con and semantic transformations by non-strict AU-functors; and the use of 2-fibrations to index over a 2-category of base toposes S.
Original language | English |
---|---|
Pages (from-to) | 213-248 |
Journal | Cahiers de Topologie et Géométrie Différentielle Catégoriques |
Volume | 58 |
Issue number | 3 & 4 |
Publication status | Published - 1 Dec 2017 |
Keywords
- geometric theory
- 2-fibration
- sketch
- Gray tensor