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.
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.
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-holconst
func : GS → BOOL
∀s• func s ≡ ∃d c g•
fttabs = (d↦g c)↦g g
fttab∧ fun g
fttab∧ dom g = d
fttab∧ 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-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)
fttab∧ rights f = snd (fst f)
fttab∧ 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)
fttab∧ 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 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-holconst
appg : GS → GS → GS
∀f g• appg f g =
fttab(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 =
fttabmk_func
fttab(lefts f)
fttab((graph f) og (graph g))
fttab(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-holconst
ccat : GS → BOOL
∀s• ccat s ≡
fttab∀t• t ∈g s ⇒ func t
fttab∧ idleft t ∈g s
fttab∧ idright t ∈g s
fttab∧ ∀u• u ∈g s
fttabfttab∧ rights t = lefts u
fttabfttab⇒ (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-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.
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-holconst
cfunc : GS → BOOL
∀f• cfunc f ≡ func f
fttab∧ (∀g• g ∈g fields f ⇒ func g)
fttab∧ ∀g h• g ∈g (lefts f)
fttabfttab∧ h ∈g (lefts f)
fttabfttab∧ rights g = lefts h
fttabfttab⇒ appg f (g ogf h)
fttabfttab= (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-holconst
cfunc_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-holconst
ccat_cfunc : GS → BOOL
∀f• ccat_cfunc f ≡ cfunc f
fttab∧ ∀c• c ∈g (fields f)
fttabfttab⇒ ccat c
Functor-Categories

xl-holconst
cfunc_ccat : GS → BOOL
∀c• cfunc_ccat c ≡ ccat c
fttab∧ ∀f• f ∈g c
fttabfttab⇒ 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-holconst
pf_hered : (GS → BOOL) → BOOL
∀p• pf_hered p ≡ ∀f•
fttabccat_cfunc f
fttab∧ (∀g• g ∈g cfunc_const f ⇒ p g)
fttab⇒ 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-holconst
pc_hered : (GS → BOOL) → BOOL
∀p• pc_hered p ≡ ∀c•
fttabcfunc_ccat c
fttab∧ (∀d• d ∈g ccat_const c ⇒ p d)
fttab⇒ 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-holconst
pure_functor : GS → BOOL
∀s• pure_functor s ≡
fttab∀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-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⌝);


up quick index © RBJ

privacy policy

Created:

$Id: pcf2-defns.xml,v 1.1 2005/04/09 14:00:53 rbj Exp $

V