Maths - Extensionality

The terminology 'extensionality' and 'extensional equality' seem to be a source of confusion:

In logic: extensionality, or extensional equality, refers to principles that judge objects to be equal if they have the same external properties. Wiki
In sets: two sets are equal if they contain the same elements.

So it seem that the term can be used for equality of either external properties or internal properties? Although perhaps we can construe all of these things as being external observations as opposed to being defined in an equal way.

Formal Systems

Often, formal systems for mathematics will include axioms designed to capture this principle.

Extensionality and Intensionality

In some type theories:

This almost seem to reverse the above definitions. So this terminology around the realm of Type theory, logic and set theory seems very hard to tie down.


extensional type theory - nCat

intensional type theory - nCat

Extension (predicate logic)

The extension of a predicate – a truth-valued function – is the set of tuples of values that, used as arguments, satisfy the predicate. Such a set of tuples is a relation. - Wiki

Set theory - Axiom of Extensionality

two sets are equal if they contain the same elements.

the axiom of extensionality, or axiom of extension, is one of the axioms of Zermelo–Fraenkel set theory. - Wiki

Function Extensionality

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

We now recall the principle of function extensionality in type theory:
Definition 2.1.5 (Function extensionality). The principle of function extensionality
That states is, that we two have functions a map:
f, g : Q
x:A B(x) are equal whenever they are pointwise equal.

Note that function extensionality is not derivable from the rules of standard Martin-Löf
type theory. However, it is derivable from the univalence axiom

metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.


Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.