Univalence without function extensionality
This clarifies the logical relationship between univalence and function extensionality for researchers in homotopy type theory.
The paper shows that a weaker form of univalence, called categorical univalence, does not imply function extensionality, by constructing a model of type theory where categorical univalence holds but function extensionality fails.
It is a well-known theorem of homotopy type theory, originally due to Voevodsky, that function extensionality holds inside any univalent universe. We consider a weaker variant of the univalence axiom, asserting that the wild category formed by the universe is univalent, which we call categorical univalence. We show that categorical univalence does not imply function extensionality by an analysis of Von Glehn's polynomial model construction, which produces models of Martin-Löf type theory that always refute function extensionality. We find in particular that when the base model has a univalent universe, its polynomial model has a universe that is categorically univalent but lacks function extensionality.