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 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
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 Saunders 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 but 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 choose a different language, choose a different ontology. If you choose 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. The merits of non-well-founded set theories are discussed elsewhere. 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 codomain.
 xl-holconstfunc : GS → BOOL ∀s• func s ≡ ∃c g• s = c ↦g g ∧ fun g ∧ ran g ⊆g c
Of course, a functor is thought of as having a specific domain as well, but since we are thinking of conrete functors we expect the graph to be a total function, and its better to omit the domain than to include the domain redundantly are require the graph to be total over that domain (from the point view of simplicity of the underlying theory, the resulting theories are identical)
Constructor
A constructor function is defined as follows:
 xl-holconstmk_func : GS → GS → GS ∀c g• mk_func c g = c ↦g g
Projections
The projection functions are defined as follows:
 xl-holconstdoms cods graph : GS → GS ∀f• doms f = dom (snd f) ∧ cods f = fst f ∧ graph f = snd f
The final "s" should warn you that the result is a set.
 xl-gft func_thm = ⊢ ∀ f• func f ⇒ fun (graph f) ∧ ran (graph f) ⊆g cods f

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 : GS → GS ∀f• idff f = mk_func f (id f)
Then we use it to define the dom and cod identity functors.
 xl-holconstiddom idcod : GS → GS ∀f• iddom f = idff (doms f) ∧ idcod f = idff (cods f)
