0.0

credits

Average Course Rating

Homotopy type theory (HoTT) is a new proposed foundation system for mathematics that extends Martin-Löf's dependent type theory with Voevodsky's univalence axiom. Dependent type theory is a formal system for constructive mathematics, in which a theorem is proven by constructing a term in the type that encodes its statement. In Homotopy type theory, types are thought of as spaces and terms as points in those spaces. A proof that two terms in a common type are equal is now interpreted as a path between two points in a space. In particular, types might have interesting higher homotopical structure, which can be thought of as revealing fundamental differences between two proofs of a common proposition. One advantage of this foundation system is its amenability to computer formalization, which this course will illustrate by introducing the computer proof assistant Agda.