An Introduction to Homotopy Type Theory Seminar

Homotopy type theory (HoTT) is a new theory of the foundations of mathematics that brings together the seemingly disparate worlds of logic and homotopy theory. HoTT allows us to treat isomorphic objects as being actually equal, something we do day-to-day anyway, without worrying about set-theoretic difficulties.
The HoTT program is not just theoretical; by replacing sets with types we can implement a computer-checkable proof that the fundamental group of a circle is the integers!

I am not an expert on the subject, I will mainly be aiming to share with the audience some of the ideas involved in this new area. In particular I won't be going into any technical details.