nLab function extensionality

Contents

Context

Set theory

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
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity 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 set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
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

semantics

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

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

Category theory

Discrete and concrete objects

Contents

Idea

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

Definition

In set theory

In set theory, in the same way that the axiom of choice has internal and external versions, depending on whether one uses the external logic? or the internal logic of the set theory, function extensionality also has internal and external versions.

External function extensionality

In set theory, let 𝟙\mathbb{1} denote the unique singleton up to bijection. There are multiple notions of external function extensionality, due to the different possible notions of function and element in set theory:

  • for all sets AA and BB and functions f:ABf:A \to B and g:ABg:A \to B, f=gf = g if and only if for all elements xAx \in A, f(x)=g(x)f(x) = g(x).

  • for all sets AA and BB and functions f:ABf:A \to B and g:ABg:A \to B, f=gf = g if and only if for all functions x:𝟙Ax:\mathbb{1} \to A, fx=gxf \circ x = g \circ x.

  • for all sets AA and BB and elements of the function set fB Af \in B^A and gB Ag \in B^A, f=gf = g if and only if for all elements xAx \in A, ev A,B(f,x)=ev A,B(g,x)\mathrm{ev}_{A, B}(f, x) = \mathrm{ev}_{A, B}(g, x).

  • for all sets AA and BB and elements of the function set fB Af \in B^A and gB Ag \in B^A, f=gf = g if and only if for all elements of the function set xA 𝟙x \in A^\mathbb{1}, comp 𝟙,A,B(f,x)=comp 𝟙,A,B(g,x)\mathrm{comp}_{\mathbb{1}, A, B}(f, x) = \mathrm{comp}_{\mathbb{1}, A, B}(g, x).

The first is the one most commonly found in foundations of categorical set theories with separate notions of element and function. The second is the one most commonly found in foundations of categorical set theories where an element is defined as a function out of the terminal set 𝟙\mathbb{1}.

The first and the third notions of function extensionality are equivalent to each other, since for every set theory with function sets, the category of sets is a cartesian closed category, which means that there is a bijection between the hom-sets

Hom(X,Y)Hom(1,Y X)\mathrm{Hom}(X, Y) \cong \mathrm{Hom}(1, Y^X)

and thus for every function f:XYf:X \to Y there is a unique element of a function set [f]Y X[f] \in Y^X, and for every element of a function set gY Xg \in Y^X there is a unique function g:XYg':X \to Y.

Internal function extensionality

In set theory, let 𝟙\mathbb{1} denote the unique singleton up to bijection and let xAB x\prod_{x \in A} B_x denote the Cartesian product of a family of sets (B x) xA(B_x)_{x \in A}. For all sets AA, let Δ A:AA×A\Delta_{A}:A \to A \times A denote the diagonal function; this means that the preimage of Δ A\Delta_{A} at (x,y)A×A(x, y) \in A \times A, Δ A *(x,y)\Delta_{A}^*(x, y), is a subsingleton, and (Δ A *(x,y)) xA,yA(\Delta_{A}^*(x, y))_{x \in A, y \in A} is a family of sets.

The principle of internal function extensionality is given by one of the two equivalent statements:

  • given sets AA and BB, one can derive the element of the set

    funext A,B fB A gB AΔ B A *(f,g) xAΔ B *(ev A,B(f,x),ev A,B(g,x))\mathrm{funext}_{A, B} \in \prod_{f \in B^A} \prod_{g \in B^A} \Delta_{B^A}^*(f, g)^{\prod_{x \in A} \Delta_{B}^*(\mathrm{ev}_{A, B}(f, x), \mathrm{ev}_{A, B}(g, x))}
  • given sets AA and BB, one can derive the element of the set

    funext A,B fB A gB AΔ B A *(f,g) xA 𝟙Δ B 𝟙 *(comp 𝟙,A,B(f,x),comp 𝟙,A,B(g,x))\mathrm{funext}_{A, B} \in \prod_{f \in B^A} \prod_{g \in B^A} \Delta_{B^A}^*(f, g)^{\prod_{x \in A^\mathbb{1}} \Delta_{B^\mathbb{1}}^*(\mathrm{comp}_{\mathbb{1}, A, B}(f, x), \mathrm{comp}_{\mathbb{1}, A, B}(g, x))}

This is the set theoretic analogue of the axiom of function extensionality found in dependent type theories, where functions are elements of function types, the type theoretic analogue of function sets, and equalities are represented by identity types, the type theoretic analogue of the diagonal one-to-one correspondence, and is true in any set theory with Cartesian products of arbitrary families of sets as well as function sets.

