A Theory of Pure Categories
Two new types are introduced in HOL, C and F of pure categories and functors respectively. Axioms are asserted to make these into a foundation for mathematics with strength similar to ZFC + infinitely many inaccessibles. The initial stages of the development of mathematics in this system are presented.
A new "pc" theory is created as a child of "hol".
This is a place holder.
A new "pc" theory is created as a child of "hol".
The Theory pc
The new theory is first created, together with a proof context which we will build up as we develop the theory.
open_theory "hol";
force_new_theory "pc";
force_new_pc "pc";
merge_pcs ["xl_cs_∃_conv"] "pc";
set_merge_pcs ["hol", "pc"];

New Types


Composition and Application

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.

declare_infix (240, "o");
new_const("o",qqco.gifF → F → F⌝);
declare_infix (240, "a");
new_const("a",qqco.gifF → F → F⌝);

We also have a membership relation which asserts that a morphism is a member of a category.
declare_infix (240, "∈f");
new_const("∈f",qqco.gifF → C → 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.
new_const("dom",qqco.gifF → C⌝);
new_const("cod",qqco.gifF → C⌝);
new_const("inj",qqco.gifC → (F → BOOL) → F⌝);

Identity functors are special cases of injections defined as follows:
id: C → F
∀c: C• id c = inj c (λf•T)
We are now in a position to give the first axioms. First we assert that functors and categories are extensional.
val cat_ext_axiom = new_axiom (["cat_ext_axiom"], ⌜
ftbr ∀c1 c2:C• (∀f:F• f ∈f c1 ≡ f ∈f c2) ⇒ c1=c2
val fun_ext_axiom = new_axiom (["fun_ext_axiom"], ⌜
ftbr ∀f1 f2:F• dom f1 = dom f2 ∧ cod f1 = cod f2
fttab∧ (∀g:F• g ∈f dom f1 ⇒ f1 a g = f2 a g)
fttab⇒ 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.
val comp_assoc_axiom = new_axiom (["comp_assoc_axiom"], ⌜
ftbr ∀f1 f2 f3:F• cod f1 = dom f2 ∧ cod f2 = dom f3
fttab⇒ (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.
val cat_comp_axiom = new_axiom (["cat_comp_axiom"], ⌜
ftbr ∀c: C; f1 f2:F• f1 ∈f c ∧ f2 ∈f c ∧ cod f1 = dom f2
fttab⇒ (f1 o f2) ∈f c
val func_comp_axiom = new_axiom (["func_comp_axiom"], ⌜
ftbr ∀f f1 f2:F• f1 ∈f (dom f) ∧ f2 ∈f (dom f) ∧ cod f1 = dom f2
fttab⇒ 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.
declare_infix (240, "∈c");

$∈c: C → C → BOOL
∀c1 c2: C• c1 ∈c c2 ≡ (id c1) ∈f c2

val cat_id_axiom = new_axiom (["cat_id_axiom"], ⌜
ftbr ∀c: C; f:F• f ∈f c
fttab⇒ (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.
val injection_axiom = new_axiom (["injection_axiom"], ⌜
ftbr ∀c: C; p: F → BOOL•
fttab(∀f g: F• f ∈f c ∧ g ∈f c ∧ p f ∧ p g ⇒ p (f o g))
fttab∧ (∀f: F• f ∈f c ∧ p f ⇒ p (id (dom f)) ∧ p (id (cod f)))
fttab⇒ (∀f: F• f ∈f (dom (inj c p)) ≡ p f)
fttab∧ (∀f: F• f ∈f (dom (inj c p)) ⇒ (inj c p) a f = f)
fttab∧ 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.
val well_founded_axiom = new_axiom (["well_founded_axiom"], ⌜
ftbr ∀pc:C → BOOL; pf: F → BOOL•
fttab(∀c:C• (∀f:F• f ∈f c ⇒ pf f) ⇒ pc c)
ftbrfttab(∀f:F• (pc (dom f) ∧ pc (cod f)) ⇒ pf f)
fttab⇒ (∀c:C• pc c) ∧ (∀f:F• pf f)

Dependent Functor Spaces
The "dependent functor space constructor" plays a key role in getting this theory up to a decent level of strength.
The Constructor

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".

new_const("λc",qqco.gif(F → F) → C → F⌝);
new_const("Λc",qqco.gif(F → C) → C → C⌝);

val beta_axiom = new_axiom (["beta_axiom"], ⌜
ftbr ∀c:C; lam: F → F; f:F•
fttab(∀g h:F• g ∈f c ∧ g ∈f c ∧ cod g = dom h
fttabfttab⇒ cod (lam f) = dom (lam h)
fttabfttab∧ lam (g o h) = (lam g) o (lam h))
fttab∧ f ∈f c ⇒ (λc lam c) a f = lam f

val dfs_axiom = new_axiom (["dfs_axiom"], ⌜
ftbr ∀c:C; l: F → F; L: F → C•
fttab(∀f:F• f ∈f c ⇒ (l f) ∈f (L f))
fttab∧ (∀g h:F• g ∈f c ∧ h ∈f c
fttabfttab⇒ cod g = dom h ⇒ cod (l g) = dom (l h)
fttabfttab∧ l (g o h) = (l g) o (l h))
fttab⇒ (λc l c) ∈fc L c)

The following infinity axiom incorporates a union axiom.
val infinity_axiom = new_axiom (["infinity_axiom"], ⌜
ftbr ∀f: F• ∃c:C• f ∈f c
fttab∧ (∀L: F → C; g: F; d: C•
fttabfttabd = dom g
fttabfttab∧ (∀g:F• g ∈f d ⇒ (L g) ∈c c)
fttabfttab⇒ (Λc L d) ∈c c
fttabfttab∧ (∃uf:C• uf ∈c c
fttabfttabfttab∧ ∀h1 h2:F• h1 ∈f cod f
fttabfttabfttab∧ h2 ∈f dom h1
fttabfttabfttab⇒ h2 ∈f uf)

Definitions and Proofs
The Empty Category and Functor

The empty category is obtainable by separation.

c :C
c = dom(inj (εc•T) (λf•F))

The empty functor is the identity functor over the empty category.

f :F
f = id ∅c
We may as well have the lambdas declared as binders.
declare_binder "λc";
declare_binder "Λc";

We now prove that the empty category is indeed empty.
set_goal([], ⌜∀ f:F• ¬f ∈fc⌝);
a (strip_tac
fttabTHEN rewrite_tac [get_spec ⌜∅c⌝]);
a (strip_asm_tac injection_axiom);
a (LIST_SPEC_NTH_ASM_T 1 [⌜ε c:C• T⌝, ⌜λ f:F• F⌝]
fttab(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.
set_goal([], ⌜
ftbr ∀c1 c2:C• c1=c2 ≡ (∀f:F• f ∈f c1 ≡ f ∈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";

set_goal ([], ⌜
ftbr ∀f1 f2:F• f1=f2 ≡ dom f1 = dom f2 ∧ cod f1 = cod f2
fttab∧ (∀g:F• g ∈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.
set_goal([], ⌜∀c:C• ∃1 f:F• dom f = ∅c ∧ cod f = c⌝);
a (strip_tac THEN ∃1_tac ⌜inj c (λf•F)⌝);
a (strip_asm_tac injection_axiom);
a (LIST_SPEC_NTH_ASM_T 1 [⌜c⌝, ⌜λ f:F• F⌝]
fttab(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";

Finite Discrete Categories

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

Proof Context
This is a place holder.
Proof Context

up quick index © RBJ

privacy policy


$Id: pure_categories.xml,v 1.3 2008/04/15 18:21:36 rbj01 Exp $