[[!redirects ETCS as a dependent type theory]] < [[nlab:ETCS]] category: redirected to nlab