A relatively recent extension to type theory is “homotopy type theory”. This provides a new view on types, where a type A is interpreted as a topological space, a term t of type A is interpreted as a point in the space and a proof of an equality, p : q=t is interpreted as a path from q to t in the space A. This gives rise to new type theoretic principles (like “Univalence”) and new type formers (like “Higher Inductive Types”). This allows to adequately formalize various concepts from algebraic topology, but it is also relevant for computer science.

In the talk I will present some applications of homotopy type theory in computer science, especially how to use Higher Inductive Types to write programs for “data types with laws”, like the type of finite sets.