Types were invented by Bertrand Russell in the early 20th century as a way to resolve his paradox. Type theory was further developed in relation to the lambda calculus, computer science and constructive mathematics. Recently, it was noticed that the correspondence between propositions and types can be extended to include notions from homotopy theory, forming the beginning of homotopy type theory.

One aspect of homotopy type theory is as a theory of homotopy where the points and paths are primitive objects (as opposed to continuous maps from intervals, etc.). Another aspect of it is in motivating developments in type theory. Connected to this is the use of the type theory developed as a foundation of mathematics, that is more suitable for formalizing mathematics with proof assistants than set theory.

I will present a version of Martin-Löf's intensional intuitionistic type theory, and connect it to homotopy theory. If there is time, I will calculate the homotopy groups of the circle.