[[!redirects univalent type theory]] < [[nlab:univalent type theory]]