A BRICS Mini-Course
May 20 and 22, 1997
Lectures by
Michael Makkai
McGill University, Canada
One of the bases of this series of lectures is a monograph of mine entitled First Order Logic with Dependent Sorts, accepted for the Lecture Notes of Logic, Springer Verlag, presently (still) under revision. Another is my paper Avoiding the axiom of choice in general category theory J. Pure and Applied Algebra 108 (1996), 109-173. A third one is a joint paper with C. Hermida and J. Power, On higher dimensional categories, whose draft I am in the last frantic days of finishing. The latter gives a modified version of the definition for ``weak n-category'', presented in J. Baez's and J. Dolan's recent paper, an approximate title of which is Higher dimensional algebra: a definition of weak n-category. A fourth source is an essentially expository paper of mine, Towards a categorical foundation of mathematics, to appear in the Proceedings of the Haifa Logic Colloquium, 1995.
My interest in higher dimensional categories is based on the view that they form the universe of the foundation proposed in the fourth item, which foundation may also be called the Structuralist Foundation of Mathematics (SFM). First Order Logic with Dependent Sorts (FOLDS) provides the syntax SFM. FOLDS is based on a more general variant of first order logic, whose formulation is fibrational (hyperdoctrinal), and which also serves the purposes of a general concept of (bi)simulation; I call ``theories'' in this logic ``quantificational fibrations'' (QF's). Each QF L canonically gives rise to the notion of ``L-equivalence'' of L-structures. For any one of a number of examples of QF's relevant to models of computation, L-equivalence is a notion of bisimulation for computations of the given kind. The quantificational fibration L itself is then related to the Henessy-Milner logic associated with the instance of bisimulation at hand. Quantificational fibrations, and in particular FOLDS, provides a general notion of equivalence for categorical structures, which notion works out to be the standard one in a number of cases. The logic and the notion of equivalence are precisely matched: in the logic, exactly those first order properties can be expressed that are invariant under the equivalence. The theory of higher dimensional categories, which is only in its beginnings at this point, is being developed, in my inverstigations, in the context of FOLDS.