equivalence of categories
Two categories can fail to be literally identical and yet be “the same for all practical purposes,” the way the category of finite-dimensional real vector spaces and the category of real matrices describe one situation in two languages. Equivalence of categories is the precise notion of sameness that ignores irrelevant differences — in particular it does not demand that objects match up on the nose, only up to isomorphism. It is almost always the right notion of when two mathematical theories are interchangeable.
A functor F : C -> D is an equivalence if there is a functor G : D -> C (a quasi-inverse) together with natural isomorphisms G ∘ F ≅ id_C and F ∘ G ≅ id_D. The relaxation from equality to natural isomorphism is essential: insisting on G ∘ F = id_C gives the much rarer and rigid notion of isomorphism of categories, which is too strict for real mathematics.
There is a clean recognition theorem. A functor F is an equivalence if and only if it is fully faithful and essentially surjective, that is, every object of D is isomorphic to some F(A). This criterion lets one verify equivalence without ever constructing the quasi-inverse by hand (constructing G typically requires the axiom of choice, picking one isomorphism per object). Equivalences are the morphisms in the “2-category of categories,” the level at which category theory really lives.
Stone duality gives an equivalence between the category of Boolean algebras and the opposite of the category of compact totally disconnected Hausdorff spaces. A more elementary equivalence: finite-dimensional vector spaces over a field k are equivalent to the category whose objects are natural numbers n and whose morphisms n -> m are m-by-n matrices over k.
“Same theory, two presentations” is captured exactly by an equivalence.