Equality

Equality is the fundamental mathematical relation asserting that two expressions represent the same value or object. But “the same” is not a single concept — it sits on a spectrum from strict definitional identity to loose structural similarity, and the right notion depends on what you’re trying to preserve.

Extensional Equality

Also known as behavioural equality or operational equality.

Two expressions are extensionally equal if they produce the same results for all inputs, regardless of their internal structure or implementation. You treat them as black boxes and compare outputs.

For functions: $f{=}_{\text{ext}}g$ iff $f(x)=g(x)$ for all $x$ in the domain.

In Martin-Löf Type Theory, the extensional variant treats identity proofs as unique — if two terms behave the same, they are equal, and there is nothing more to say. This makes equality transparent but renders type-checking undecidable.

Intensional Equality

Also known as structural equality or definitional equality.

Two expressions are intensionally equal if they have the same definition or structure within a formal system — regardless of their observable behaviour. This is a stricter requirement: same syntax, same construction, same type signature.

Note: intensional derives from intension — the defining properties of a term — as distinct from intentional (relating to purpose). The terminology traces back to Frege’s distinction between sense (intension) and reference (extension).

In Martin-Löf Type Theory, the intensional variant allows identity proofs to differ — two terms can be equal in genuinely different ways, and the proof of equality itself carries computational content. This keeps type-checking decidable and opened the door to Homotopy Type Theory, where identity proofs are interpreted as paths in a topological space.

The Spectrum of Sameness

Equality is really the strictest case of a broader question: in what sense are these two things “the same”? Mathematics has a hierarchy of answers, each preserving less structure than the last:

Notion	What it preserves	Example
Intensional equality	Everything — identical definitions	$2+3$ and $2+3$
Extensional equality	Input-output behaviour	$x^2-1$ and $(x+1)(x-1)$
Isomorphism	All structure — bijective, reversible	${\mathbb{Z}}_2$ and $(\{-1,1\},\times )$
Homomorphism	Some structure — not necessarily reversible	$\exp :(\mathbb{R},+)\to ({\mathbb{R}}^{+},\times )$
Equivalence relation	Whatever the relation specifies	$7\equiv 2(\mathrm{mod}5)$

Isomorphism as Structural Equality

An isomorphism is a bijective morphism — a structure-preserving map with a structure-preserving inverse. Isomorphic objects are interchangeable for all mathematical purposes within their category. You can’t tell them apart by any structural property.

This is the working mathematician’s notion of equality. When a mathematician says two groups “are the same”, they almost always mean isomorphic, not literally identical. The univalence axiom in HoTT formalises this intuition: isomorphic types are equal.

Homomorphism as Partial Preservation

A homomorphism preserves structure in one direction but may lose information. It maps one object into another while respecting operations — $f(a\cdot b)=f(a)\cdot f(b)$ — but need not be injective or surjective.

Homomorphisms are the general arrows of algebra. They tell you that some structural relationship exists between two objects, even when those objects aren’t “the same” in any strong sense. The kernel of a homomorphism (what it collapses) measures exactly how much information is lost.

The chain: automorphism $\subset$ isomorphism $\subset$ homomorphism $\subset$ morphism — each step relaxes what’s required.

Resources

• https://en.wikipedia.org/wiki/Equality_(mathematics)
• Equivalence (Biconditional)
• Equivalence