You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Graham Manuell (Apr 13 2023 at 11:22):I gave a course on constructive (mathematics and) pointfree topology at the TACL summer school last year and I have now put lecture notes for that course on the arXiv: https://arxiv.org/abs/2304.06000. (Later this will form a chapter of a book along with the lecture notes for the other courses.)
The constructive approach to mathematics has the advantage that witnesses can be extracted from statements of existence and theorems can be unwound to give algorithms. Even better, constructive theorems can be interpreted in any topos, giving many different results for the price of one. On the other hand, you might have heard that fundamental results from topology such as Tychonoff's theorem or even the intermediate value theorem do not hold constructively, which can make the price of constructive theorems seem rather steep. However, almost all of these pathologies disappear if we take the pointfree approach to topology, in which spaces are studied algebraically and logically through their lattices of opens without reference to a predefined underlying set of points. In fact, this perspective also sheds light on aspects of constructive mathematics that might at first appear to have little to do with topology. These notes provide a gentle introduction to the main aspects of constructive pointfree topology and some of its applications.
I hope that the notes are accessible to anyone with only very basic knowledge of topology, category theory and lattice theory and I have tried to give motivation for the different concepts involved. (On the other hand, anyone who looking for an extensive treatment of topos theory will be disappointed.) Any comments would be welcome.