[[!redirects type family]] [[!redirects type families]] [[!redirects Type families]] [[!redirects family]] < [[nlab:dependent type]] category:redirected to nlab