[[!redirects effective epic function]] [[!redirects effective epimorphism]] [[!redirects effective epic]] < [[nlab:effective epimorphism in homotopy type theory]] category: redirected to nlab