      Computation and Reasoning - This
book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types. |
Type Theory and Category Theory
| Categorical Logic and Type Theory - This
book is about logic, type theory and category theory. It assumes the reader is familiar with category theory concepts such as adjunctions, limits and CCCs. |
| Categories for Types - The book has some introductory material including a chapter about category theory (although it would be a steep learning curve with no other sources). Then the book shows how to represent category theory in type theory. |