In category theory

Generalizing external function extensionality

There are multiple ways to extend the set-theoretic definition of external function extensionality from the category of sets to more general categories.

None of these notions are called “function extensionality” in category theory. The term “function extensionality” is reserved for the generalization of internal function extensionality to arbitrary categories, as documented in the next section.

Generalizing internal function extensionality

The notion of function extensionality in a category arises from the generalization of the set-theoretic definition of internal function extensionality from the category of sets to more general categories. In particular, similar to internal function extensionality, it is the logical formulation of function extensionality in the internal language of the category. The “internal” formulation can be interpreted in a category with a rich enough internal language. For instance, function extensionality can be stated in the Mitchell-Benabou language and is true in any topos. So every topos internally satisfies function extensionality despite the fact that toposes do not generally satisfy the external notion of being concrete or well-pointed. This is because the quantifier x:X\forall x:X in the internal language is interpreted as a quantification over all generalized elements IXI \to X rather than merely the global elements 1X1 \to X. Then the statement when quantifying over generalized elements is true as a consequence of the definition of an exponential object.

In dependent type theory

In intensional type theory, the notion of equality a=aa = a' is replaced by identifications, these being terms of identity type Id A(a,a)Id_A(a,a'). Since such identity type are in general not mere propositions, care needs to be exercised in stating function extensionality in intensional type theory:

For types A,B:TypeA, B \,\colon\, Type and parallel functions f,g:ABf, g \,\colon\, A \to B, there are the following two canonical functions (from identity types of function types to dependent products of pointwise identity types), which one may use for expressing function extensionality (2), both defined via path induction (see function application to identifications) as shown now:

