[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hey there. I also prefer Steve Awodey's "Category Theory" to many of the other references. Contravariant functors happen to be mentioned there as well (p. 107 in 2nd edition - just a functor from C^op -> D : ) ), and it has an example how slice categories relate to indexed families, if dependent types is what you are pursuing. I believe the catamorphism jargon for the arrow from an initial algebra was introduced in Meijer, Fokkinga, Paterson's "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire". Certainly, knowing the categorical treatment of algebras (described succinctly in Pierce's book) will help with the understanding of that paper - and many others. Popular as that jargon seems to be, I believe it is unlikely to come across those terms in category theory books (but I might be wrong). Crole's "Categories for Types" looks like a valuable reference, the way it draws an arc from algebraic type theory over simply typed lambda calculus to system F and F-omega. It does not seem to make as good an introduction though. When looking for another, inspiring introduction that connects category theory and type theory, Lambek and Scott's "Introduction to Higher-Order Categorical Logic" is still an outstanding book, though note the "higher order" refers to lambdas in the same way simply typed lambda calculus was called higher order logic by Church. If you want to take a break from the categories : ) and consider approaching the topic via logic, another reference treating type theory as in "higher order logic" is Andrews "To truth through proof". It focuses on classical logic. To close the circle, for categorical models of dependent types, there are also plenty of references on https://ncatlab.org/nlab/show/categorical+model+of+dependent+types sincerely hope this helps! Burak On Oct 23, 2017 9:48 PM, "Aaron Gray" <[email protected]> wrote: [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Thanks everyone, but as far as I can tell none of these books give me any real stuff on covariance, contravariance, anamophisms and catamophisms. On 19 October 2017 at 16:59, John Leo <[email protected]> wrote: > I agree Pierce's book is great, and my favorite overall reference Awodey > also has some material on applications to type theory. > > For specific connections, the best sources are probably lecture notes for > various summer school courses. My three favorites are those in the > "Category Theory and Functional Programming" section of this page: > https://github.com/halfaya/BayHac/blob/master/references.md > > John > > > > On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad <[email protected]> > wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> ilman/listinfo/types-list ] >> >> In addition to Pierce's book, which was earlier mentioned, I strongly >> recommend Spivak's Category Theory for The Sciences and Lawvere & >> Schanuel's Conceptual Mathematics. Even though neither book is specifically >> for computer scientists, but both books are more modern, very accessible, >> and frequently discuss CS applications. >> >> -Moez >> >> -------- Original message -------- >> From: Aaron Gray <[email protected]> >> Date: 18/10/2017 21:22 (GMT+02:00) >> To: The TYPES forum <[email protected]> >> Subject: [TYPES] Book on Category Theory >> >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> ilman/listinfo/types-list ] >> >> I am looking for a book on Category Theory that is ideally either aimed at >> Type Theory or has the relevant topics to support the area. >> >> I have bought three books on the topic so far, one 'Categories for Typesw' >> by Crole did not even cover covariance and contravariance.I would also >> like >> coverage of monoid and monads, and morphisms like anamorphisms and >> catamorphisms. >> >> I am also interested in papers applying category theory to areas of type >> theory. >> >> Suggestions of either online or printed material would be appreciated. >> >> Many tahnks in advance, >> -- >> Aaron Gray >> >> Independent Open Source Software Engineer, Computer Language Researcher, >> Information Theorist, and amateur computer scientist. >> > > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist.
