Definitions of pure categories and functors.
Overview
 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 A concrete category is (in our special world) just a set of functor functions which is closed under composition and has left and right identities. Concrete Functors A concrete functor is a functor function whose domain and codomains are sets of functor functions and which respects composition.
 Category-Functors and Functor-Categories A category-functor (ccat_cfunc) is a concrete functor whose domain and codomain are concrete categories (not just sets) while a functor-category (cfunc_ccat) 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 Pure functors are the concrete functors 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. Pure Categories Pure categories are the concrete 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. Listing of Theory pcf-defs
Introduction
 Pure functors and categories are the concrete functors and categories which can be constructed by an iterative process starting from the empty category.
Goals
 1. Goals I regard this work as frivolous. It is motivated more by curiosity than by any expectation of applicability. Nevertheless, there are some fairly definite objectives in mind. 2. Categorical Foundations There is a long running extant debate between certain category theorists and others about whether category theory can offer better foundations for mathematics than set theory. To some extent this debate is fuelled by ambiguity about what a foundation is, and it may be that what some of these category theorists are thinking of is not the kind of thing which I call a "logical foundation for mathematics". In this sense, a logical foundation is simply any logical system within which the main body of mathematics can be developed by conservative extension, i.e. following Frege's formula: Mathematics = Logic + Definitions With a liberal interpretation of what can be used as a logic (you need something with a decently high "proof theoretic strength", i.e. something like set theory, if you want to provide a foundation for classical mathematics). This material explores one way of providing a "logical foundation" for mathematics based on category theory.
 3. Existing Approaches The kinds of foundational story provided by category theorists seem to me largely irrelevant to the problems which they identify with set theoretic foundations. So far as I understand them there are two kinds of problem. The first kind is explained in the introduction to Sauders Mac Lane's "Categories for the Working Mathematician", in which observes that many of the things which one would like to be categories aren't. It should be fairly obvious here that the complaint arises from the well-foundedness of classical set theory, and is essentially ontological. The only answer to this kind of problem is a "non-well-founded" foundation system (set-theoretic or otherwise), and I have not come across any category theorists arguing for this kind of system. The other kind of problem is linguistic. Category theory is often thought of as a better way of talking, and in this respect is somewhat coy. Not only does category theory provide a new way of talking, it regards the previous idioms as disreputable, and therefore a category theorist might seek a foundation system which has the same domain of discourse but a new vocabulary. Perhaps the most common approach to categorical foundations follows this line, usually through topos theory. The idea is not that sets are the wrong thing to have in your universe, but that we should talk about them in a more abstract way. The other kind of foundational innovation which has been advocated by category theorists (notably Mac Lane) is the use of weak set theories. This apparently on the grounds that the strength of existing theories is not necessary. I am completely unaware of any category theoretic rationale for this kind of innovation, which is in any case, not very innovative, and does not offer to fix either of the kinds of problem which I identified above (and I don't know of any kind of problem at all that it fixes, except perhaps ontological vertigo).
 4. Problems with Alternatives There are two kinds of problems which can be raised with these alternatives. Firstly that the proposed systems are in pragmatic ways, less good than classical foundations. Secondly that the proposed approaches are fundamentally incapable of providing adequate foundations for classical mathematics. The proposals here are an answer to the second kind of objection. The "can't be done" objection can be made to hold water where a weak foundation system is proposed as adequate for the whole of classical mathematics, and support for this answer can probably be found in "reverse mathematics" (if one needs to look that far). However, where weakness is not a definitive part of the proposed alternative (as it is in Mac Lane's set theories), the "can't be done" objection is on weak grounds. Once you have a weak foundation system it can be made technically adequate by nasty by effective (in principle) ways of importing proof theoretic strength, such as adding an axiom asserting the consistency of ZFC. Though this approach would probably not yield a practically useful foundation, it would yield a technically sufficient one (i.e. the results derivable would encompass those derivable in ZFC).
 5. Another Kind of Alternative Don't just chose a different language, chose a different ontology. If you chose a non-well-founded ontology you can solve some of the problems of categories that don't exist in classical set theory (e.g. the category of categories), but you tend to find that other things happen which you might not like (e.g. the category of categories might not be cartesian closed). You are also likely to find it difficult to get strength in a nice usable way, and you may find that people complain about the lack of intuition about your ontology. You can have a completely category theoretic ontology which is ontologically as rich and intuitively as comprehensible as classical set theory, and on that base contruct a foundational system which is category theoretic and strong. Not sure how "pragmatic" it would be. This is what we are exporing. 6. Another Kind of Negative Claim Though a part of this enterprise is just to show that a negative result about category theoretic foundations is hard to establish, I might say that my main gripe about such a claim is that it is just too vague to be capable of establishment. How do we know which foundation systems are "categorical". It seems to me quite obvious that one can have technically adequate foundation systems which are categorical, either in the linguistic sense, by adding consistency of ZFC into topos theory, or in the ontological sense, by the means explored here. However, adding consistency of ZFC into topos theory might only be possible by the use of language which category theorists abjure (and the ontological approach adopted here is likely to be linguistically distasteful to category theorists). Its just possible (though I still think unlikely) that if one could clarify the linguistic proscriptions which category theorists advocate you would end up with a fundamentally limited language.
The Theory pcf
First we introduce for these definitions the new theory "pcf-defs", a child of gst.
 xl-sml open_theory "gst"; force_new_theory "pcf-defs"; force_new_pc "pcf-defs"; set_merge_pcs ["gst","pcf-defs"];

Functor Functions
 A functor function is a graph together with its domain and codomain.
Functor Functions
A functor is a function which may have a codomain which is larger than its range, and which cannot therefore be represented just by its graph. We therefore define first a special kind of function, which we call a "func" (think of the "c" as hinting the connection with categories), and which consists of an graph together with its domain and codomain.
 xl-holconstfunc : 'a GS BOOL s func s d c g s = (dc)g fun g dom g = d ran g c
Of course, the "d" component here is redundant since it can be recovered from the graph, so maybe it should omitted. I'm going to wait and see whether it gets in the way in the proofs.
Constructor
A constructor function is defined as follows:
 xl-holconstmk_func : 'a GS 'a GS 'a GS 'a GS l g r mk_func l g r = (l r) g
Projections
The projection functions are defined as follows:
 xl-holconstlefts rights graph : 'a GS 'a GS f lefts f = fst (fst f) rights f = snd (fst f) graph f = snd f
The final "s" should warn you that the result is a set. Next we define analogues which return functor (still as sets however).
Identity Functor Functions
First we define a function which converts an arbitrary set into an identity functor function over that set.
 xl-holconstidff : 'a GS 'a GS f idff f = mk_func f (id f) f
Then we use it to define the left and right identity functors.
 xl-holconstidleft idright : 'a GS 'a GS f idleft f = idff (lefts f) idright f = idff (rights f)
Later left and right will be defined as functions over a new type "PFc" of pure functors.
Field
Its handy to have this definition of the union of the domain and codomain:
 xl-holconstfields : 'a GS 'a GS f fields f = lefts f rights f
Application and Composition
 Application and composition of functor functions is very similar to ordinary function application and composition.
Application of Functors
Application of a functors is application of its graph.
 xl-holconstappg : 'a GS 'a GS 'a GS f g appg f g = (graph f) g g
We introduce here the use of suffix f for something which operates on functors or the sets which represent them. In the latter case a "g" is appended to the name to distinguish it from the corresponding operation which will later be defined over the type of functors. Composition of functors is associative, and in our concrete categories composition is always this operation.
Composition of Functors
Composition of functors is essentially composition of their graphs.
 xl-sml declare_infix(240,"ogf");

 xl-holconst\$ogf : 'a GS 'a GS 'a GS f g f ogf g = mk_func (lefts f) ((graph f) o (graph g)) (rights g)
We introduce here the use of suffix f for something which operates on functors or the sets which represent them. In the latter case a "g" is appended to the name to distinguish it from the corresponding operation which will later be defined over the type of functors. Composition of functors is associative, and in our concrete categories composition is always this operation.
Concrete Categories
 A concrete category is (in our special world) just a set of functor functions which is closed under composition and has left and right identities.
Categories
A category is a collection of "func"s which is closed under composition and has left and right identities.
 xl-holconstccat : 'a GS BOOL s ccat s t t s func t idleft t s idright t s u u s rights t = lefts u (t ogf u) s
Category Constituents
Categories are built out of categories. In order to express the purity requirement which is characteristic of the categories in our chosen domain of discourse ("pure" as in "pure set", suitably modified for categories), we need to be able to talk about the categories which are immediate constituents of some category (analogously to the members of a set).
 xl-holconstccat_const : 'a GS 'a GS c ccat_const c = (Image lefts c)
This is the union of the set which is the image of the category under left projection, i.e. the union of the domains of all the functors in the category.
Concrete Functors
 A concrete functor is a functor function whose domain and codomains are sets of functor functions and which respects composition.
Definition
A concrete functor is a func which respects composition.
 xl-holconstcfunc : 'a GS BOOL f cfunc f func f (g g fields f func g) g h g (lefts f) h (lefts f) rights g = lefts h appg f (g ogf h) = (appg f g) ogf (appg f h)
Functor Constituents
Functors are built out of functors. In order to express the purity requirement which is characteristic of the functors in our chosen domain of discourse ("pure" as in "pure set", suitably modified for functors), we need to be able to talk about the functors which are immediate constituents of some functor (analogously to the members of a set).
 xl-holconstcfunc_const : 'a GS 'a GS f cfunc_const f = (lefts f) (rights f)
Category-Functors and Functor-Categories
 A category-functor (ccat_cfunc) is a concrete functor whose domain and codomain are concrete categories (not just sets) while a functor-category (cfunc_ccat) is a concrete category whose elements are concrete functors (not just functor functions).
Category-Functors

 xl-holconstccat_cfunc : 'a GS BOOL f ccat_cfunc f cfunc f c c (fields f) ccat c
Functor-Categories

 xl-holconstcfunc_ccat : 'a GS BOOL c cfunc_ccat c ccat c f f c cfunc f
Hereditary Properties
 Hereditary properties are those which are inherited as new (concrete) functors and categories are constructed from old.
 Ideally, so far as clarity is concerned, we would here define two mutually recursive properties of properties, one for functors and the other for categories. However, in practice there would be difficulties in demonstrating the consistency of such a definition which would make necessary one of two other approaches to establishing the existence of the desired properties.
 One approach would be to take one of the properties as primary, define it first and then define the other in terms of it. Its not immediately obvious which one to start with. So I've done them both. Naturally, having defined each independently I don't need to define either in terms of the other. However, the theorems which show how they interlink may prove useful, we probably want to end up as if we had defined them mutually.
functor hereditary properties
A property of an ordered pair of sets is "pf_hered" if a functor inherits this property from its constituent functors. i.e. if all functors whose constituents are pf_hered functors are themselves pf_hered.
 xl-holconstpf_hered : ('a GS BOOL) BOOL p pf_hered p f ccat_cfunc f (g g cfunc_const f p g) p f
category hereditary properties
(probably to be scrapped) A property of a category is "pc_hered" if a category inherits this property from its constituent categories. i.e. if all categories whose constituents are pc_hered categories are themselves pc_hered.
 xl-holconstpc_hered : ('a GS BOOL) BOOL p pc_hered p c cfunc_ccat c (d d ccat_const c p d) p c
Pure Functors
 Pure functors are the concrete functors 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.
Pure Functors
A pure functor is a functor which has all the pcf_hereditary properties. This is an oblique way of saying that the functor can be constructed from the trivial endo-functor over the empty category by a process which involves only the formation of functors from functors already constructed.
 xl-holconstpure_functor : 'a GS BOOL s pure_functor s p pf_hered p p s
Pure Categories
 Pure categories are the concrete 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.
Pure Categories
A pure category is a category all of whose members (the arrows) are pure functors.
 xl-holconstpure_category : 'a GS BOOL c pure_category c p pc_hered p p c
consistency proof
We now prove that there exists a pure function.
 xl-sml set_goal([],x pure_functor x);