Categories: An implementation of category theory in Coq

https://github.com/amintimany/Categories

by guifortaine • 10 years ago

68 6 10 years ago

WaxProlix• 10 years ago

If I want to investigate this project, where should I start? (after configure/make)

dkural• 10 years ago

Saunders MacLane: Category Theory for the Working Mathematician - most of the concepts implemented in this package are introduced there. I tend to dislike the "Category Theory for ___" type books, too much verbiage and misleading metaphors/analogies in many of them.

delish• 10 years ago

To my fellow self-taught mathematicians and computer scientists:

When I was starting out, I'd learn from what was too-dense-for-me (Mac Lane, Awodey, Spivak). When I didn't understand, I'd get frustrated, then go learn something else.

There are two differences between me-then, and me-now. First, I spend a lot more time choosing books to read. I find books that meet me where I am. I need all the help I can get. Second, when I don't understand, I skip being frustrated, and go learn something else.

I agree though with dkurai when it comes to math I'm already familiar with. If I'm reading what I already know, it's usually foundational to something I'm about to learn. Then, I need rigor and concision, to avoid being misled.

js8• 10 years ago

MacLane was too heavy for me, but I can wholeheartedly recommend lectures from Steve Awodey: https://www.youtube.com/watch?v=BF6kHD1DAeU

starseeker• 10 years ago

What's the license on this project? I'm wondering if it might fit in well with some work Tim Daly has started on the Axiom project hooking up computer algebra to coq et. al.:

https://lists.gnu.org/archive/html/axiom-developer/2015-07/m...

mafribe• 10 years ago

There are quite a few formalisations of category theory for proof assistants. For a relatively recent overview, see:

https://mathoverflow.net/questions/152497/formalizations-of-...

Categories: An implementation of category theory in Coq

Related Stories