Category Theoretic Foundation Systems
Overview
 This document creates a theory of pure concrete categories and functors. The theory contains a set of theorems which might serve as an independent axiomatisation of the theory.
 Introduction Work on foundation systems for mathematics which are ontologically category theoretic, i.e. in which the things in the domain of discourse are the stuff of category theory, categories, arrows, functors. Definitions of Pure Categories and Functors This document defines the concepts "pure category" and "pure functor" as a preliminary to developing a foundation system whose domains of discourse are the pure categories and functors.
 Axioms for Pure Categories and Functors This document creates a theory of pure concrete categories and functors. The theory contains a set of theorems which might serve as an independent axiomatisation of the theory. Definitions of Pure Abstract Categories and Functors This document defines the concepts "pure category" and "pure functor" as a preliminary to developing a foundation system whose domains of discourse are the pure categories and functors.
Introduction
 Work on foundation systems for mathematics which are ontologically category theoretic, i.e. in which the things in the domain of discourse are the stuff of category theory, categories, arrows, functors.
 What is a "Foundation System" In this context this term refers to a logical foundation for mathematics. This means, a formal deductive system sufficiently strong (in an appropriate sense) that in it the concepts of mathematics can be introduced by definition and the theorems of mathematics expressed in terms of these concepts can be formally demonstrated. No such systems were known prior to the twentieth century. The most widely accepted system in the twentieth century has been the first order formalisation of set theory known as Zermelo-Fraenkel set theory (ZFC).
 What is a "Category Theoretic" Foundation System Not an easy question to answer. Category theorists and others have made certain complaints about set theory as a foundation for mathematics, and have made some suggestions about alternative foundations. I have not myself found it easy see the connection between the complaints and the remedies, but I will mention some of each before saying something more about the kinds of "category theoretic" foundation systems which interest me personally.
Some Complaints
 well-foundedness Sauders Mac Lane in his classic texbook "Categories for the Working Mathematician" has an eary section on "Foundations". It is the purpose of that section to clarify the foundational context in which the rest of the book is to be understood, and the terminology of "small" (which actually means though he doesn't put it this way, "of accessible rank") and "large" categories (which have the smallest inaccessible rank) which is adopted. Here he remarks on the problems arising from the fact that many collections of interest to category theorists (for example, the collection of all groups) are not sets in ZFC. This problem is a consequence of the well-foundedness of the ontology of ZFC (though I doubt that Mac Lane says that).
 lack of abstraction Category theory is arguably, in a certain sense of the word, the most abstract kind of mathematics. Some category theorist, believing that the mathematics should be as it is seen through category theory, find fault with the method used in the derivation of mathematics in set theory. This method is usually considered to consist in "coding up" (or representing) the various mathematical structures as sets. The study of mathematical structures should be done without reference to particular exemplars of the structure, the structure should be studied "up to isomorphism", in abstraction from its instances. ontological extravagence Some category theorists regard category theory as being constructive, think that appropriate foundations for mathematics should also be constructive, and are hostile particularly to the outer reaches of set theoretic ontology as being the antithesis of constructive mathematics. Such constructivist antipathy to set theory is of course, not exclusive to category theorists.
 Some Remedies
 Method This stuff is all done in the context of a strong higher order set theory, i.e. gst in ProofPower HOL. The method is to construct a set theoretic semantic model of the proposed category theoretic foundation system, to make new types and define the primitive relations and operators by this means and then formulate and prove a set of theorems which would serve as an indepedent axiomatisation of the proposed foundation systems. Generally they are intended to be equivalent in strength to gst, and so in principle the gst could be reconstructed. In some cases some steps toward this have been taken.
 Three Variants I have at present in mind three categorical foundation system along the lines discussed. The first, and the only one on which I have done any work on is that in which the ontology consists of heriditarily pure concrete categories and functors, all arrows being in fact functors.
Definitions of Pure Categories and Functors
 This document defines the concepts "pure category" and "pure functor" as a preliminary to developing a foundation system whose domains of discourse are the pure categories and functors.
 Introduction Pure functors and categories are the concrete functors and categories which can be constructed by an iterative process starting from the empty category. Functor Functions A functor function is a graph together with its domain and codomain. Application and Composition Application and composition of functor functions is very similar to ordinary function application and composition. Concrete Categories and Functors A concrete category is (in our special world) just a set of functor functions which is closed under composition and has dom and cod identity functors (the objects are recoverable from the identities). A concrete functor is a functor function whose domain and codomain are sets of functor functions and which respects composition. Category-Functors and Functor-Categories A category-functor (_cfunc) is a concrete functor whose domain and codomain are concrete categories (not just sets) while a functor-category (cfunc_) is a concrete category whose elements are concrete functors (not just functor functions).
 Hereditary Properties Hereditary properties are those which are inherited as new (concrete) functors and categories are constructed from old. Pure Functors and Categories Pure functors and categories are the concrete functors and categories which can be built starting from the empty category using a sequence of alternating constructions of categories and functors from functors and categories (resp.) already constructed. Composition, Identity, Membership, Application It is now necessary to define the usual category theoretic operators over the new types. Abstraction and Galaxies Category and functor abstraction, and the Galaxy (or "Grothendieck Universe") contructor. Listing of Theory pcf-defs
Axioms for Pure Categories and Functors
 This document creates a theory of pure concrete categories and functors. The theory contains a set of theorems which might serve as an independent axiomatisation of the theory.
 Introduction Pure functors and categories are the concrete functors and categories which can be constructed by an iterative process starting from the empty category.
Definitions of Pure Abstract Categories and Functors
 This document defines the concepts "pure category" and "pure functor" as a preliminary to developing a foundation system whose domains of discourse are the pure categories and functors.
 Introduction Pure functors and categories are the concrete functors and categories which can be constructed by an iterative process starting from the empty category. Functor Functions A functor function is a graph together with its domain and codomain. Application and Composition Application and composition of functor functions is very similar to ordinary function application and composition. Concrete Categories and Functors A concrete category is (in our special world) just a set of functor functions which is closed under composition and has dom and cod identity functors (the objects are recoverable from the identities). A concrete functor is a functor function whose domain and codomain are sets of functor functions and which respects composition. Category-Functors and Functor-Categories A category-functor (_cfunc) is a concrete functor whose domain and codomain are concrete categories (not just sets) while a functor-category (cfunc_) is a concrete category whose elements are concrete functors (not just functor functions).
 Hereditary Properties Hereditary properties are those which are inherited as new (concrete) functors and categories are constructed from old. Pure Functors and Categories Pure functors and categories are the concrete functors and categories which can be built starting from the empty category using a sequence of alternating constructions of categories and functors from functors and categories (resp.) already constructed. Composition, Identity, Membership, Application It is now necessary to define the usual category theoretic operators over the new types. Abstraction and Galaxies Category and functor abstraction, and the Galaxy (or "Grothendieck Universe") contructor. Listing of Theory pcf-defs

Created:

\$Id: ctf.xml,v 1.2 2006/03/25 22:50:36 rbj01 Exp \$

V