[[!redirects type theory over logic]] < [[nlab:predicate logic as a dependent type theory]] category: redirected to nlab