(1)happly(f,g) : Id (AB)(f,g) a:AId B(f(a),g(a)) happly(f,f) : refl (AB)(f) λ(a:A).refl B(f(a)) happly(f,g) : Id (AB)(f,g) a:Aa:A p:Id A(a,a)Id B(f(a),g(a)) happly(f,f) : refl AB(f) λ(a:A).λ(a:A).λ(refl A(x):Id A(a,a)).refl B(f(a)) \begin{array}{ll} \mathrm{happly}(f, g) &\colon& Id_{(A \to B)} (f ,\, g) & \longrightarrow & \underset{ a \colon A } {\prod} Id_B \big( f(a) ,\, g(a) \big) \\ \mathrm{happly}(f,f) &\colon& \mathrm{refl}_{(A \to B)}(f) &\mapsto& \lambda (a \colon A). \mathrm{refl}_B \big(f(a)\big) \\ \phantom{-} \\ \mathrm{happly}(f, g) &\colon& Id_{(A \to B)}(f, g) & \longrightarrow & \underset{a \colon A}{\prod} \; \underset{a' \colon A}{\prod} \prod_{p \colon Id_A(a,a')} Id_B \big( f(a) ,\, g(a') \big) \\ \mathrm{happly}(f,f) &\colon& \mathrm{refl}_{A \to B}(f) &\mapsto& \lambda (a \colon A). \lambda (a \colon A). \lambda \big( \mathrm{refl}_A(x) \colon Id_A(a, a) \big). \mathrm{refl}_B\big(f(a)\big) \end{array}

(These two definitions of happly\mathrm{happly} become the same under singleton contractibility. The second definition behaves better with the function application to 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) (1) is an equivalence of types after all, for all functions f,g:ABf, g \,\colon\,A \to B:

(2)funext(f,g):isEquiv(happly(f,g)) \mathrm{funext}(f, g) \;\colon\; \mathrm{isEquiv} \big( \mathrm{happly}(f, g) \big)

(e.g. UFP13 (2.9.1)).

In the generality of dependent functions f,g:(d:D)C df,g \,:\, (d \colon D) \to C_d (using the notation here) this reads:

(In this dependent generality this is a special case of UFP13, Lem. 2.9.7.)

Compare this to the analogous extensionality principle for dependent pairs (see there):


Judgmental function extensionality

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

Id (AB)(f,g) x:Aid B(f(x),g(x)) Id_{(A \to B)}(f, g) \;\;\equiv\; \prod_{x:A} id_B\big( f(x) ,\, g(x) \big)

and

Id (AB)(f,g) x:A y:A p:Id A(x,y)Id B(f(x),g(y)) Id_{(A \to B)} (f ,\, g) \;\equiv\; \prod_{x:A} \prod_{y:A} \prod_{p \colon Id_A(x, y)} Id_B\big( f(x) ,\, g(y) \big)

respectively.

For judgmental equality of sections

Suppose that given functions f:ABf:A \to B and g:ABg:A \to B, for all x:Ax:A, f(x)f(x) and g(x)g(x) are judgmentally equal to each other f(x)g(x):Bf(x) \equiv g(x):B. Then it follows that ff and gg are judgmentally equal to each other, fg:ABf \equiv g:A \to B, and thus function extensionality holds. This result is crucial in the proof of function extensionality from an interval type with judgmental computation rules.

Properties

There are a number of axioms in dependent type theory which imply function extensionality. These include

 Relation to weak function extensionality

Function extensionality is equivalent to weak function extensionality – see at References – General.

Relation to the univalence axiom

In homotopy type theory, the univalence axiom implies type-theoretic function extensionality (2) – see at References – in HoTT.

Relation to interval types

Postulating an interval type with judgmental computation rules for the point constructors of the interval type implies function extensionality.

The proof assumes a typal uniqueness rule for function types. Let ap f:Id 𝕀(0,1)Id A(f(0),f(1))\mathrm{ap}_f \colon Id_{\mathbb{I}}(0, 1) \to Id_A(f(0),f(1)) be the function application to identities, concat a,b,c:Id A(a,b)×Id A(b,c)Id A(a,c)\mathrm{concat}_{a, b, c}: Id_A(a , b) \times Id_A(b , c) \to Id_A(a , c) be concatenation of identities (i.e. transitivity), and inv a,b:Id A(a,b)Id A(b,a)\mathrm{inv}_{a, b}: Id_A(a , b) \to Id_A(b , a) be the inverse of identities (i.e. symmetry).

First the proof constructs a function k:A(𝕀B)k:A \to (\mathbb{I} \to B) from a dependent function h: x:AId B(f(x),g(x))h:\prod_{x:A} Id_B\big(f(x) , g(x)\big), inductively defined by

  • β k(x) 0:Id B(k(x)(0),f(x))\beta_{k(x)}^0 : Id_B\big(k(x)(0) , f(x)\big)

  • β k(x) 1:Id B(k(x)(1),g(x))\beta_{k(x)}^1 : Id_B\big( k(x)(1) , g(x) \big)

  • β k(x) p:Id Id B(k(x)(0),k(x)(1))(ap k(x)(p),concat k(x)(0),f(x),k(x)(1)(concat k(x)(0),f(x),g(x)(β k(x) 0,h(x)),inv k(x)(1),g(x)(β k(x) 1)))\beta_{k(x)}^p : Id_{Id_B\big(k(x)(0) , k(x)(1)\big)}\big(\mathrm{ap}_{k(x)}(p) , \mathrm{concat}_{k(x)(0), f(x), k(x)(1)}(\mathrm{concat}_{k(x)(0), f(x), g(x)}(\beta_{k(x)}^0, h(x)), \mathrm{inv}_{k(x)(1), g(x)}(\beta_{k(x)}^1))\big)

Then it uses the properties of function types, product types, currying, uncurrying, and the symmetry of products A×BB×AA \times B \simeq B \times A, to construct a function k:𝕀(AB)k':\mathbb{I} \to (A \to B), inductively defined by

  • β k 0(x):Id B(k(0)(x),f(x))\beta_{k'}^0(x): Id_B\big( k'(0)(x) , f(x)\big)

  • β k 1(x):Id B(k(1)(x),g(x))\beta_{k'}^1(x): Id_B\big( k'(1)(x) , g(x) \big)

  • β k p(x):ap k(p)(x)= Id B(k(0)(x),k(1)(x))concat k(0)(x),f(x),k(1)(x)(concat k(0)(x),f(x),g(x)(β k 0(x),h(x)),inv k(1)(x),g(x)(β k 1(x)))\beta_{k'}^p(x):\mathrm{ap}_{k'}(p)(x) =_{Id_B\big( k'(0)(x) , k'(1)(x) \big)} \mathrm{concat}_{k'(0)(x), f(x), k'(1)(x)}(\mathrm{concat}_{k'(0)(x), f(x), g(x)}(\beta_{k'}^0(x), h(x)), \mathrm{inv}_{k'(1)(x), g(x)}(\beta_{k'}^1(x)))

