[[!redirects Book HoTT]] < [[nlab:book homotopy type theory]]