Homotopy type theory is an alternative foundational system for mathematics built to more naturally describe mathematical objects exhibiting ``higher dimensional structure'' or relating to each other via weaker notions of equivalence than identity or isomorphism. These sorts of rich structures have been studied for decades by mathematicians including homotopy theorists and algebraic geometers, but using complicated techniques that suggest set theoretic and topological foundations are not ideal for expressing and reasoning about such concepts.
In homotopy type theory the fundamental objects are types, which seamlessly play the role of both spaces and logical propositions. The axioms of these types encode both homotopical and logical structure, allowing them to serve as both theory and metatheory in interesting ways. For instance, given two types A and B, there is a type which can be regarded as containing either homotopy equivalences between A and B or proofs that A and B are homotopy equivalent.
Following on last week's talk, I will review the higher dimensional structure arising from the axioms for identity types, discuss propositional equality in the various types defined previously building up to the univalence axiom, and give new examples of types that use this higher dimensional structure to model spaces, sets, and classical logic.