nLab function extensionality



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts


Category theory

Discrete and concrete objects



The principle of functional extensionality states that two functions are equal if their values are equal at every argument.


In type theory

In intensional (Martin-Löf) dependent type theory the existence of identity types induces a notion on paths between terms of a given type.

In particular for two terms f,g[X,Y]f, g \in [X,Y]

f g: X -> Y

of function type, a path/morphism fpgf \stackrel{p}{\to} g

p: f == g

between them is to be thought of as a homotopy or natural transformation (a 11-transfor). In particular it implies, one can prove, that there are families of paths happly f,g,phapply_{f,g,p} between all the values of the functions

happly f g p: forall x: X, f x == g x .

However, from general intensional dependent type theory one cannot prove the converse:

  • the existence of paths between all pairs of values does not imply that there is a path between the functions.

From a purely intensional point of view, this is to be expected — two functions could be defined in different ways, and thus be intensionally different, yet produce the same values on all inputs (i.e. be extensionally the same).

However, in many contexts one wants to treat functions extensionally, such as when regarding type theory as the internal language of some category. In particular, this is the case in homotopy type theory, where one wants to interpret the type theory as the internal language of an (∞,1)-topos, for instance of Top \simeq ∞Grpd.

In such an internal logic context, a family of anything must always mean “continuous family”, so that a family of paths between the values of two functions is a continuous homotopy between them, and hence ought to induce a path between them in the function-space. Thus, one wants to impose the condition that from a term

eta: forall x: X, f x == g x .

we can deduce an actual path between ff and gg.

Translating this into direct categorical terms, the term η\eta gives a map

1Π X1[fx=gx]1 \to \Pi_{X \to 1} [f x = g x]

into the dependent product, which (as discussed there), in turn corresponds to a section σ:X[fx=gx]\sigma \colon X \to [f x = g x] of the display map on the left side of the pullback

[fx=gx] P(Y) X f,g Y×Y,\array{ [f x = g x] & \to & P(Y) \\ \downarrow & & \downarrow \\ X & \underset{\langle f, g \rangle}{\to} & Y \times Y } \,,

where P(Y)P(Y) is the identity type or space of paths in YY. Such a section is tantamount to a lift XP(Y)X \to P(Y) of f,g:XY×Y\langle f, g \rangle \colon X \to Y \times Y. From this we would like to deduce an actual path p:1P(Y X)p \colon 1 \to P(Y^X).

So, very simply, function extensionality means we are able to lift elements h:1P(Y) Xh \colon 1 \to P(Y)^X through a canonical map ϕ:P(Y X)P(Y) X\phi \colon P(Y^X) \to P(Y)^X that is obtained from a dependent eliminator?.

Of course we are not just interested in global elements here. What we really want is an actual section P(Y) XP(Y X)P(Y)^X \to P(Y^X) of ϕ\phi in the slice over (Y×Y) X(Y \times Y)^X (although this can be derived from the global element formulation by using the Yoneda lemma together with currying and uncurrying tricks). This condition may be called “naive” or “weak” function extensionality, in view of an apparently stronger condition that this section (and therefore also ϕ\phi) be equivalences. This latter condition might be called “strong function extensionality”.

Under reasonable assumptions on the type theory, it turns out that these and other versions of function extensionality are equivalent; for now see (Lumsdaine) below. In any case, if the type theory has an extra axiom that implies some such version, one says that function extensionality holds.

In category theory

Function extensionality in category theory is true in any concrete category 𝒞\mathcal{C}. The axiom could be called “morphism extensionality”; however, in all concrete categories, the morphisms are functions between sets.


Homotopy categorical semantics


Function extensionality holds in the internal type theory of a type-theoretic fibration category precisely if dependent products (i.e. right base change) along fibrations preserve acyclic fibrations.

(Shulman 12, lemma 5.9)


The condition in prop. holds in particular in right proper Cisinski model structures, since in these right base change along fibrations is a right Quillen functor (see e.g. the proof here).

Notice that every presentable locally Cartesian closed (∞,1)-category (by the discussion there) has a presentation by a right proper Cisinski model category. Accordingly we may say that every presentable locally Cartesian closed (∞,1)-category interprets HoTT+FunExt.

Relation to interval types

An interval type in homotopy type theory (with definitional computation rule for the endpoints) implies function extensionality; see this blog post

Relation to the univalence axiom

The univalence axiom implies function extensionality (this is due to Vladimir Voevodsky). See for instance (Bauer-Lumsdaine).

See also


An introduction to the relevant notions and a guided walk through the formal proof that univalence implies functional extensionality is at

A discussion of various flavors of function extensionality, and how to move between them, can be found in

Discussion of the categorical semantics in the context of homotopy type theory is in

See also

Last revised on June 9, 2022 at 16:32:09. See the history of this page for a list of all contributions to it.