Synthetic topos theory

  • Taichi Uemura
2023-10-31

© 2023 Taichi Uemura

This work is licensed under a Creative Commons Attribution 4.0 International License.

Repository: https://github.com/uemurax/synthetic-topos-theory

Abstract: We propose a type theory in which topos theory is developed synthetically.

      • Introduction
        • Structure
          • Status
          • Logoses and toposes
            • Étale morphisms
              • A universal property of \(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\)
                • Sheaves on \(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\)
                  • Internal topos theory
                  • Topical type theory
                    • Universe levels
                      • Core type theory
                        • Base type theory
                          • Internal type theories
                            • Type theory of spaces
                              • Type theory of sheaves
                                • Cross-theory axioms
                                • Topos theory
                                  • Classifying spaces
                                    • The category of sheaves
                                      • Inverse images
                                        • Direct images
                                          • Étale toposes
                                            • Essential morphisms
                                              • Subtoposes and modalities
                                              • The topos of types
                                                • The topos of propositions
                                                  • Linear orders and simplicial types
                                                    • Index
                                                      • Notation index
                                                        • Bibliography