[TYPES] Book on Category Theory

[Burak Emir]

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" <aaronngray.lists at gmail.com> 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 <leo at halfaya.org> 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 <moez at cs.rice.edu>
> 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 <aaronngray.lists at gmail.com>
>> Date: 18/10/2017  21:22  (GMT+02:00)
>> To: The TYPES forum <types-list at lists.seas.upenn.edu>
>> 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.