Definitions of Pure Abstract 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 abstract 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 abstract functors and categories which can be constructed by an iterative process starting from the empty category.
Goals
 1. Goals This is a variant of pure categories and functors in which the categories and functors are not concrete. I don't actually remember why I made them concrete in the first version. I guess that seemed natural and simple. We shall see whether it really is more complicated to have abstract categories. One benefit of the abstract approach is that it will allow ill-founded categories.
The Theory pcf2-defs
First we introduce for these definitions the new theory "pcf2-defs", a child of gst.
 xl-sml open_theory "gst"; force_new_theory "pcf2-defs"; force_new_pc "pcf2-defs"; set_merge_pcs ["gst","pcf2-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 : GS → BOOL ∀s• func s ≡ ∃d c g• s = (d↦g c)↦g g ∧ fun g ∧ dom g = d ∧ ran g ⊆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 : GS → GS → GS → GS ∀l g r• mk_func l g r = (l ↦g r) ↦g g
Projections
The projection functions are defined as follows:
 xl-holconstlefts rights graph : GS → 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 : GS → 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 : GS → 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 : GS → GS ∀f• fields f = lefts f ∪g 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 : 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. 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 (lefts f) ((graph f) og (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 : GS → BOOL ∀s• ccat s ≡ ∀t• t ∈g s ⇒ func t ∧ idleft t ∈g s ∧ idright t ∈g s ∧ ∀u• u ∈g s ∧ rights t = lefts 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 = ⋃g (Imagep 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 : GS → BOOL ∀f• cfunc f ≡ func f ∧ (∀g• g ∈g fields f ⇒ func g) ∧ ∀g h• g ∈g (lefts f) ∧ h ∈g (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 : GS → GS ∀f• cfunc_const f = (lefts f) ∪g (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 : GS → BOOL ∀f• ccat_cfunc f ≡ cfunc f ∧ ∀c• c ∈g (fields f) ⇒ ccat c
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
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
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 : 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 : 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⌝);