This may be a simple minded question. First, background: Coming from a linguistic and computer science background, I keep on getting Category Theory shoved, ah, shown to me, when studying both algebraic topology and also group theory, specifically, I was reading Lee Lady's papers and meta-papers on finite rank torsion-free abelian groups. (I've even seen it used in proofs in metric spaces, if I remember correctly.) Category Theory was very similar to Type Theory, which is used in CS. (It's obvious to me that they are equivalent. One is based on sets the other on types. Category Theory is just a stripped down version of Type Theory or so it seems to me.)

Programming Language theory uses Type Theory as well as Denotational, Operational and Axiomatic Semantics. (I've done some work with Denotational Semantics and Hoare Logic in computer science awhile back as well as Montague Semantics, modal logic and possible worlds semantics in linguistics, also awhile back.)

Now for the question: It seems to me that Category Theory is akin to a meta-grammar, or really a hyper-grammar, in Programming Languages (theory). Meta-grammars are usually combined with a semantics. But instead of generating an algebra, or rather a language, what CT does is allows one to compare algebras at an abstract level and show equivalence between isomorphic things (Categories). Does this sound right? But if I can generate both algebras using the same meta-grammar it should be equivalent to comparing them using CT, right? That is, my meta-grammar would generate a grammar, Turing complete, that would generate the algebra. I also wonder if I could apply graph rules and operations to Category Theory.

Could someone also recommend a great book, and by great I mean clear well written, on Category Theory. I already have Samson Abramsky and Nikos Tzevelekos's book, Introduction to Categories and Categorical Logic. Any other good books on Category Logic? Or Category Semantics for Linear Logic? Thanks.

  • 1
    $\begingroup$ No, category theory is not a special case of type theory, nor vice versa. If you think they are then you have not seen enough examples. Since you mention algebraic topology, perhaps you know some mathematics, in which case you should read the classic Categories for the working mathematician. $\endgroup$ – Zhen Lin Oct 11 '15 at 7:33
  • $\begingroup$ OK. I will. I was under the impression that Category theory was similar to Type theory without a lot of the syntactic constraints. I am familiar with Type theory, basically formal languages, and I could see the similarities. But perhaps I have not had enough examples. I've only seen few examples used in topology and a couple of examples in group theory. Thanks. I'll look that up. $\endgroup$ – Mark LaPolla Oct 11 '15 at 15:21

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.