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 - The Fusion of Science and Community**

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

Loading...

Similar Threads - Equational description categories | Date |
---|---|

I What does the vertical line in this equation mean? | Feb 28, 2018 |

I Empirical equation from two variables (1 input and 1 output) | Feb 19, 2018 |

I Equation with two unknowns (old title: Einstein's Insanity) | Feb 9, 2018 |

I Comparing two absolute value equations | Feb 4, 2018 |

Is this a fair description of mathematics (in one sentence)? | Mar 14, 2016 |

**Physics Forums - The Fusion of Science and Community**