FOLDS, first-order logic with dependent sorts, was introduced by me in a 1995 monograph (www.math.mcgill.ca/makkai/). It is explained in outline in the paper "Towards a categorical foundation of mathematics" published in Springer Lecture Notes in Logic, no.11, 1998. FOLDS is intended as the formal language for a foundational system  based on higher dimensional categories, analogously to ordinary first-order logic in ZFC set theory. The syntax of FOLDS is simple; it is related, although not identical, to earlier formalisms by Per Martin-Lof and John Cartmell. However, unlike the latter, FOLDS is a fully model-theoretical language, with a general Tarskian semantics and an accompanying model theory.  Its main feature is a replacement of ordinary (Fregean) equality (as in "logic with equality") by a new, signature-dependent notion of FOLDS equivalence. In its most direct application, FOLDS equivalence takes the role of isomorphism of ordinary model theory; but it also specializes, in the appropriate contexts, to equivalence of categories, biequivalence of bicategories, etc. The most important application of FOLDS equivalences appear in my definition of a universe called "The multitopic category of all multitopic categories" (1999 and 2004; the site above).

In the lectures, I will try to describe the concepts and their theory through examples, rather than general formulations. The project of the new "categorical" foundation has as its aim the establishing of a self-contained formal theory of totalities that is workable, and also fundamentally different from ordinary set-theory insofar it should be free from smallness considerations of the Cantorian type. This project is far from being completed, and the audience is invited to join in the investigation of the several precise mathematical questions as well as the more general philosophical aspects of the project.