[[!redirects HoTT Mini-Course]] < [[nlab:HoTT Mini-Course]] category: redirected to nlab