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.
xlsml
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.
xlsml
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.
Identity functors are special cases of injections defined as follows:
xlholconst 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.
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.
xlsml
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.
Categories are also closed under left and right identity.
First we define membership as a relation between categories.
xlsml
declare_infix (240, "∈_{c}");

xlholconst $∈_{c}: C → C → BOOL

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

xlsml
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 oneone function, but also an identity functor.
The next axiom asserts wellfoundedness.
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.