Axioms for Pure Categories and Functors.
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 Pure functors and categories are the concrete functors and categories which can be constructed by an iterative process starting from the empty category.
Introduction
 Pure functors and categories are the concrete functors and categories which can be constructed by an iterative process starting from the empty category.
The Theory pcf-axs
First we introduce for these definitions the new theory "pcf-axs", a child of "pcf-defs".
 xl-sml open_theory "pcf-defs"; force_new_theory "pcf-axs"; force_new_pc "pcf-axs"; set_merge_pcs ["gst","pcf-defs","pcf-axs"];

Elementary Axioms
 Provisional Axiomatisation This is my guess at a set of "axioms", entered as axioms. They should all be provable, and as they are proved the axioms will be removed. I could have used conjectures instead of axioms, but then I would not have been able to reason from them. There is a sense in which the nature of sets is fully captured by the axiom of extensionality, the remaining axioms of set theory telling us not what a set is, but what sets there are. In the axiomatisation I moot here for my categorical foundation system, the pattern of saying what kinds of thing exist and then saying which of these kinds of entity are found in the domain of discourse is retained. The things which exist are (pure, concrete) categories and functors rather than sets. Our categories and functors are extensional, but they are more complex than sets, and so saying that these functors and categories are extensional still leaves more to be said about what categories and functors are before we pass to saying which of these kinds of entity are in our domain of discourse. Extensionality comes in two flavours of course, though they may not be independent.

 xl-sml new_axiom (["pc_ext"], ⌜∀c1 c2• c1 = c2 ≡ (∀f• f ∈f c1 ≡ f ∈f c2)⌝); new_axiom (["pf_ext"], ⌜ ∀f1 f2• f1 = f2 ≡ (domc f1 = domc f2) ∧ (codc f1 = codc f2) ∧ (∀f• f ∈f domc f1 ⇒ f1 f f = f2 f f) ⌝);

The other things to be said, before we pass to purely ontological principles are (roughly) as follows:
1. that id yields an identity functor
2. that well-typed composition is associative
3. that categories have identity functors and are closed under well-typed composition

 xl-sml new_axiom (["associative_axiom"], ⌜ ∀f g h:PF• codc h = domc g ∧ codc g = domc f ⇒ f of (g of h) = (f of g) of h ⌝); new_axiom (["identity_axiom"], ⌜ ∀c:PC; f:PF• (domc f = c ⇒ (idf c) of f = f) ∧ (codc f = c ⇒ f of (idf c) = f) ⌝);

Before giving the category closure axiom it is convenient to define a membership relation between categories.
 xl-sml declare_infix (300, "∈c");

 xl-holconst \$∈c : PC → PC → BOOL ∀c d• c ∈c d ≡ idf c ∈f d
The closure axioms can then be stated:
 xl-sml new_axiom (["pc_closure_axiom"], ⌜ ∀c:PC; f g:PF• (f ∈f c ⇒ domc f ∈c c ∧ codc f ∈c c ∧ (g ∈f c ∧ domc f = codc g ⇒ (f of g) ∈f c)) ⌝);

In saying which of these things appears in our domain of discourse we begin with a negative principle, the principle of well-foundedness. This tells us that anything which is ill-founded doesn't exist, even if it satisfies all the other principles.

Well-foundedness is I think nicer given as an induction principle, at least it is so long as we are working in a higher order logic. One principle suffices and the one for pure functors seems neater.
 xl-sml new_axiom (["pf_induction"], ⌜ ∀p• (∀f• (∀g• (g ∈f domc f ∨ g ∈f codc f) ⇒ p g) ⇒ p f) ⇒ ∀f• p f⌝);

From this an induction principle for pure categories should be derivable.
 Now the difficult one, the ontology axiom, which serves to place lower bounds on what exists. Its useful to define galactic categories and then write the axiom in terms of that definition. This is rather more difficult to state for category theoretic foundations than for set theoretic so its best to make some definitions first. The things we to defined are: transitive categories functorial abstraction limits and co-limits of functors functor space categories The ontology axiom asserts that every functor belongs to some category which is transitive and which is closed under limits and co-limits, functorial abstraction and construction of functor space categories. Functorial abstraction plays a role similar to the replacement axiom in ZFC (which subsumes separation when suitably stated), closure under limits and co-limits that if the closure under unions and intersections, closure under functor space categories plays the role of closure under formation of powersets. It seems better here to use a function rather than a relation for functorial abstraction, but this prevents the empty category from being defined this way and we might need to assert the existence of the empty category. However, asserting the existence of limits and co-limits is stronger than closure under unions and ought to give us the empty category. Its not so specific as the set theoretic union axiom, and therefore may not be sufficient for present purposes.
The following is the gst ontology axiom in the process of being massaged into a pcf ontology axiom.
 xl-gft new_axiom (["pcf_ontology_axiom"], ⌜ ∀c• ∃g• c ∈g g ∧ ∀d• d ∈g g ⇒ d ⊆c g ∧ (∃p• (∀v• v ∈g p ≡ v ⊆g d) ∧ p ∈g g) ∧ (∃u• (∀v• v ∈g u ≡ ∃w• v ∈g w ∧ w ∈g d) ∧ u ∈g g) ∧ (∀rel• ManyOne rel ⇒ (∃r• (∀v• v ∈g r ≡ ∃w • w ∈g d ∧ rel w v) ∧ (r ⊆g g ⇒ r ∈g g)))⌝ );

In the above "ManyOne" is not enough, rel must respect composition.