univalence

Univalence is a term used in mathematics with more than one meaning. In complex analysis, a univalent function is a holomorphic function that is injective on its domain. In the setting of modern foundations of mathematics, the Univalence Axiom in Homotopy Type Theory posits that equivalent types can be identified.

In complex analysis, a function f defined on a domain D is univalent if it is injective there. Univalent functions are central to geometric function theory and conformal mapping, since holomorphy plus injectivity implies conformality. A function is locally univalent when its derivative is nonzero everywhere, which for holomorphic functions also gives local injectivity. Global univalence requires a one-to-one correspondence on the entire domain. The unit disk and the class S of normalized univalent functions (f(0)=0, f'(0)=1) are classical objects of study, with results such as distortion theorems and the Koebe quarter theorem guiding their behavior. Examples include the identity map, which is univalent, while z ↦ z^2 is not univalent on any domain containing both z and −z, and the exponential map e^z is not univalent on the complex plane (though it can be univalent on certain strips).

In Homotopy Type Theory, the Univalence Axiom, introduced by Vladimir Voevodsky, states that for types A and B in a universe, the canonical map from the identity type (A = B) to the type of equivalences (A ≃ B) is itself an equivalence. Put differently, equivalent types can be identified. This principle implies function extensionality and supports reasoning about mathematical structures up to equivalence within a formal system.

See also: conformal mapping, schlicht functions, Koebe theorems, homotopy type theory, univalent foundations.