Later dom and cod 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 : GS → GS ∀f• fields f = doms f ∪g cods 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 functor is application of its graph.
 xl-holconstappg : GS → GS → 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.
 xl-gft appg_thm1 = ⊢ ∀ f x• func f ⇒ (∃1 y• x ↦g y ∈g graph f) ⇒ x ↦g appg f x ∈g graph f appg_thm2 = ⊢ ∀ f x• func f ∧ x ∈g doms f ⇒ x ↦g appg f x ∈g graph f appg_thm3 = ⊢ ∀ f x y• func f ∧ x ↦g y ∈g graph f ⇒ appg f x = y appg_thm4 = ⊢ ∀ f x• func f ∧ x ∈g doms f ⇒ appg f x ∈g cods f

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 : GS → GS → GS ∀f g• f ogf g = mk_func (cods f) ((graph f) og (graph 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 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.
Concrete Categories
A category is a collection of "func"s which is closed under composition and has dom and cod identities.
 xl-holconstccat : GS → BOOL ∀s• ccat s ≡ ∀t• t ∈g s ⇒ func t ∧ iddom t ∈g s ∧ idcod t ∈g s ∧ ∀u• u ∈g s ∧ doms t = cods u ⇒ (t ogf u) ∈g 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 : GS → GS ∀c• ccat_const c = (Imagep doms c) ∪g (Imagep cods c)
This is 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 func which respects composition.
 xl-holconstcfunc : GS → BOOL ∀f• cfunc f ≡ func f ∧ (∀g• g ∈g fields f ⇒ func g) ∧ ∀g h• g ∈g (doms f) ∧ h ∈g (doms f) ∧ doms g = cods h ∧ (g ogf h) ∈g (doms f) ⇒ doms (appg f g) = cods (appg f 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 : GS → GS ∀f• cfunc_const f = (doms f) ∪g (cods f)
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).
Category-Functors

 xl-holconstccat_cfunc : GS → BOOL ∀f• ccat_cfunc f ≡ cfunc f ∧ ccat (doms f) ∧ ccat (cods f)
Functor-Categories

 xl-holconstcfunc_ccat : GS → BOOL ∀c• cfunc_ccat c ≡ ccat c ∧ ∀f• f ∈g 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 : (GS → BOOL) → BOOL ∀p• pf_hered p ≡ ∀f• ccat_cfunc f ∧ (∀g• g ∈g cfunc_const f ⇒ p g) ⇒ p f
Lemmas
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 : (GS → BOOL) → BOOL ∀p• pc_hered p ≡ ∀c• cfunc_ccat c ∧ (∀d• d ∈g ccat_const c ⇒ p d) ⇒ p c
Lemmas
Lemmas Connecting these Concepts
 Lemmas
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.
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 : GS → BOOL ∀s• pure_functor s ≡ ∀p• pf_hered p ⇒ p s
consistency proof and type definition
We now prove that there exists a pure function, and introduce the type PF of pure functors.
 xl-gft pure_functor_exists ⊢ ∃x• pure_functor x

Lemmas

 xl-gft pf_≡_lem1 = ⊢ ∀ f• pure_functor f ≡ ccat_cfunc f ∧ (∀ g• g ∈g cfunc_const f ⇒ pure_functor g)

Pure Categories
A pure category is a category all of whose members (the arrows) are pure functors.
 xl-holconstpure_category : GS → BOOL ∀c• pure_category c ≡ ∀p• pc_hered p ⇒ p c
consistency proof and type definition
It is proved that there exists a pure category and the type PC of pure categories is introduced:
 xl-gft pure_category_exists ⊢ ∃x• pure_category x

Lemmas

 xl-gft pc_≡_lem1 = ⊢ ∀ c• pure_category c ≡ cfunc_ccat c ∧ (∀ d• d ∈g ccat_const c ⇒ pure_category d)

 xl-gft pf_≡_lem2 = ⊢ ∀ f• pure_functor f ≡ cfunc f ∧ pure_category (doms f) ∧ pure_category (cods f)

 xl-gft pc_≡_lem2 = ⊢ ∀ c• pure_category c ≡ c ∧ (∀ g• g ∈g c ⇒ pure_functor g)

Composition, Identity, Membership, Application
 It is now necessary to define the usual category theoretic operators over the new types.
Representation and Abstraction Functions
ProofPower doesn't give you these for free, only the existence of the bijection. In principle you can manage without defining these functions, but its easier to define them and then use them to define the required operations over the new types.
 xl-holconstpf_rep : PF → GS; mk_pf : GS → PF OneOne pf_rep ∧ (∀x• mk_pf (pf_rep x) = x) ∧ (∀x• pure_functor x ≡ (∃ y• x = pf_rep y))

 xl-holconstpc_rep : PC → GS; mk_pc : GS → PC OneOne pc_rep ∧ (∀x• mk_pc (pc_rep x) = x) ∧ (∀x• pure_category x ≡ (∃ y• x = pc_rep y))
Definitions

 xl-sml declare_infix (310, "of");

 xl-holconst\$of : PF → PF → PF ∀f g• f of g = mk_pf ((pf_rep f) ogf (pf_rep g))

 xl-holconst\$idf : PC → PF ∀c• idf c = mk_pf (idff(pc_rep c))

 xl-holconst\$domc : PF → PC ∀f• domc f = mk_pc (doms(pf_rep f))

 xl-holconst\$codc : PF → PC ∀f• codc f = mk_pc (cods(pf_rep f))
Elementary Theorems

 xl-gft pf_pf_rep_thm = ⊢ ∀f• pure_functor (pf_rep f) cf_cf_rep_thm = ⊢ ∀c• pure_category (pc_rep c) pf_inv_thm = ⊢ ∀ x• pure_functor x ⇒ pf_rep (mk_pf x) = x pc_inv_thm = ⊢ ∀ x• pure_category x ⇒ pc_rep (mk_pc x) = x idff_closure_lem = ⊢ ∀ c• pure_category c ⇒ pure_functor (idff c) func_comp_thm = ⊢ ∀ x y• func x ∧ func y ⇒ func (mk_func (cods x) (graph x og graph y))=XML fields_⊆g_thm = ⊢ ∀ f g• fields (f ogf g) ⊆g fields f ∪g fields g appg_ogf_thm = ⊢ ∀x y g• func x ∧ func y ∧ doms x = cods y ∧ g ∈g doms y ⇒ appg (x ogf y) g = appg x (appg y g)

Membership
Membership is a relation between functors and categories. A relationship between categories and categories will be defined from it,
 xl-sml declare_infix(310, "∈f");

 xl-holconst\$∈f : PF → PC → BOOL ∀f c• f ∈f c ≡ (pf_rep f) ∈g (pc_rep c)
Functor Application

 xl-sml declare_infix(310, "f");

 xl-holconst\$f : PF → PF → PF ∀f g• f f g = mk_pf(appg (pf_rep f) (pf_rep g))
Abstraction and Galaxies
 Category and functor abstraction, and the Galaxy (or "Grothendieck Universe") contructor.
Category Abstraction
This is analogous to separation in set theory. Possibly this could have been defined in terms of functorial abstraction.
 xl-holconstSepc : PC → (PF → BOOL) → PF ∀c p• Sepc c p = mk_pf (Sep (pc_rep c) (λs• ∃f• s = pf_rep f ∧ p f))
Functorial Abstraction

 xl-holconstΛf : PC → (PF → PF) → PF ∀pc pfpf• Λf pc pfpf = mk_pf (mk_func (Imagep (pf_rep o pfpf o mk_pf) (pc_rep pc)) (Imagep (λf• (f ↦g pf_rep (pfpf (mk_pf f)))) (pc_rep pc)))
Galactic Categories
The following defines a function which takes a pure category and returns the smallest galactic category which contains it. A function taking a functor and returning the smallest containing galactic category is easy to define from it.
 xl-holconstGc : PC → PC ∀pc• Gc pc = mk_pc (Sep (Gx (pc_rep pc)) pure_functor)