Formalization in Homotopy Type Theory - Equivalences, 3-for-2 and Definitional Equality

Explore a practical technique for proving map equivalence in this 48-minute lecture on formalization in Homotopy Type Theory (HoTT). Delve into the concepts of equivalences, the 3-for-2 property, and definitional equality as presented by Tom de Jong at the Hausdorff Center for Mathematics. Gain insights into advanced mathematical concepts and their applications in formal proofs within the context of HoTT.

Tom de Jong: Formalization in HoTT: equivalences, 3-for-2 and definitional equality