[[!redirects Categorical Homotopy Type Theory]] < [[nlab:André Joyal#JoyalCategorialHoTT]] category: redirected to nlab