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