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",F → F → F⌝); declare_infix (240, "a"); new_const("a",F → F → F⌝);

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",F → 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.

xl-sml new_const("dom",F → C⌝); new_const("cod",F → C⌝); new_const("inj",C → (F → BOOL) → F⌝);

Identity functors are special cases of injections defined as follows:

xl-holconst 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.

xl-sml val cat_ext_axiom = new_axiom (["cat_ext_axiom"], ⌜ ∀c1 c2:C• (∀f:F• f ∈f c1 ≡ f ∈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• g ∈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• f1 ∈f c ∧ f2 ∈f c ∧ cod f1 = dom f2 ⇒ (f1 o f2) ∈f c ⌝); val func_comp_axiom = new_axiom (["func_comp_axiom"], ⌜ ∀f f1 f2:F• f1 ∈f (dom f) ∧ f2 ∈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 → C → BOOL

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

xl-sml val cat_id_axiom = new_axiom (["cat_id_axiom"], ⌜ ∀c: C; f: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 ∈f c ∧ g ∈f c ∧ p f ∧ p g ⇒ p (f o g)) ∧ (∀f: F• f ∈f c ∧ p f ⇒ p (id (dom f)) ∧ p (id (cod f))) ⇒ (∀f: F• f ∈f (dom (inj c p)) ≡ p f) ∧ (∀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 ∈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",(F → F) → C → F⌝); new_const("Λc",(F → C) → C → C⌝);

xl-sml val beta_axiom = new_axiom (["beta_axiom"], ⌜ ∀c:C; lam: F → F; f:F• (∀g h:F• g ∈f c ∧ g ∈f c ∧ cod g = dom h ⇒ cod (lam f) = dom (lam h) ∧ lam (g o h) = (lam g) o (lam h)) ∧ f ∈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 → C• (∀f:F• f ∈f c ⇒ (l f) ∈f (L f)) ∧ (∀g h:F• g ∈f c ∧ h ∈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 ∈f c ∧ (∀L: F → C; g: F; d: C• d = dom g ∧ (∀g:F• g ∈f d ⇒ (L g) ∈c c) ⇒ (Λc L d) ∈c c ∧ (∃uf:C• uf ∈c c ∧ ∀h1 h2:F• h1 ∈f cod f ∧ h2 ∈f dom h1 ⇒ h2 ∈f uf) ) ⌝);

The empty category is obtainable by separation.

xl-holconst ∅c :C

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

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

xl-holconst ∅f :F

∅f = id ∅c

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• ¬f ∈f ∅c⌝); a (strip_tac THEN rewrite_tac [get_spec ⌜∅c⌝]); a (strip_asm_tac injection_axiom); a (LIST_SPEC_NTH_ASM_T 1 [⌜ε c:C• T⌝, ⌜λ f: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 ∈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";

xl-sml set_goal ([], ⌜ ∀f1 f2:F• f1=f2 ≡ dom f1 = dom f2 ∧ cod f1 = cod f2 ∧ (∀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.

xl-sml 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⌝] (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.