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.

In this first talk I will introduce the basic notions of type theory with an emphasis on how these axioms endow types with higher dimensional structure and generalize classical set theory.