[[!redirects algebraic formulation of dependent type theory]] < [[nlab:dependent type theory]] category: redirected to nlab