Peter Aczel
(a) Constructive Set Theory and formal topology
Constructive Set Theory (CST) was initiated by John Myhill in 1975
with an intuitionistic axiom system for constructive mathematics that
was essentially a subsystem of ZFC, but might be an appropriate formal
foundational language for Bishop style constructive mathematics that
did not assume the full impredicativity of IZF (Intuitionistic Zermelo
Fraenkel set theory).
In practise constructive mathematics can be carried out in CST in much
the same style as classical mathematics can be carried out in ZFC, with
natural numbers, ordered pairs, functions etc. treated in the usual
set theoretical style.
In my first tutorial I will focus on the axiom systems CZF and CZF+REA, the first of which which is closely related to Myhill's axiom system, except that Myhill assumed DC (Dependent Choices). CZF+REA+DC has a natural interpretation in Martin-Löf's Type Theory, showing that the ideas of constructive set theory have a natural interpretation on the basis of the fundamental constructive ideas of the type theory.
There are good reasons to drop DC and focus on CZF and CZF+REA, one reason being that sheaf reinterpretations generally hold in CZF and probably also in CZF+REA, but DC often fails.
The tutorial will be divided into the following parts:
References
(b) Logic-enriched type theory and formal topology
Logic-enriched Type Theory is a variant of Martin-Löf's Type Theory
which treats both data types and propositions as primitive and so does
not assume the type theoretic axiom of choice.
By including suitable collection principles in the type theory constructive
mathematics can be developed in the type theory.
The advantage of logic-enriched type theory over standard Martin-Löf type theory is that sheaf reinterpretations are generally expected to be possible for logic-enriched type theories in a form that mirror such reinterpretations in set theory and category theory.
In the first part of this tutorial I focus on logic-enriched type theory, its relationships with constructive set theory and with standard Martin-Löf type theory. In the second part I look at how some of the notions of formal topology might be presented in logic-enriched type theory.
References
Bernhard Banaschewski
(a) Uniformity in pointfree topology
An introduction to the notion of uniformity on a frame and various concepts connected with this such as: completeness, completion, Cauchy completeness and Cauchy completion, uniformities and compactifications, special uniformities.
Readings
(b) The real numbers in pointfree topology
The frame L(R) of reals and some of its basic properties. The completeness of L(R) as uniform frame. The real-valued continuous functions on a frame L ( = the homomorphisms L(R) -->L) and their role in relation to complete regularity and normality of frames. The ring RL of real valued continuous functions on a frame L and its subring ZL of integer-valued functions. The real uniformity of a completely regular frame.
Readings
Giovanni Sambin
(a) Basic picture and formal topology I
Readings
(b) Basic picture and formal topology II
Readings
Silvio Valentini
(a) A primer for type theory
This part of the tutorial is meant to be a short introduction to that
fragment of type theory which is relevant to formal topology.
Thus I intend to give a general introduction to Martin-Loef type theory
first by focusing on the idea of inductively generated type and then
by observing that this lead to the fact that the collection of the subsets
of a given set cannot be a set.
Then I will recall that it is still possible to deal with subsets, and
their algebra, within type theory if quantification over them is avoided
or limited to the case of set-indexed families of subsets.
(b) A complete formalization of formal topology
The second part of my tutorial will deal with the problem of the completeness of the actual formalization of formal topology. Indeed the conditions that we require on the cover relation and the positivity predicate are clearly valid in any concrete topological space but nothing guarantee for their completeness. To solve this problem I will analyze the structure of the subsets of a Heyting algebra which correspond to the concrete closed and open sets of a topological space. In this way the rules for a complete formalization of constructive topology are disclosed.Readings
For type theory, the classical references are the books by Martin-Löf and by Nordstrom-Peterson-Smith, but many other shorter introduction are available, also in the internet. As concerning the second part it can be useful to read my paper "A complete and predicative formalization of constructive topology" which can be found in my web page within the section "work in progress".