Re:Categories: An implementation of category theory in Coq
by WaxProlix on Monday April 11, 2016 @09:33PM
(#11476588)
If I want to investigate this project, where should I start? (after configure/make)
[ Parent
| on HN ]
Re:Categories: An implementation of category theory in Coq
by dkural on Monday April 11, 2016 @10:04PM
(#11476697)
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.
Re:Categories: An implementation of category theory in Coq
by delish on Monday April 11, 2016 @10:40PM
(#11476843)
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.
Re:Categories: An implementation of category theory in Coq
by js8 on Tuesday April 12, 2016 @05:00AM
(#11478099)
MacLane was too heavy for me, but I can wholeheartedly recommend lectures from Steve Awodey: https://www.youtube.com/watch?v=BF6kHD1DAeU