Greetings PF, I am would like to play with using an automated theorem prover to reason about categories. I would like to be able to type the axioms of category theory into an equational theorem prover (such as E). However, I am looking for a nice way to translate the theory of categories into a theorem prover language. For example, we often state the composition of homsets as a partial semigroup without needing to refer to objects at all. defined(s(f),f) , s(f) f = f defined(f,(t(f)) , f t(f) = f defined(fg) iff t(f) = s(g) , s(fg) = s(f) , t(fg) = t(g) if defined(f,g),defined(g,h),defined((fg),h),defined(f,(gh)) then (fg)h = f(gh) s(t(f)) = t(f) s(s(f)) = s(f) t(t(f)) = t(f) t(s(f)) = s(f) However the above feels huge. Any suggestions?