preface.tex

\chapter{Preface}

These notes were written partly as a supplement to part of a course on higher categories and categorical logic at the AARMS Summer School 2016; but also with a goal of clarify and setting down some ideas that had only recently begun coalescing in my own head.
They are currently somewhat rough, with promised sections or chapters missing and others in an imperfectly consistent state; no guarantee of correctness is provided.
Nevertheless I have some hope they may be useful to the category theorist who needs some help, as I did, to figure out what this ``type theory'' is all about.

In my own case, whatever correct understanding I have come to (and attempted to share in this book) is due largely to the generous help and explanations provided by others, particularly Dan Licata and Peter LeFanu Lumsdaine, but also (in no particular order) Todd Trimble, Toby Bartels, Steve Awodey, Bob Harper, Vladimir Voevodsky, Thorsten Altenkirch, Mart\'in Escard\'o, Andrej Bauer, and many others all of whom it would be impossible to list.
Of course, all the errors are my own.

I am also very grateful to Dorette Pronk and the other organizers of the 2016 AARMS Summer School for the invitation to co-teach a course on categorical logic; and to Peter Lumsdaine for teaching the other half of the course and helping with the planning of my half.
Finally, I would like to thank all the students in that course for the lively classroom discussion; frequently their questions made me realize that something was unclear or missing from the notes.


% Local Variables:
% TeX-master: "catlog"
% End: