Univalence without function extensionality

TL;DR

The paper explores a weaker form of univalence called categorical univalence, demonstrating it does not imply function extensionality through model analysis.

Contribution

It introduces categorical univalence and shows it does not entail function extensionality using polynomial model constructions.

Findings

Categorical univalence does not imply function extensionality.

Polynomial models can have univalent universes without function extensionality.

Models with univalent universes can lack function extensionality.

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\"of 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.