I was planning to learn category theory with coq's aid and its category theory implementation, but a stackoverflow user told me in the comments (of other question) that it may be too difficult. So, following his suggestion, I'm asking if there is a better alternative and which would be the best.

  • 1
    $\begingroup$ You don't need any kind of computer program to study category theory... $\endgroup$ Nov 29 '16 at 11:24
  • 3
    $\begingroup$ Seconding @NajibIdrissi: if you start using a theorem prover, you'll most likely get swamped in questions about the right notion of equality and you won't go very far. However you can implement constructions without doing the proofs. For that any typed functional language ought to do although it'll probably be easier if they have good support for higher-kinded types (so: Haskell, Coq, Agda, Idris in no particular order). $\endgroup$
    – gallais
    Nov 29 '16 at 12:49
  • $\begingroup$ @gallais have you heard of lambda prolog? It's my understanding that even between higher-kinded types there are some "higher" than others... Could lambda prolog be a good choice? $\endgroup$ Dec 1 '16 at 6:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.