Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Equational description of categories

  1. Aug 23, 2010 #1
    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?
  2. jcsd
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook

Can you offer guidance or do you also need help?
Draft saved Draft deleted