An Introduction to Intuitionistic Type Theory
New York Haskell Users Group
Homotopy type theory is a new foundation for mathematics based upon type theory and the univalence axiom. This is a topic that unifies the foundations of mathematics, computer science, algebraic topology, and type theory.
This will be the first focused reading of the Homotopy type theory reading group, covering sections 1.1-1.7 of the book. This will serve as an introduction to Intuitionistic Type Theory as developed by Martin-Löf, including notions of decidability and judgmental equality, up through dependent function and pair types (aka Pi and Sigma).
The reading group includes those with type theory background and no homotopy background, with homotopy background but no type theory background, and with no significant background in either but a healthy thirst for knowledge.
Gershom Bazerman studied Computer Science at UC Berkeley. He is an
organizer of the New York Haskell Users Group. His interests are
scattered in the general direction of programming languages and