Homogeneous models and their toposes of supported sets

This thesis studies homogeneous models by looking at their topos of finitely supported sets. Of various well-known toposes, such as cubical sets and simplicial sets, it is shown that they can be presented as a topos of this kind. It is argued that these examples can be understood as coming from a homogeneous model, in the sense of model theory, but formulated in topos-theoretical terms. It is shown that the connecting structure between the two is a factorizing prime site and the notion of a principal model. This is further substantiated by demonstrating that the Fraïssé-Hrushovski construction can be formulated in terms of such sites. The notion of finite support is abstracted and a general calculus of orbits for toposes of supported sets is developed. It is shown that these form a factorizing prime site and that they can be compared to the age of structure as in classical model theory, and can be given a topos-theoretic characterization in terms of the hyperconnected-localic factorization of a geometric morphism. The theory is then applied by revisiting and generalizing the Ryll-Nardzewski theorem to the new setting and by constructing a very general class of Fraenkel-Mostowki models of intuitionistic set theory. Lastly, a notion of a Kan fibration for such toposes is studied and shown to generalize the familiar notions in simplicial sets and cubical sets. Under particular assumptions, it is proved that these Kan fibrations are closed under dependent product and hence interpret a version of Martin-Löf intensional dependent type theory. For simplicial sets, a different approach using simplicial Moore paths and its connection to the present work is announced.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2020

Author dc:creator

• Faber, Eric Ernst

Advisor dc:contributor.advisor

• Hyland, John Martin Elliott

• topos theory
• category theory
• model theory
• intuitionism
• constructive mathematics
• mathematical logic
• sheaves
• Fraïssé theory
• set theory

Licence

• https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/365ae17d-368a-4204-8d50-45df5e5836ab/download
• https://www.rioxx.net/licenses/all-rights-reserved/

Language dc:language

en

DOI dc:identifier.doi

https://doi.org/10.17863/CAM.49282

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/302208