Greetings PF,(adsbygoogle = window.adsbygoogle || []).push({});

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?

**Physics Forums | Science Articles, Homework Help, Discussion**

Join Physics Forums Today!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

# Equational description of categories

Can you offer guidance or do you also need help?

Draft saved
Draft deleted

**Physics Forums | Science Articles, Homework Help, Discussion**