[[!redirects Eric Finster, Towards Higher Universal Algebra in Type Theory]] < [[nlab:Towards Higher Universal Algebra in Type Theory]] category: redirected to nlab