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

- Extensionality - objects are considered to be equal if they have the same external properties.
- Intensionality - concerned with whether the internal definitions of objects are the same.

In some type theories:

- extension is taken to be the actual thing
- intension is more elusive and described as being the meaning.

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.

see

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