Definitions of Pure Abstract Categories and Functors.
Pure functors and categories are the abstract functors and categories which can be constructed by an iterative process starting
from the empty category.
|
A functor function is a graph together with its domain and codomain.
|
Application and composition of functor functions is very similar to ordinary function application and composition.
|
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.
|
A concrete functor is a functor function whose domain and codomains are sets of functor functions and which respects composition.
|
|
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 are those which are inherited as new (concrete) functors and categories are constructed from old.
|
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 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.
|
|
|
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 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.
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-holconst mk_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-holconst lefts 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-holconst idff : GS → GS
|
∀f• idff f = mk_func f (id f) f
|
Then we use it to define the left and right identity functors.
xl-holconst idleft 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-holconst fields : GS → GS
|
∀f• fields f = lefts f ∪g rights f
|
|
|
Application of Functors
Application of a functors is application of its graph.
xl-holconst appg : 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");
|
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.
|
|
Categories
A category is a collection of "func"s which is closed under composition and has left and right identities.
|
|
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-holconst ccat_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.
|
|
Definition
A concrete functor is a func which respects composition.
|
|
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-holconst cfunc_const : GS → GS
|
∀f• cfunc_const f = (lefts f) ∪g (rights f)
|
|
|
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.
|
|
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.
|
|
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-holconst pure_functor : GS → BOOL
|
∀s• pure_functor s ≡ ∀p• pf_hered p ⇒ p s
|
|
|
Pure Categories
A pure category is a category all of whose members (the arrows) are pure functors.
xl-holconst pure_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⌝);
|
|
|