Explanation of The HoTT Book: Chapter 11 Part I

The following is part one of a summary of Chapter 11 on the construction of the real numbers as a Higher Inductive Type within Homotopy Type Theory.

Updated: