# Are there semi-decision procedures for this theory?

I have the following typed theory

|- 1_X : X -> X
f : A -> B, g : B -> C |- compose(g,f) : A -> C
F, f : A -> B |- apply(F,f) : F(A) -> F(B)


with equations for all terms:

f : A -> B, g : B -> C, h : C -> D |- compose(h,compose(f,g)) = compose(compose(h,f),g)
f : A -> B |- compose(f,1_A) = f
f : A -> B |- compose(1_B,f) = f
F |- apply(F,1_X) = 1_F(X)
f, f : A -> B, g : B -> C |- apply(F,compose(g,f)) = compose(apply(F,g),apply(F,f))


I am looking for a semi-decision procedure that will be able to prove equations in this theory given a set of hypothetical equations. It is also not clear whether a complete decision procedure exists or not: There doesn't seem to be any way to encode the word problem for groups into it. Neel Krishnaswami showed how to encode the word problem into this, so the general problem is undecidable. The associativity and identity subtheory can easily be decided using a monoid model of the theory, while the full problem is harder than congruence closure. Any references or pointers would be most welcome!

Here is an explicit example of something we would hope to be able to automatically proved:

f : X -> Y, F, G,
a : F(X) -> G(X), b : G(X) -> F(X),
c : F(Y) -> G(Y), d : G(Y) -> F(Y),
compose(a,b) = 1_F(X), compose(b,a) = 1_G(X),
compose(c,d) = 1_F(Y), compose(d,c) = 1_G(Y),
compose(c,apply(F,f)) = compose(apply(G,f),a)
|- compose(d,apply(G,f)) = compose(apply(F,f),b)


It looks to me that you can encode the word problem for groups within the theory of categories in the following way. Pick an object $X$, and then for each generator of the group introduce two morphisms $x,x' : X \to X$, and assume the equalities $x \circ x' = 1_X$ and $x' \circ x = 1_X$. Then you can define the unit to be the identity map, the composition to be the group multiplication, and the negation of a string $x\circ y\circ z$ to be the reverse primed string $z' \circ y' \circ x'$. Hence this problem is undecidable.