Equality and Equivalence

Category theory



In general two objects are considered equivalent if they may be replaced by one another in all contexts under consideration (see also the principle of equivalence).

At the propositional level, the general theory of equivalence is discussed at equivalence relation, but that leaves us with the question of the correct definition of equivalence in various situations. Furthermore, we can work on a higher level and ask what the equivalences are, not just whether things are equivalent.

In higher category theory

In higher category theory an equivalence often means a morphism which is invertible in a maximally weak sense (that is, up to all higher equivalences). Two objects are equivalent if there is an equivalence between them. For example:

There is also the more structured/coherent notion of an adjoint equivalence, but one hopes to have a theorem that any equivalence can be improved to an adjoint one. This is known in some cases, including 2-categories, 3-categories, strict ω\omega-categories, and some models for (,1)(\infty,1)-categories.

In addition to this, there is the notion of equivalence of categories (and higher categories), which is on a separate page. But it is related: properly done, two nn-categories are equivalent if and only if they're equivalent as objects in the (n+1)(n+1)-category of nn-categories.

In homotopy theory

In the category Top of topological spaces, notions weaker than isomorphism become very important: homotopy equivalence and weak homotopy equivalence. The latter notion is generalized to weak equivalence for objects in any model category. There is also a notion of equivalence between model categories: Quillen equivalence.

These can be understood to some extent using higher categories. For example, topological spaces should be weakly homotopy-equivalent if and only if they have equivalent fundamental infinity-groupoids. Similarly, Quillen equivalent model categories give rise to equivalent (infinity,1)-categories.

See equivalence in an (infinity,1)-category.

In homotopy type theory

In homotopy type theory equivalences can be axiomatized as those terms of function types all whose homotopy fibers are contractible.

See equivalence in homotopy type theory.

basic symbols used in logic

A\phantom{A}\inA\phantom{A}element relation
A\phantom{A}:\,:A\phantom{A}typing relation
A\phantom{A}\vdashA\phantom{A}A\phantom{A}entailment / sequentA\phantom{A}
A\phantom{A}\topA\phantom{A}A\phantom{A}true / topA\phantom{A}
A\phantom{A}\botA\phantom{A}A\phantom{A}false / bottomA\phantom{A}
A\phantom{A}\LeftrightarrowA\phantom{A}logical equivalence
A\phantom{A}\neqA\phantom{A}negation of equality / apartnessA\phantom{A}
A\phantom{A}\notinA\phantom{A}negation of element relation A\phantom{A}
A\phantom{A}¬¬\not \notA\phantom{A}negation of negationA\phantom{A}
A\phantom{A}\existsA\phantom{A}existential quantificationA\phantom{A}
A\phantom{A}\forallA\phantom{A}universal quantificationA\phantom{A}
A\phantom{A}\wedgeA\phantom{A}logical conjunction
A\phantom{A}\veeA\phantom{A}logical disjunction
A\phantom{A}\otimesA\phantom{A}A\phantom{A}multiplicative conjunctionA\phantom{A}
A\phantom{A}\oplusA\phantom{A}A\phantom{A}multiplicative disjunctionA\phantom{A}