Univalence without function extensionality
2026-05-01 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study a weaker version of the univalence principle called categorical univalence, which applies to the universe seen as a category. They show that this weaker version does not guarantee function extensionality, a property important in type theory. By analyzing a certain polynomial model based on previous work, they demonstrate that even if a universe is categorically univalent, it can still fail to have function extensionality. This clarifies subtle differences between these related concepts in homotopy type theory.
homotopy type theoryunivalent universefunction extensionalitycategorical univalenceMartin-Löf type theorypolynomial modelVoevodskyunivalence axiomtype theory models
Authors
Evan Cavallo, Jonas Höfer
Abstract
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.