A Theory of Pure Categories

A new "pc" theory is created as a child of "hol".

This is a place holder.

The new theory is first created, together with a proof context which we will build up as we develop the theory.

xl-sml

open_theory "hol";
force_new_theory "pc";
force_new_pc "pc";
merge_pcs ["xl_cs_

_conv"] "pc";
set_merge_pcs ["hol", "pc"];

xl-sml

new_type("C",0);
new_type("F",0);

In this theory we have available both composition and application. Probably one can manage with only composition, but its easier for me to have both.

xl-sml

declare_infix (240, "_o");
new_const("_o",

);
declare_infix (240, "_a");
new_const("_a",

);

We also have a membership relation which asserts that a morphism is a member of a category.

xl-sml

declare_infix (240, "

_f");
new_const("

_f",

BOOL

);

Before we can say much at all we also need the domain and codomain functions. These yield objects (categories) not morphisms (functors) and an injection morphism function is also provided.

xl-sml

new_const("dom",

);
new_const("cod",

);
new_const("inj",

BOOL)

);

Identity functors are special cases of injections defined as follows:

xl-holconst

╷ id: C

╷

c: C

id c = inj c (

We are now in a position to give the first axioms. First we assert that functors and categories are extensional.

xl-sml

val cat_ext_axiom = new_axiom (["cat_ext_axiom"],

c1 c2:C

(

f:F

_f c1

_f c2)

c1=c2

);
val fun_ext_axiom = new_axiom (["fun_ext_axiom"],

f1 f2:F

dom f1 = dom f2

cod f1 = cod f2

(

g:F

_f dom f1

f1 _a g = f2 _a g)

f1=f2

);

Composition is given as a total function rather than a partial one. The axioms will however speak only about the values of the function in the cases where the partial composition we expect in categories would be defined. That is reflected first in the axiom which asserts that composition is associative.

xl-sml

val comp_assoc_axiom = new_axiom (["comp_assoc_axiom"],

f1 f2 f3:F

cod f1 = dom f2

cod f2 = dom f3

(f1 _o f2) _o f3 = f1 _o (f2 _o f3)

);

Two key properties of categories and functors respectively are now asserted, viz. that categories are closed under composition and functors respect composition.

xl-sml

val cat_comp_axiom = new_axiom (["cat_comp_axiom"],

c: C; f1 f2:F

_f c

cod f1 = dom f2

(f1 _o f2)

_f c

);
val func_comp_axiom = new_axiom (["func_comp_axiom"],

f f1 f2:F

_f (dom f)

cod f1 = dom f2

f _a (f1 _o f2) = (f _a f1) _o (f _a f2)

);

Categories are also closed under left and right identity. First we define membership as a relation between categories.

xl-sml

declare_infix (240, "

_c");

xl-holconst

╷ $

_c: C

BOOL

╷

c1 c2: C

_c c2

(id c1)

_f c2

xl-sml

val cat_id_axiom = new_axiom (["cat_id_axiom"],

c: C; f:F

_f c

(dom f)

_c c

(cod f)

_c c

);

The following axiom tells us that, given a category c and a predicate p over functors which defines a subcategory of c,

inj c p

is a functor which injects that subcategory into c. This is not only an injection in the sense of a one-one function, but also an identity functor.

xl-sml

val injection_axiom = new_axiom (["injection_axiom"],

c: C; p: F

BOOL

(

f g: F

_f c

p f

p g

p (f _o g))

(

f: F

_f c

p f

p (id (dom f))

p (id (cod f)))

(

f: F

_f (dom (inj c p))

p f)

(

f: F

_f (dom (inj c p))

(inj c p) _a f = f)

cod (inj c p) = c

);

The next axiom asserts well-foundedness. It is probably unnecessary for the development of mathematics in this system, but is valuable in giving insight into the underlying model which has inspired the rest of the axioms.

xl-sml

val well_founded_axiom = new_axiom (["well_founded_axiom"],

pc:C

BOOL; pf: F

BOOL

(

c:C

(

f:F

_f c

pf f)

pc c)

(

f:F

(pc (dom f)

pc (cod f))

pf f)

(

c:C

pc c)

(

f:F

pf f)

);

The dependent function space constructor is an operator which takes a category and a function over that category assigning to each morphism in the category a category. The operator yields a new category which contains just two objects. The first object is the original category. The second object is the union of the the image of that category (considered as a set of morphisms) under the function. The arrows in the new category are "dependent functions".

xl-sml

new_const("

_c",

);
new_const("

_c",

);

xl-sml

val beta_axiom = new_axiom (["beta_axiom"],

c:C; lam: F

F; f:F

(

g h:F

_f c

cod g = dom h

cod (lam f) = dom (lam h)

lam (g _o h) = (lam g) _o (lam h))

_f c

(

_c lam c) _a f = lam f

);

xl-sml

val dfs_axiom = new_axiom (["dfs_axiom"],

c:C; l: F

F; L: F

(

f:F

_f c

(l f)

_f (L f))

(

g h:F

_f c

cod g = dom h

cod (l g) = dom (l h)

l (g _o h) = (l g) _o (l h))

(

_c l c)

_f (

_c L c)

);

The following infinity axiom incorporates a union axiom.

xl-sml

val infinity_axiom = new_axiom (["infinity_axiom"],

f: F

c:C

_f c

(

L: F

C; g: F; d: C

d = dom g

(

g:F

_f d

(L g)

_c c)

(

_c L d)

_c c

(

uf:C

_c c

h1 h2:F

_f cod f

_f dom h1

_f uf)

)

);

The empty category is obtainable by separation.

xl-holconst

╷

_c :C

╷

_c = dom(inj (

T) (

F))

xl-tex

<p>
The empty functor is the identity functor over the empty category.
</p>

xl-holconst

╷

_f :F

╷

_f = id

We may as well have the lambdas declared as binders.

xl-sml

declare_binder "

_c";
declare_binder "

_c";

We now prove that the empty category is indeed empty.

xl-sml

set_goal([],

f:F

);
a (strip_tac

THEN rewrite_tac [get_spec

]);
a (strip_asm_tac injection_axiom);
a (LIST_SPEC_NTH_ASM_T 1 [

c:C

f:F

]

(fn x=> strip_asm_tac (rewrite_rule[] x)));
a (asm_rewrite_tac[]);
val empty_cat_thm = save_pop_thm "empty_cat_thm";

The following theorems permit the extensionality axioms to be used as rewrites.

xl-sml

set_goal([],

c1 c2:C

c1=c2

(

f:F

_f c1

_f c2)

);
a (REPEAT_N 4 strip_tac);
(* *** Goal "1" *** *)
a (strip_tac THEN asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (rewrite_tac [cat_ext_axiom]);
val cat_ext_thm = save_pop_thm "cat_ext_thm";

xl-sml

set_goal ([],

f1 f2:F

f1=f2

dom f1 = dom f2

cod f1 = cod f2

(

g:F

_f dom f1

f1 _a g = f2 _a g)

);
a (REPEAT_N 4 strip_tac);
(* *** Goal "1" *** *)
a (strip_tac THEN asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (rewrite_tac [fun_ext_axiom]);
val fun_ext_thm = save_pop_thm "fun_ext_thm";

We now prove that the empty category is an initial object in our domain of categories.

xl-sml

set_goal([],

c:C

₁ f:F

dom f =

cod f = c

);
a (strip_tac THEN

₁_tac

inj c (

);
a (strip_asm_tac injection_axiom);
a (LIST_SPEC_NTH_ASM_T 1 [

f:F

]

(fn x=> strip_asm_tac (rewrite_rule[] x)));
a (REPEAT strip_tac);
(* *** Goal "1" *** *)
a (rewrite_tac [cat_ext_thm]);
a (REPEAT_N 2 strip_tac);
a (asm_rewrite_tac[empty_cat_thm]);
(* *** Goal "2" *** *)
a (once_rewrite_tac [fun_ext_thm]);
a (REPEAT strip_tac THEN_TRY asm_rewrite_tac[]);
(* *** Goal "2.1" *** *)
a (asm_rewrite_tac [cat_ext_thm, empty_cat_thm]);
(* *** Goal "2.2" *** *)
a (swap_nth_asm_concl_tac 1);
a (GET_NTH_ASM_T 3 rewrite_thm_tac);
a (rewrite_tac [empty_cat_thm]);
val empty_cat_initial_thm = save_pop_thm "empty_cat_initial_thm";

Any finite collection of categories can be made into a discrete category.