Definition of a group object + two lemmas

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work

BSD 3-Clause "New" or "Revised" License

745 stars 68 forks source link

Definition of a group object + two lemmas #7

Closed timjb closed 6 years ago

timjb commented 6 years ago

I wrote this mainly to get back into proving things with Coq. If you're interested, I will try to clean this up a bit.

jwiegley commented 6 years ago

I like it! So yes, I'm interested. :)

timjb commented 6 years ago

I've moved the lemmas to a separate file (so someone only using the definition does not have to wait for the proofs to check), and added some comments to help someone trying to understand the proofs.