bibliography.bib

@book{johnstone:elephant,
  author = {Johnstone, P. T.},
  title = {Sketches of an Elephant: A Topos Theory Compendium},
  year = {2002},
  publisher = {Oxford University Press}}

@book{johnstone:topos-theory,
  author = {Johnstone, P. T.},
  title = {Topos Theory},
  year = {1977},
  series = {L.M.S. Monographs},
  volume = {10},
  publisher = {Academic Press}}

@article{leinster:introduction,
  author = {Leinster, T.},
  title = {An informal introduction to topos theory},
  journal = {Publications of the nLab},
  volume = {1},
  number = {1},
  year = {2011}}

@inbook{vickers:locales-toposes,
  author = {Vickers, S.},
  title = {Locales and Toposes as Spaces},
  year = {2007},
  pages = {429--496},
  booktitle = {Handbook of Spatial Logics},
  publisher = {Springer},
  editor = {Aiello, M. and Pratt-Hartmann, I. and van Benthem, J.},
  url = {https://www.cs.bham.ac.uk/~sjv/LocTopSpaces.pdf}}

@article{vickers:continuity,
  author = {Vickers, S.},
  title = {Continuity and geometric logic},
  volume = {12},
  number = {1},
  year = {2014},
  pages = {14--27},
  journal = {J. Appl. Log.},
  url = {https://www.cs.bham.ac.uk/~sjv/GeoAspects.pdf}}

@article{vickers:case-study,
  author = {Vickers, S.},
  title = {The double powerlocale and exponentiation: a case study in geometric logic},
  year = {2004},
  journal = {Theory Appl. Categ.},
  volume = {12},
  number = {13},
  pages = {372--422}}

@inproceedings{mulvey:repr,
  author = {Mulvey, C.},
  title = {Intuitionistic algebra and representations of rings},
  booktitle = {Recent Advances in the Representation Theory of Rings and $C^*$-algebras by Continuous Sections},
  year = {1974},
  editor = {Hofmann, K. H. and Liukkonen, J. R.},
  series = {Mem. Amer. Math. Soc.},
  volume = {148},
  publisher = {American Mathematical Society},
  pages = {3--57}}

@inproceedings{wraith:generic-galois-theory,
  author = {Wraith, G.},
  title = {Generic Galois theory of local rings},
  booktitle = {Applications of sheaves},
  year = {1979},
  editor = {Fourman, M. and Mulvey, C. and Scott, D.},
  series = {Lecture Notes in Math.},
  volume = {753},
  publisher = {Springer},
  pages = {739--767}}

@unpublished{shulman:stack,
  author = {Shulman, M.},
  title = {Stack semantics and the comparison of material and structural set theories},
  year = {2010},
  url = {https://arxiv.org/abs/1004.3802}}

@unpublished{shulman:set-theory,
  author = {Shulman, M.},
  title = {Set theory for category theory},
  year = {2008},
  url = {https://arxiv.org/abs/0810.1279}}

@inproceedings{feferman:set-foundations,
  author = {Feferman, S.},
  title = {Set-theoretical foundations of category theory},
  booktitle = {Reports of the Midwest Category Seminar~III},
  year = {1969},
  series = {Lecture Notes in Math.},
  volume = {106},
  publisher = {Springer},
  pages = {201--247}}

@book{troelstra-dalen:constructivism,
  author = {Troelstra, A. S. and van Dalen, D.},
  title = {Constructivism in Mathematics: An Introduction},
  year = {1988},
  publisher = {North-Holland Publishing}}

@misc{stacks-project,
  author = "The {Stacks Project Authors}",
  title = "{Stacks Project}",
  url = {https://stacks.math.columbia.edu/}}

@book{moerdijk-maclane:sheaves-logic,
  author = {Mac Lane, S. and Moerdijk, I.},
  title = {Sheaves in Geometry and Logic: a First Introduction to Topos Theory},
  publisher = {Springer},
  series = {Universitext},
  year = {1992}}

@book{mines-richman-ruitenburg:constructive-algebra,
  title = {A Course in Constructive Algebra},
  author = {Mines, R. and Richman, F. and Ruitenburg, W.},
  series = {Universitext},
  year = {1988},
  publisher = {Springer}}

@article{richman:noetherian,
  title = {The ascending tree condition: constructive algebra without choice},
  author = {Richman, F.},
  journal = {Comm. Algebra},
  volume = {31},
  number = {4},
  pages = {1993--2002},
  year = {2003}}

@book{bishop-bridges:constructive-analysis,
  author = {Bishop, E. and Bridges, D.},
  title = {Constructive Analysis},
  publisher = {Springer},
  year = {1985}}

@incollection{bauer:int-mathematics,
  author = {Bauer, A.},
  title = {Intuitionistic Mathematics and Realizability in the Physical World},
  booktitle = {A Computable Universe},
  publisher = {World Scientific Pub Co},
  editor = {Zenil, H.},
  year = {2012}}

@misc{bauer:video,
  author = {Bauer, A.},
  title = {Five Stages of Accepting Constructive Mathematics},
  note = {Lecture at the Institute for Advanced Study},
  year = {2013},
  url = {https://video.ias.edu/members/1213/0318-AndrejBauer}}

@article{awodey-bauer:bracket,
  title = {Propositions as [Types]},
  author = {Awodey, S. and Bauer, A.},
  journal = {J. Logic Comput.},
  volume = {14},
  number = {4},
  pages = {447--471},
  year = {2004}}

@inbook{bell:catlogprime,
  author = {Bell, J.},
  title = {The development of categorical logic},
  editor = {Gabbay, D. and Guenthner, F.},
  booktitle = {Handbook of Philosophical Logic},
  publisher = {Springer},
  edition = {2},
  year = {2005},
  volume = {12},
  pages = {279--361}}

@book{vakil:foag,
  author = {Vakil, Ravi},
  title = {The Rising Sea. Foundations of Algebraic Geometry},
  year = {2017},
  url = {http://math.stanford.edu/~vakil/216blog/}}

@article{kleiman:misconceptions,
  author = {Kleiman, S.},
  title = {Misconceptions about $K_X$},
  year = {1979},
  volume = {25},
  journal = {Enseign. Math.},
  pages = {203--206}}

@article{bohr1,
  author = {Butterfield, J. and Hamilton, J. and Isham, C.},
  title = {A topos perspective on the Kochen--Specker theorem, I. quantum states as generalized valuations},
  journal = {Internat. J. Theoret. Phys.},
  volume = {37},
  number = {11},
  pages = {2669--2733},
  year = {1998}}

@article{bohr2,
  year = {2009},
  journal = {Comm. Math. Phys.},
  volume = {291},
  number = {1},
  title = {A topos for algebraic quantum theory},
  publisher = {Springer},
  author = {Heunen, C. and Landsman, N. and Spitters, B.},
  pages = {63--110}}

@misc{bohr3,
  author = {Henry, S.},
  title = {A geometric Bohr topos},
  year = {2015},
  url = {https://arxiv.org/abs/1502.01896}}

@article{vries:sheafification,
  year = {1987},
  author = {de Vries, F.-J.},
  title = {Applications of constructive logic to sheaf constructions in toposes},
  volume = {25},
  journal = {Logic Group preprint series, Rijksuniversiteit Utrecht}}

@inproceedings{johnstone:art,
  title = {The art of pointless thinking: a student's guide to the category of locales},
  author = {Johnstone, P. T.},
  booktitle = {Category theory at work (Bremen, 1990)},
  pages = {85--107},
  series = {Res. Exp. Math.},
  number = {18},
  publisher = {Heldermann},
  year = {1991}}

@article{johnstone:point,
  title = {The point of pointless topology},
  author = {Johnstone, P. T.},
  year = {1983},
  journal = {Bull. Amer. Math. Soc.},
  volume = {8},
  number = {1},
  pages = {41--53}}

@inbook{dyn:char-krull,
  author = {Coquand, T. and Lombardi, H. and Roy, M.-F.},
  booktitle = {From Sets and Types to Analysis and Topology: Towards Practicable Foundations for Constructive Mathematics},
  publisher = {Oxford Univ. Press},
  year = {2005},
  title = {An elementary characterisation of Krull dimension},
  pages = {239--244}}

@article{dyn:krull-integral,
  author = {Coquand, T. and Ducos, L. and Lombardi, H. and Quitté, C.},
  title = {Constructive Krull dimension I: integral extensions},
  journal = {J. Algebra Appl.},
  volume = {8},
  number = {1},
  pages = {129-138},
  year = {2009}}

@article{dyn:krull-dim-polynomial-ring,
  author = {Coquand, T. and Lombardi, H.},
  title = {A short proof for the Krull dimension of a polynomial ring},
  journal = {Amer. Math. Monthly},
  volume = {112},
  number = {9},
  year = {2005},
  pages = {826--829}}

@article{gillam:localization,
  author = {Gillam, W. D.},
  title = {Localization of ringed spaces},
  journal = {Adv. Pure Math.},
  volume = {1},
  number = {5},
  pages = {250--263},
  year = {2011}}

@book{hakim:relative-schemes,
  author = {Hakim, M.},
  title = {Topos annelés et schémas relatifs},
  series = {Ergeb. Math. Grenzgeb.},
  volume = {64},
  year = {1972},
  publisher = {Springer}}

@phdthesis{jackson:sheaf-theoretic-measure-theory,
  author = {Jackson, M.},
  title = {A sheaf theoretic approach to measure theory},
  year = {2006},
  school = {University of Pittsburgh}}

@article{aczel:russell-prawitz,
  author = {Aczel, P.},
  title = {The Russell--Prawitz modality},
  year = {2001},
  journal = {Math. Structures Comput. Sci},
  volume = {11},
  number = {4},
  pages = {541--554}}

@inproceedings{escardo:oliva:peirce-shift,
  author = {Escardó, M. and Oliva, P.},
  title = {The Peirce translation and the double negation shift},
  year = {2010},
  booktitle = {Programs, Proofs, Processes},
  series = {Lecture Notes in Comput. Sci.},
  volume = {6158},
  editor = {Ferreira, F. and Löwe, B. and Mayordomo, E. and Mendes Gomes, L.},
  publisher = {Springer},
  pages = {151--161}}

@unpublished{lurie:dag5,
  author = {Lurie, J.},
  title = {Derived Algebraic Geometry V: Structured Spaces},
  year = {2009},
  url = {https://arxiv.org/abs/0905.0459}}

@misc{tao:analysis-rel-measure-space,
  author = {Tao, T.},
  title = {Real analysis relative to a finite measure space},
  year = {2014},
  url = {https://terrytao.wordpress.com/2014/07/15/real-analysis-relative-to-a-finite-measure-space/}}

@misc{tao:cheap-nsa,
  author = {Tao, T.},
  title = {A cheap version of nonstandard analysis},
  year = {2012},
  url = {https://terrytao.wordpress.com/2012/04/02/a-cheap-version-of-nonstandard-analysis/}}

@book{kock:sdg,
  author = {Kock, A.},
  title = {Synthetic Differential Geometry},
  year = {2006},
  publisher = {Cambridge University Press},
  edition = {2},
  series = {London Math Soc. Lecture Note Ser.},
  number = {333},
  url = {http://home.math.au.dk/kock/sdg99.pdf}}

@book{moerdijk:reyes:models,
  author = {Moerdijk, I. and Reyes, G.},
  title = {Models for Smooth Infinitesimal Analysis},
  year = {1991},
  publisher = {Springer}}

@inproceedings{mannaa:coquand:alg-closure,
  author = {Mannaa, B. and Coquand, T.},
  title = {A sheaf model of the algebraic closure},
  booktitle = {Proc. of the Fifth International Workshop on Classical Logic and Computation},
  year = {2014},
  url = {https://arxiv.org/abs/1404.4549}}

@unpublished{pasquali:sheafification,
  author = {Pasquali, F.},
  title = {A sheafification theorem for doctrines},
  year = {2014},
  url = {https://arxiv.org/abs/1311.1424}}

@unpublished{henry:measure-theory-boolean-toposes,
  author = {Henry, S.},
  title = {Measure theory over boolean toposes},
  year = {2014},
  url = {https://arxiv.org/abs/1411.1605}}

@phdthesis{henry:classifying-topoi,
  title = {Classifying topoi and preservation of higher order logic by geometric morphisms},
  author = {Henry, S.},
  year = {2013},
  school = {University of Michigan},
  url = {https://arxiv.org/abs/1305.3254}}

@book{borceux:handbook3,
  author = {Borceux, F.},
  title = {Handbook of Categorical Algebra: Volume 3, Sheaf Theory},
  series = {Encyclopedia Math. Appl.},
  year = {1994},
  publisher = {Cambridge University Press}}

@inproceedings{birkedal:al:sgdt,
  author = {Birkedal, L. and Mogelberg, R. and Schwinghammer, J. and Stovring, K.},
  title = {First steps in synthetic guarded domain theory: step-indexing in the topos of trees},
  year = {2012},
  booktitle = {Proc. of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science},
  url = {https://www.cs.au.dk/~birke/papers/sgdt-journal.pdf}}

@article{awodey-kishida:modal,
  author = {Awodey, S. and Kishida, K.},
  title = {Topology and modality: The topological interpretation of first-order modal logic},
  year = {2008},
  journal = {The Review of Symbolic Logic},
  volume = {1, special issue 2},
  pages = {146--166}}

@unpublished{caramello:1,
  author = {Caramello, O.},
  title = {The unification of mathematics via topos theory},
  year = {2010},
  url = {https://arxiv.org/abs/1006.3930}}

@unpublished{caramello:2,
  author = {Caramello, O.},
  title = {A topos-theoretic approach to Stone-type dualities},
  year = {2011},
  url = {https://arxiv.org/abs/1103.3493}}

@unpublished{caramello:lattices,
  author = {Caramello, O.},
  title = {Lattices of theories},
  year = {2009},
  url = {https://arxiv.org/abs/0905.0299}}

@unpublished{caramello:preliminaries,
  author = {Caramello, O.},
  title = {Topos-theoretic background},
  year = {2014},
  url = {https://www.oliviacaramello.com/Unification/ToposTheoreticPreliminariesOliviaCaramello.pdf}}

@phdthesis{brandenburg:tensor-foundations,
  author = {Brandenburg, M.},
  title = {Tensor categorical foundations of algebraic geometry},
  year = {2014},
  school = {Universität Münster},
  url = {https://arxiv.org/abs/1410.1716}}

@unpublished{brandenburg:schur,
  author = {Brandenburg, M.},
  title = {Operations on categories of modules are given by Schur functors},
  year = {2016},
  url = {https://arxiv.org/abs/1610.02180}}

@article{clr:dynamicalmethod,
  author = {Coste, M. and Lombardi, H. and Roy, M.-F.},
  title = {Dynamical method in algebra: ef{}fective Nullstellensätze},
  journal = {Ann. Pure Appl. Logic},
  volume = {111},
  number = {3},
  pages = {203--256},
  year = {2001},
  url = {https://perso.univ-rennes1.fr/michel.coste/publis/clr.pdf}}

@article{cl:logical,
  author = {Coquand, T. and Lombardi, H.},
  title = {A logical approach to abstract algebra},
  journal = {Math. Structures Comput. Sci},
  year = {2006},
  volume = {16},
  number = {5},
  pages = {885--900},
  url = {http://www.cse.chalmers.se/~coquand/FISCHBACHAU/AlgebraLogicCoqLom.pdf}}

@article{kock:univ-proj-geometry,
  author = {Kock, A.},
  title = {Universal projective geometry via topos theory},
  journal = {J. Pure Appl. Algebra},
  volume = {9},
  number = {1},
  pages = {1--24},
  year = {1976}}

@inproceedings{bauer:synthetic-computability-theory,
  author = {Bauer, A.},
  title = {First steps in synthetic computability theory},
  booktitle = {Proc. of the 21st Annual Conference on Mathematical Foundations of Programming Semantics},
  year = {2006},
  editor = {Escardó, M. and Jung, A. and Mislove, M.},
  series = {Electron. Notes Theor. Comput. Sci.},
  volume = {155},
  publisher = {Elsevier B.V.},
  pages = {5--31},
  url = {http://math.andrej.com/data/synthetic.pdf}}

@inproceedings{hyland:synthetic-domain-theory,
  author = {Hyland, J. M. E.},
  title = {First steps in synthetic domain theory},
  booktitle = {Proc. of the International Conference held in Como, Italy, 1990},
  year = {1991},
  editor = {Carbonia, A. and Pedicchio, M. and Rosolini, G.},
  series = {Lecture Notes in Math.},
  volume = {1488},
  publisher = {Springer},
  pages = {131--156}}

@unpublished{anel:factorization-systems,
  author = {Anel, M.},
  title = {Grothendieck topologies from unique factorisation systems},
  year = {2009},
  url = {https://arxiv.org/abs/0902.1130}}

@incollection{tierney:spectrum,
  author = {Tierney, M.},
  title = {On the spectrum of a ringed topos},
  year = {1976},
  booktitle = {Algebra, Topology, and Category Theory. A Collection of Papers in Honor of Samuel Eilenberg},
  publisher = {Academic Press},
  editor = {Heller, A. and Tierney, M.},
  pages = {189--210}}

@article{bauer:lumsdaine:bourbaki-witt,
  author = {Bauer, A. and Lumsdaine, P.},
  title = {On the Bourbaki--Witt principle in toposes},
  pages = {87--99},
  volume = {155},
  number = {1},
  year = {2013},
  journal = {Math. Proc. Cambridge Philos. Soc.},
  url = {https://arxiv.org/abs/1201.0340}}

@unpublished{melikhov:intuitionistic-logic,
  author = {Melikhov, S.},
  title = {Mathematical semantics of intuitionistic logic},
  year = {2015},
  url = {https://arxiv.org/abs/1504.03380}}

@book{atiyah:macdonald:commutative-algebra,
  author = {Atiyah, M. and Macdonald, I.},
  title = {Introduction to Commutative Algebra},
  year = {1969},
  publisher = {Addison--Wesley}}

@book{demazure:gabriel,
  title = {Groupes algébriques: Géométrie algébrique. Généralités. Groupes commutatifs},
  volume = {1},
  author = {Demazure, M. and Gabriel, P.},
  publisher = {Masson \& Cie},
  year = {1970}}

@phdthesis{penon,
  title = {De l'infinitésimal au local},
  author = {Penon, J.},
  year = {1985},
  school = {Université Paris VII},
  pages = {1--191},
  journal = {Diagrammes},
  volume = {S13}}

Cite?
https://www.sciencedirect.com/science/article/pii/0022404983900750
https://www.sciencedirect.com/science/article/pii/0022404986900915

@article{aczel-et-al:injective,
  author = {Aczel, P. and van den Berg, B. and Granström, J. and Schuster, P.},
  title = {Are there enough injective sets?},
  year = {2011},
  journal = {Studia Logica},
  volume = {101},
  number = {3},
  pages = {467--482}}

@article{blass:inj-proj-axc,
  author = {Blass, A.},
  title = {Injectivity, projectivity, and the axiom of choice},
  year = {1979},
  journal = {Trans. Amer. Math. Soc.},
  volume = {255},
  pages = {31--59}}

@article{harting,
  author = {Harting, R.},
  title = {Locally injective abelian groups in a topos},
  year = {1983},
  journal = {Comm. Algebra},
  volume = {11},
  number = {4},
  pages = {349--376}}

@misc{staats:generic-freeness,
  author = {Staats, C.},
  title = {Elementary proof of generic freeness},
  year = {2011},
  url = {https://math.uchicago.edu/~cstaats/Charles_Staats_III/Notes_and_papers_files/generic_freeness.pdf}}

@phdthesis{lesnik,
  author = {Lešnik, D.},
  title = {Synthetic Topology and Constructive Metric Spaces},
  school = {University of Ljubljana},
  year = {2010}}

@article{escardo,
  author = {Escardó, M.},
  title = {Synthetic topology of data types and classical spaces},
  journal = {Electron. Notes Theor. Comput. Sci.},
  year = {2004},
  volume = {87},
  pages = {21--156}}

@book{hott,
  author = {The {Univalent Foundations Program}},
  title  = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  url = {https://homotopytypetheory.org/book},
  address = {Institute for Advanced Study},
  year = {2013}}

@unpublished{blechschmidt:generic-freeness,
  author = {Blechschmidt, I.},
  title = {An elementary and constructive proof of Grothendieck's generic freeness lemma},
  year = {2018},
  url = {https://arxiv.org/abs/1807.01231}}

@misc{mo:kernel,
  title = {Constructive proof that a kernel consists of nilpotent elements (thread started by HeinrichD)},
  author = {MathOverflow contributors},
  year = {2016},
  url = {https://mathoverflow.net/questions/250040}}

@misc{mo:pp1,
  title = {What does the Zariski topos of $\mathbb{P}^1$ classify? (thread started by Yuhao Huang)},
  author = {MathOverflow contributors},
  year = {2017},
  url = {https://mathoverflow.net/questions/258485}}

@misc{mo:gubkin,
  title = {Several topos theory questions},
  author = {Gubkin, S.},
  year = {2009},
  url = {https://mathoverflow.net/questions/2314/several-topos-theory-questions}}

@misc{arndt:lax-pullback,
  author = {Arndt, P.},
  title = {MaxSpec, Spec, … ``RadSpec''? Or, why not look at all radical ideals? (answer to a question by Zev Chonoles on MathOverflow)},
  year = {2010},
  url = {https://mathoverflow.net/a/14335/31233}}

@article{penon:locally-internal-categories,
  author = {Penon, J.},
  title = {Catégories localement internes},
  journal = {C. R. Acad. Sc. Paris Sér. A},
  number = {278},
  year = {1974},
  pages = {1577--1580},
  url = {https://gallica.bnf.fr/ark:/12148/bpt6k6236784g/f355.image}}

@article{lawvere:icm-address,
  author = {Lawvere, F.},
  title = {Quantifiers and sheaves},
  year = {1970},
  journal = {Actes Congrès Intern. Math.},
  volume = {1},
  pages = {329--334}}

@book{lombardi:quitte:constructive-algebra,
  author = {Lombardi, H. and Quitté, C.},
  title = {Commutative Algebra: Constructive Methods},
  year = {2015},
  publisher = {Springer}}

@article{vermeulen:locales,
  author = {Vermeulen, J. J. C.},
  title = {Proper maps of locales},
  journal = {J. Pure Appl. Algebra},
  volume = {92},
  number = {1},
  pages = {79--107},
  year = {1994}}

@article{cls:spectral-schemes,
  author = {Coquand, T. and Lombardi, H. and Schuster, P.},
  title = {Spectral schemes as ringed lattices},
  year = {2009},
  journal = {Ann. Math. Artif. Intell.},
  volume = {56},
  issue = {3-4},
  pages = {339--360}}

@article{cls:projective-spectrum,
  author = {Coquand, T. and Lombardi, H. and Schuster, P.},
  title = {The projective spectrum as a distributive lattice},
  year = {2007},
  journal = {Cah. Topol. Géom. Différ. Catég.},
  volume = {48},
  number = {3},
  pages = {220--228}}

@article{schuster:formal-zariski,
  author = {Schuster, P.},
  title = {Formal Zariski topology: positivity and points},
  journal = {Ann. Pure Appl. Logic},
  volume = {137},
  number = {1},
  pages = {317--359},
  year = {2006}}

@unpublished{tarizadeh:flat,
  author = {Tarizadeh, A.},
  title = {The flat topology and its duality aspects},
  year = {2017},
  url = {https://arxiv.org/abs/1503.04299v9}}

@article{adamek:rosicky:reflective,
  author = {Adámek, J. and Rosický, J.},
  title = {On reflective subcategories of locally presentable categories},
  journal = {Theory Appl. Categ.},
  volume = {30},
  number = {41},
  year = {2015},
  pages = {1306--1318}}

@article{banaschewski:vermeulen:radical-content,
  author = {Banaschewski, B. and Vermeulen, J. J. C.},
  title = {Polynomials and radical ideals},
  journal = {J. Pure Appl. Algebra},
  year = {1996},
  volume = {113},
  number = {3},
  pages = {219--227}}

@article{cole:spectra,
  author = {Cole, J.},
  title = {The bicategory of topoi and spectra},
  pages = {1--16},
  year = {2016},
  journal = {Repr. Theory Appl. Categ.},
  number = {25}}

@book{adamek:rosicky:presentable,
  title = {Locally Presentable and Accessible Categories},
  author = {Adámek, J. and Rosicky, J.},
  series = {London Math. Soc. Lecture Note Ser.},
  year = {1994},
  publisher = {Cambridge University Press},
  volume = {189}}

@article{reyes:wraith:note-tangent-bundles,
  author = {Reyes, G. and Wraith, G.},
  title = {A note on tangent bundles in a category with a ring object},
  journal = {Math. Scand.},
  volume = {42},
  number = {1},
  year = {1978},
  pages = {53--63}}

@unpublished{schroer:points-fppf,
  author = {Schröer, S.},
  title = {Points in the fppf topology},
  year = {2014},
  url = {https://arxiv.org/abs/1407.5446}}

@unpublished{gabber:kelly:points,
  author = {Gabber, O. and Kelly, S.},
  title = {Points in algebraic geometry},
  year = {2014},
  url = {https://arxiv.org/abs/1407.5782}}

@inproceedings{ziegler:brattka:spectrum,
  author = {Ziegler, M. and Brattka, V.},
  title = {A computable spectral theorem},
  booktitle = {Computability and Complexity in Analysis},
  year = {2001},
  series = {Lecture Notes in Comput. Sci.},
  volume = {2064},
  editor = {Blanck, J. and Brattka, V. and Hertling, P.},
  publisher = {Springer},
  pages = {378--388}}

@inproceedings{ruitenburg:roots,
  author = {Ruitenburg, W.},
  title = {Constructing roots of polynomials over the complex numbers},
  editor = {Cohen, A.},
  booktitle = {Computational Aspects of Lie Group Representations and Related Topics, Proc. of the 1990 Computer Algebra Seminar held in Amsterdam},
  series = {CWI Tract},
  volume = {84},
  year = {1991},
  pages = {107--128}}

@book{goldblatt:topoi,
  author = {Goldblatt, R.},
  title = {Topoi: The Categorical Analysis of Logic},
  year = {1984},
  publisher = {Elsevier},
  series = {Stud. Logic Found. Math.},
  volume = {98}}

@article{goldblatt:modality,
  author = {Goldblatt, R.},
  title = {Grothendieck topology as geometric modality},
  year = {1981},
  journal = {MLQ Math. Log. Q.},
  volume = {27},
  number = {31--35},
  pages = {495--529}}

@article{pfenning:davies:reconstruction,
  author = {Pfenning, F. and Davies, R.},
  title = {A judgmental reconstruction of modal logic},
  year = {2001},
  journal = {Math. Structures Comput. Sci.},
  volume = {11},
  number = {4},
  pages = {511--540}}

@article{awodey:birkedal:local-maps,
  author = {Awodey, S. and Birkedal, L.},
  title = {Elementary axioms for local maps of toposes},
  year = {2003},
  journal = {J. Pure Appl. Algebra},
  volume = {177},
  number = {3},
  pages = {215--230}}

@misc{secret-blogging-seminar:fpov,
  author = {Commentators on the Secret Blogging Seminar},
  title = {Algebraic geometry without prime ideals (thread started by Joel Kamnitzer)},
  year = {2009},
  url = {https://sbseminar.wordpress.com/2009/08/06/algebraic-geometry-without-prime-ideals/}}

@mastersthesis{vezzani:fun,
  author = {Vezzani, A.},
  title = {On the geometry over the field with one element},
  year = {2010},
  url = {https://www.math.univ-paris13.fr/~vezzani/Files/Research/tesi_vezzani.pdf},
  school = {Università degli Studi di Milano}}

@misc{pena-lorscheid:fun,
  author = {Peña, J. and Lorscheid, O.},
  title = {Mapping $\mathbb{F}_1$-land: An overview of geometries over the field with one element},
  year = {2009},
  url = {https://arxiv.org/abs/0909.0069}}

@inbook{mclarty:ontology,
  title = {`There is no ontology here': visual and structural geometry in arithmetic},
  author = {McLarty, C.},
  year = {2008},
  booktitle = {The Philosophy of Mathematical Practice},
  editor = {Mancosu, P.},
  publisher = {Oxford University Press}}

@article{mclarty:what-does-it-take,
  title = {What does it take to prove Fermat's Last Theorem? Grothendieck and the logic of number theory},
  author = {McLarty, C.},
  year = {2010},
  journal = {Bull. Symbolic Logic},
  volume = {16},
  number = {3},
  pages = {359--377}}

@misc{belmans:topologies,
  title = {Comparison of topologies on the categories of schemes},
  author = {Belmans, P.},
  year = {2015},
  url = {https://pbelmans.ncag.info/topologies-comparison/}}

@phdthesis{low:local-models,
  title = {Categories of spaces built from local models},
  author = {Low, Z. L.},
  year = {2016},
  url = {https://zll22.user.srcf.net/dpmms/thesis.pdf},
  school = {University of Cambridge}}

@book{eisenbud:syzygies,
  title = {The Geometry of Syzygies},
  author = {Eisenbud, D.},
  series = {Grad. Texts in Math.},
  volume = {229},
  year = {2005},
  publisher = {Springer}}

@manual{gap,
  author = {{The GAP Group}},
  title = {GAP -- Groups, Algorithms, and Programming, Version 4.8.7},
  year = {2017},
  url = {https://www.gap-system.org/}}

@article{joyal:spectrum,
  author = {Joyal, A.},
  title = {Les théorèmes de Chevalley--Tarski et remarques sur l'algèbre constructive},
  year = {1975},
  journal = {Cah. Topol. Géom. Différ. Catég.},
  volume = {16},
  number = {3},
  pages = {256--258}}

@article{espanol:spectrum,
  author = {Español, L.},
  title = {Le spectre d'un anneau dans l'algèbre constructive et applications à la dimension},
  year = {1983},
  journal = {Cah. Topol. Géom. Différ. Catég.},
  volume = {24},
  number = {2},
  pages = {133--144}}

@article{barakat-lh:ext,
  author = {Barakat, M. and Lange-Hegermann, M.},
  title = {On the Ext-computability of Serre quotient categories},
  journal = {J. Algebra},
  volume = {240},
  year = {2014},
  pages = {333--349}}

@article{barakat-lh:homalg,
  author = {Barakat, M. and Lange-Hegermann, M.},
  title = {An axiomatic setup for algorithmic homological algebra and an alternative approach to localization},
  journal = {J. Algebra Appl.},
  volume = {10},
  number = {2},
  year = {2011},
  pages = {269--293}}

@article{awodey-butz:completeness,
  author = {Awodey, S. and Butz, C.},
  title = {Topological completeness for higher-order logic},
  journal = {J. Symbolic Logic},
  volume = {65},
  number = {3},
  pages = {1168--1182},
  year = {2000}}

@inproceedings{coste:sheaf-representation,
  title = {Localisation, spectra and sheaf representation},
  author = {Coste, M.},
  booktitle = {Applications of sheaves},
  year = {1979},
  editor = {Fourman, M. and Mulvey, C. and Scott, D.},
  series = {Lecture Notes in Math.},
  volume = {753},
  publisher = {Springer},
  pages = {212--238}}

@article{kelly-lawvere:essential-localizations,
  author = {Kelly, G. and Lawvere, F.},
  title = {On the complete lattice of essential localizations},
  journal = {Bull. Soc. Math. Belg., Sér. A},
  volume = {41},
  year = {1989},
  pages = {289--319}}

@misc{shulman:categorical-logic,
  author = {Shulman, M.},
  title = {Categorical logic from a categorical point of view (draft for AARMS Summer School 2016)},
  year = {2016},
  url = {https://github.com/mikeshulman/catlog}}

@misc{streicher:ctcl,
  author = {Streicher, T.},
  title = {Introduction to category theory and categorical logic},
  year = {2004},
  url = {https://www.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf}}

@inbook{thomason-trobaugh,
  author = {Thomason, R. and Trobaugh, T.},
  title = {Higher algebraic K-theory of schemes and of derived categories},
  booktitle = {The Grothendieck Festschrift},
  series = {Progr. Math.},
  volume = {88},
  publisher = {Birkhäuser},
  pages = {247--435}}

@article{kempf:cohomology,
  author = {Kempf, G.},
  title = {Some elementary proofs of basic theorems in the cohomology of quasi-coherent sheaves},
  journal = {Rocky Mountain J. Math.},
  volume = {10},
  number = {3},
  year = {1980},
  pages = {637--646}}

@article{johnstone:rings-fields-and-spectra,
  author = {Johnstone, P. T.},
  title = {Rings, fields, and spectra},
  journal = {J. Algebra},
  volume = {49},
  number = {1},
  pages = {238--260},
  year = {1977}}

@misc{lawvere:finiteness-question,
  author = {Lawvere, F.},
  title = {Question on finiteness in toposes (thread on the category theory mailing list started by Thomas Streicher)},
  year = {1997},
  url = {https://www.mta.ca/~cat-dist/catlist/1999/finite-topos}}

@misc{madore:diary,
  author = {Madore, D.},
  title = {Mathematical diary},
  year = {2003},
  url = {http://www.madore.org/~david/math/diary.pdf}}

@article{goodwillie-lichtenbaum:cohomological-bound,
  title = {A cohomological bound for the h-topology},
  author = {Goodwillie, T. and Lichtenbaum, S.},
  journal = {Amer. J. Math.},
  volume = {123},
  number = {3},
  year = {2001},
  pages = {425--443}}

@article{perdry-schuster:noetherian,
  title = {Noetherian orders},
  author = {Perdry, H. and Schuster, P.},
  journal = {Math. Structures in Comput. Sci.},
  volume = {21},
  number = {1},
  year = {2011},
  pages = {111--124}}

@article{perdry:noetherian,
  author = {Perdry, H.},
  title = {Strongly Noetherian rings and constructive ideal theory},
  journal = {J. Symbolic Comput.},
  volume = {37},
  number = {4},
  year = {2004},
  pages = {511--535}}

@phdthesis{tennenbaum:hilbert,
  author = {Tennenbaum, J.},
  title = {A constructive version of Hilbert's basis theorem},
  school = {University of California},
  year = {1973}}

@article{perdry:lazy,
  title = {Lazy bases: a minimalist constructive theory of Noetherian rings},
  author = {Perdry, H.},
  journal = {MLQ Math. Log. Q.},
  volume = {54},
  number = {1},
  year = {2008},
  pages = {70--82}}

@incollection{coquand:classical,
  author = {Coquand, T.},
  title = {Computational content of classical logic},
  year = {1997},
  booktitle = {Semantics and Logics of Computation},
  pages = {33--78},
  editor = {Pitts, A. and Dybjer, P.},
  publisher = {Cambridge University Press}}

@incollection{feferman:kreisel,
  author = {Feferman, S.},
  title = {Kreisel's `unwinding' program},
  year = {1996},
  editor = {Odifreddi, P.},
  booktitle = {Kreiseliana. About and Around Georg Kreisel},
  publisher = {A K Peters},
  pages = {247--273}}

@book{kohlenbach:applprooftheory,
  author = {Kohlenbach, U.},
  title = {Applied Proof Theory: Proof Interpretations and their Use in Mathematics},
  publisher = {Springer-Verlag},
  year = {2008}}

@misc{kiselyov:lem,
  author = {Kiselyov, O.},
  title = {Constructive law of excluded middle},
  year = {2009},
  url = {http://okmij.org/ftp/Computation/lem.html}}

@article{richman:trivial-rings,
  author = {Richman, F.},
  year = {1988},
  title = {Nontrivial uses of trivial rings},
  journal = {Proc. Amer. Math. Soc.},
  volume = {103},
  pages = {1012--1014}}

@misc{simpson:random1,
  author = {Simpson, A.},
  year = {2009},
  title = {The locale of random sequences},
  note = {Slides for \emph{Continuity, Computability, Constructivity -- From Logic to Algorithms}},
  url = {https://homepages.inf.ed.ac.uk/als/Talks/ccc09.pdf}}

@article{simpson:random2,
  author = {Simpson, A.},
  year = {2012},
  title = {Measure, randomness and sublocales},
  journal = {Ann. Pure Appl. Logic},
  volume = {163},
  number = {11},
  pages = {1642--1659}}

@misc{gathmann:ag,
  author = {Gathmann, A.},
  title = {Algebraic geometry. Notes for a class taught at the University of Kaiserslautern~2002/2003},
  year = {2002},
  url = {http://www.mathematik.uni-kl.de/~gathmann/class/alggeom-2002/main.pdf}}

@misc{schreiber:cohesive,
  author = {Schreiber, U.},
  title = {Differential cohomology in a cohesive $\infty$-topos},
  year = {2013},
  url = {https://arxiv.org/abs/1310.7930}}

@inproceedings{schreiber-shulman:qgft,
  author = {Schreiber, U. and Shulman, M.},
  title = {Quantum gauge field theory in cohesive homotopy type theory},
  booktitle = {Proceedings 9th Workshop on Quantum Physics and Logic},
  editor = {Duncan, R. and Panangaden, P.},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {158},
  year = {2014},
  url = {https://arxiv.org/abs/1408.0054}}

@misc{riehl-shulman:synthetic-infinity-categories,
  author = {Riehl, E. and Shulman, M.},
  title = {A type theory for synthetic $\infty$-categories},
  year = {2017},
  url = {https://arxiv.org/abs/1705.07442}}

@article{kraus-escardo-coquand-altenkirch:anonymous,
  author = {Kraus, N. and Escardó, M. and Coquand, T. and Altenkirch, T.},
  title = {Notions of anonymous existence in Martin--Löf type theory},
  year = {2017},
  journal = {Log. Methods Comput. Sci},
  volume = {13},
  number = {1}}

@article{awodey-butz-simpson-streicher:bist,
  author = {Awodey, S. and Butz, C. and Simpson, A. and Streicher, T.},
  title = {Relating first-order set theories, toposes and categories of classes},
  year = {2014},
  pages = {428--502},
  volume = {165},
  journal = {Ann. Pure Appl. Logic}}

@inproceedings{pitts:polymorphism,
  author = {Pitts, A.},
  title = {Polymorphism is Set Theoretic, Constructively},
  booktitle = {Category Theory and Computer Science, Proc. Edinburgh 1987},
  year = {1987},
  pages = {12--39},
  editor = {Pitt, D. and Poigné, A. and Rydeheard, D.},
  volume = {283},
  series = {Lect. Notes Comput. Sci.},
  publisher = {Springer-Verlag}}

@misc{grothendieck:functorial-ag,
  author = {Grothendieck, A.},
  title = {Introduction to functorial algebraic geometry, part 1: affine algebraic geometry (lecture notes by F. Gaeta)},
  year = {1973}}

@inproceedings{fourman:reals,
  author = {Fourman, M.},
  title = {Comparaison des réelles d'un topos; structures lisses sur un topos élémentaire},
  booktitle = {Deuxième colloque sur l'algèbre des catégories. Amiens-1975. Résumés des conférences},
  year = {1976},
  journal = {Cah. Topol. Géom. Différ. Catég.},
  volume = {16},
  number = {3},
  pages = {233--239}}

@article{veldman:kruskal,
  author = {Veldman, W.},
  title = {An intuitionistic proof of Kruskal's theorem},
  year = {2004},
  journal = {Arch. Math. Logic},
  volume = {43},
  number = {2},
  pages = {215--264}}

@book{chai:compactification,
  author = {Chai, C.},
  title = {Compactification of Siegel Moduli Schemes},
  publisher = {Cambridge University Press},
  series = {London Math. Soc. Lecture Note Ser.},
  volume = {107},
  year = {1985}}