In this course on topos theory, we mainly focus on its role in model construction, unifying techniques from forcing and Heyting-valued models to different types of realizability. We start with a very short and gentle introduction to category theory. Then, we introduce elementary toposes and as their concrete examples, we present the categories of sheaves and Heyting-valued sets, on the one hand, and the effective topos, on the other. Then, we move to the connection between topoi and logic to present a topos-theoretical version of some independence results including the independence of the continuum hypothesis and the axiom of choice. We also use toposes to realize some exotic, yet coherent possibilities including the so-called computable (resp. Brouwerian) universe in which all the functions on natural numbers (resp. real line) are computable (resp. continuous). These models are used to prove the consistency of Church-Turing thesis (resp. Brouwer's theorem on continuity of all functions on the reals) from intuitionistic arithmetic (resp. analysis).
This is an open-ended course aiming at all mathematics and computer science students, covering some parts of modern mathematics from a logical, synthetic and structural point of view. It starts with some category theory as the language of mathematical structuralism. Then, it moves to the main organizational concept of the course, i.e., the space as the world of finitely verifiable constructions. We start with the propositional part, namely the theory of locales and then move to the higher-order versions of Grothendieck toposes and higher toposes. We finally use the ultimate notion of space to touch some parts of synthetic functorial geometry as the theory of locally simple spaces.
Utrecht University
Logic and Computation, for Master Students in AI, (together with R. Iemhoff, R. Jalali), Winter 2022.
Logic and Computation, for Master Students in AI, (together with R. Iemhoff, R. Jalali), Winter 2021. Lecture Notes
Logic and Computation, for Master Students in AI, (together with R. Iemhoff), Fall 2019.
University of Tehran
Homotopy Type Theory, January - March 2020.
Geometry via Logic II, January-March 2020.
Geometry via Logic, January-March 2019, [On point-free topology and its higher version, i.e., Grothendieck toposes], References.
Category Theory, A Preliminary Course, January 2019.
Topos Theory, November-December 2018, [On topos theory from the algebraic set theory perspective].
Proof Theory of Arithmetic, August-September 2018.Martin Löf Type Theory, December 2017-January 2018.
Charles University
Bounded Arithmetic and Computational Complexity, Student Logic Seminar, (together with I. Oliveira), Fall 2015.