If the interval type has judgmental computation rules for the point constructors, then k(x)(0)f(x)k'(x)(0) \equiv f(x) and k(x)(1)g(x)k'(x)(1) \equiv g(x) for all x:Ax:A, which implies that k(0)(x)f(x)k'(0)(x) \equiv f(x) and k(1)(x)g(x)k'(1)(x) \equiv g(x) for all x:Ax:A, and subsequently that k(0)fk'(0) \equiv f and k(1)gk'(1) \equiv g. This means that there are identities β k 0:k(0)= ABf\beta_{k'}^0:k'(0) =_{A \to B} f and β k 1:k(1)= ABg\beta_{k'}^1:k'(1) =_{A \to B} g, and an identity

concat f,k(1),g(concat f,k(0),k(1)(inv k(0),g(β k 0),ap k(p),β k 1):Id (AB)(f,g)\mathrm{concat}_{f, k'(1), g}(\mathrm{concat}_{f, k'(0), k'(1)}(\mathrm{inv}_{k'(0), g}(\beta_{k'}^0), \mathrm{ap}_{k'}(p), \beta_{k'}^1): Id_{(A \to B)}(f , g)

thus proving function extensionality.

An interval type with only typal computation rules for the point constructors does not imply function extensionality. This is because the proof with the judgmental computation rules uses the fact that k(0)(x)f(x)k'(0)(x) \equiv f(x) and k(1)(x)g(x)k'(1)(x) \equiv g(x) for all x:Ax:A implies that k(0)fk'(0) \equiv f and k(1)gk'(1) \equiv g. However, if the computation rules are typal, then the equivalent statement is that having identities β k 0(x):Id B(k(0)(x),f(x))\beta_{k'}^0(x): Id_B\big(k'(0)(x) , f(x)\big) and β k 1(x):Id B(k(1)(x),g(x))\beta_{k'}^1(x): Id_B\big(k'(1)(x) , g(x)\big) for all x:Ax:A implies that there are identities β k 0:Id (AB)(k(0),f)\beta_{k'}^0: Id_{(A \to B)}\big(k'(0) , f\big) and β k 1:Id AB(k(1),g)\beta_{k'}^1 : Id_{A \to B}\big(k'(1) , g\big), which is precisely function extensionality, and so cannot be used to prove function extensionality.

Relation to equality reflection

To do: write how extensional type theory automatically satisfies function extensionality.

Relation to propositional logic

To do: write how requiring all types to be mere propositions in dependent type theory, such as in propositional logic as a dependent type theory automatically satisfies function extensionality.

Categorical semantics

Under the standard relation between type theory and category theory, the categorical semantics of the type x:XId Y(f(x),g(x)) \underset{x \colon X}{\prod} Id_Y\big( f(x),\, g(x) \big) of pointwise identifications between a pair of parallel functions f,g:XYf,g \;\colon\; X \to Y is the space of sections over (hence the right base change along) XX of the pullback

where

Since the right base change is right adjoint to pullback, this means that the categorical semantics of global elements of x:XId Y(f(x),g(x))\underset{x \colon X}{\prod} Id_Y\big( f(x),\, g(x) \big), whose immediate categorical semantics is as maps out of the terminal object (to be denoted “*\ast”):

is equivalently given by maps of the form

These in turn (now by the defining universal property of the pullback) are equivalent to maps of the form

hence to lifts of (f,g)(f,g) through the path fibration display map.

In contrast, the categorical semantics of the global type of identifications Id (XY)(f,g)Id_{(X \to Y)}(f,g) is by maps of the form

where

So the categorical semantics of function extensionality (2) says in particular that there is a map

ϕ:Paths(Maps(X,Y))Maps(X,Paths(Y)) \phi \;\colon\; Paths\big(Maps(X,Y)\big) \longrightarrow Maps\big(X, Paths(Y) \big)

which serves to lift global elements as above.

Of course we are not just interested in global elements here. What we really want is an actual section Maps(X,Paths(Y))Paths(Maps(X,Y))Maps\big(X, Paths(Y)\big) \to Paths\big(Maps(X,Y)\big) of ϕ\phi in the slice over Maps(X,(Y×Y))Maps\big(X, (Y \times Y)\big) (although this can be derived from the global element formulation by using the Yoneda lemma together with currying and uncurrying tricks), such that this exhibits a weak equivalence.

Proposition

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)

Example

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.

See also

References

General

Discussion of variants of function extensionality in Martin-Löf type theory, and their relation:

Proofs of function extensionality from an interval type with judgmental computation rules:

In homotopy type theory

Discussion of function extensionality in homotopy type theory and proof that it is implied by univalence:

Original announcement in:

Textbook accounts:

Exposition:

Tutorial for formalization in Coq:

Formalization in cubical Agda:

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

On definitional function extensionality in higher observational type theory:

Last revised on March 11, 2024 at 18:17:42. See the history of this page for a list of all contributions to it.