Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory

While languages such as Haskell and ML are based on the simply typed lambda calculus, others, such as Agda and Epigram, go one step further by using dependent types. Especially with regard to the Curry-Howard correspondence, this might be desirable as dependent pair types and dependent function types are the equivalent of existential and universal quantification. Hence dependently typed languages are used in proof assistants such as Coq or Agda. Several questions about equality arise here.
Clearly, equality in general cannot be decidable in a reasonable rich system. We therefore need equality proofs, which are just terms of the corresponding equality type. A good question here is to ask for the number of such proofs for an equality statement. Conventionally, it was assumed that there is at most one ("Uniqueness of Identity Proofs"). Recently, Fields Medal winner Vladimir Voevodsky suggested to give up this principle, thereby revealing a connection between logic and topology (more precisely type theory and homotopy theory). This may lead to a new foundation of formal reasoning where equivalent structures can be identified.