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

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
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
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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 set theory

In set theory, function extensionality states that for all sets AA and BB and functions f:ABf:A \to B and g:ABg:A \to B, if, for all elements xAx \in A, f(x)=g(x)f(x) = g(x), then f=gf = g.

There is another definition of function extensionality: for all sets AA and BB and functions f:ABf:A \to B and g:ABg:A \to B, if, for all elements xAx \in A and yAy \in A such that x=yx = y, f(x)=g(y)f(x) = g(y), then f=gf = g.

In category theory

Since sets and functions form a category, the set theory definition of function extensionality could be generalized to any category with a terminal object. Function extensionality corresponds to the fact that the terminal object is an extremal generator in category, and is one of the conditions for making a pretopos a well-pointed pretopos.

In additon, 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.

In type theory

In intensional type theory, equality is represented by the identity type, and furthermore, there might be more than one element of the identity type in intensional type theory, so a naive translation of function extensionality into intensional type theory doesn’t result in the right statement.

Instead we have the following:

For all types AA and BB and functions f:ABf:A \to B and g:ABg:A \to B, there are two canonical functions which one could use for function extensionality

happly(f,g):(f= ABg) x:Af(x)= Bg(x)\mathrm{happly}(f, g):(f =_{A \to B} g) \to \prod_{x:A} f(x) =_B g(x)

inductively defined by

happly(f,f)(refl AB(f))λ(x:A).refl B(f(x)): x:Af(x)= Bf(x)\mathrm{happly}(f,f)(\mathrm{refl}_{A \to B}(f)) \equiv \lambda (x:A).\mathrm{refl}_B(f(x)):\prod_{x:A} f(x) =_B f(x)


happly(f,g):(f= ABg)( x:A y:A p:x= Ayf(x)= Bg(y))\mathrm{happly}(f, g):(f =_{A \to B} g) \to \left(\prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} f(x) =_B g(y)\right)

inductively defined by

happly(f,f)(refl AB(f))λ(x:A).λ(x:A).λ(refl A(x):x= Ax).refl B(f(x)): x:A x:A refl A(x):x= Axf(x)= Bf(x)\mathrm{happly}(f,f)(\mathrm{refl}_{A \to B}(f)) \equiv \lambda (x:A).\lambda (x:A).\lambda (\mathrm{refl}_A(x):x =_A x).\mathrm{refl}_B(f(x)):\prod_{x:A} \prod_{x:A} \prod_{\mathrm{refl}_A(x):x =_A x} f(x) =_B f(x)

The two definitions of happly\mathrm{happly} become the same under singleton contractibility?. This second definition behaves better with the action on identifications.

In general, both functions happly(f,g)\mathrm{happly}(f, g) are not equivalences of types in intensional type theory: 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).

Function extensionality is then the statement that the function happly(f,g)\mathrm{happly}(f, g) is an equivalence of types for all functions f:ABf:A \to B and g:ABg:A \to B.

funext(f,g):isEquiv(happly(f,g))\mathrm{funext}(f, g):\mathrm{isEquiv}(\mathrm{happly}(f, g))

Definitional function extensionality

One could replace the equivalences of types above with definitional equality of types, which results in definitional function extensionality. Applied to each definition, definitional function extensionality states that for all all types AA and BB and functions f:ABf:A \to B and g:ABg:A \to B

f= ABg x:Af(x)= Bg(x)f =_{A \to B} g \equiv \prod_{x:A} f(x) =_B g(x)


f= ABg x:A y:A p:x= Ayf(x)= Bg(y)f =_{A \to B} g \equiv \prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} f(x) =_B g(y)

respectively. The second version of definitional function extensionality holds in higher observational type theory


Categorical semantics

Translating the type theoretic definition into its categorical semantics, 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.

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

For definitional function extensionality in higher observational type theory, see

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

See also

Last revised on October 20, 2022 at 04:48:36. See the history of this page for a list of all contributions to it.