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