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