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