4 ms·

Categories: An implementation of category theory in Coq

68 points by guifortaine 11y ago

jrcii 11y ago
I suppose it makes me immature but whenever I hear anything about this language I'm distracted by the name.
WaxProlix 11y ago
If I want to investigate this project, where should I start? (after configure/make)
- dkural 11y 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 11y 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 11y ago
  MacLane was too heavy for me, but I can wholeheartedly recommend lectures from Steve Awodey: https://www.youtube.com/watch?v=BF6kHD1DAeU https://www.youtube.com/watch?v=BF6kHD1DAeU
starseeker 11y 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/msg00009.html https://lists.gnu.org/archive/html/axiom-developer/2015-07/m...
mafribe 11y 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-category-theory-in-proof-assistants https://mathoverflow.net/questions/152497/formalizations-of-...

68 points by guifortaine 11y ago

jrcii 11y ago

I suppose it makes me immature but whenever I hear anything about this language I'm distracted by the name.

WaxProlix 11y ago

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

dkural 11y 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 11y 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 11y ago
MacLane was too heavy for me, but I can wholeheartedly recommend lectures from Steve Awodey: https://www.youtube.com/watch?v=BF6kHD1DAeU https://www.youtube.com/watch?v=BF6kHD1DAeU

starseeker 11y 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/msg00009.html https://lists.gnu.org/archive/html/axiom-developer/2015-07/m...

mafribe 11y 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-category-theory-in-proof-assistants https://mathoverflow.net/questions/152497/formalizations-of-...