nLab equivalence

Idea

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:

• In a set (a $0$-category), equivalence is just equality.

• In a category (a $1$-category), an equivalence is an isomorphism.

• In a (possibly weak) $2$-category, an equivalence is a morphism $f : x \to y$ such that there exists a morphism $g : y\to x$ and $2$-cell isomorphisms $f g \cong 1_y$ and $g f \cong 1_x$. In the $2$-category Cat this reduces to the usual notion of equivalence of categories (although one must define $\Cat$ carefully using anafunctors if one wants to avoid the axiom of choice).

• In a (possibly weak) $3$-category, an equivalence is a morphism $f : x \to y$ such that there exists a morphism $g : y\to x$ and 2-cells $f g \to 1_y$ and $g f \to 1_x$ which are equivalences in the appropriate hom-2-categories. In the (weak) 3-category $Bicat$ of bicategories, pseudofunctors, pseudonatural transformations, and modifications, such equivalences are often called biequivalences, and that term is sometimes also used for an equivalence in any $3$-category.

• In a (possibly weak) $\infty$-category, an equivalence is a morphism $f : x \to y$ such that there exists a morphism $g : y\to x$ and 2-cells $f g \to 1_y$ and $g f \to 1_x$ which are equivalences in the appropriate hom-$\infty$-categories. This can be made rigorous as a corecursive definition.

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 $(\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 $n$-categories are equivalent if and only if they're equivalent as objects in the $(n+1)$-category of $n$-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.

Related concepts

• principle of equivalence

• identity morphism

• identity type

• identity of indiscernibles

• equality

• isomorphism, natural isomorphism

• equivalence, natural equivalence

• weak equivalence

• logical equivalence

• equivalence of groupoids, equivalence of categories

• equivalence in a 2-category

• equivalence of 2-categories, equivalence of (2,1)-categories

• homotopy equivalence, weak homotopy equivalence, Quillen equivalence

• Bousfield equivalence

• equivalence in an (∞,1)-category

• equivalence in homotopy type theory

• equivalence of (∞,1)-categories

symbol	in propositional logic	Unicode
$:$	typing relation	U+003A
=	propositional equality relation	U+003D
$\neg$	logical negation operator	U+00AC
$\neg \neg$	double negation	U+00AC&U+00AC
$\nLeftarrow$, $\nleftarrow$	negation of converse implication, or negation of converse conditional	U+21CD, U+219A
$\nLeftrightarrow$, $\nleftrightarrow$	negation of logical equivalence, or negation of biconditional	U+21CE, U+21AE
$\nRightarrow$, $\nrightarrow$	negation of implication, or negation of conditional	U+21CF, U+219B
$\Leftarrow$, $\leftarrow$	converse implication, or converse conditional	U+21D0, U+2190
$\Rightarrow$, $\rightarrow$	implication, or conditional	U+21D2, U+2192
$\Leftrightarrow$, $\leftrightarrow$	logical equivalence, or biconditional	U+21D4, U+2192
$\wedge$	logical conjunctionoperator	U+2227
$\vee$	logical dysjunction operator	U+2228
$\neq$	inequality, or apartness relation	U+2260
$\vdash$	syntactic entailment relation	U+22A2
$\vDash$	semantic entailment relation	U+22A8
$\top$	truth value, or top element	U+22A3
$\bot$	false value, or bottom element	U+22A4
$\veebar$, $\oplus$	logical exclusive dysjunction operator	U+22BB, U+2295
$\bar{\wedge}$	logical non-conjunction operator	U+22BC
$\bar{\vee}$	logical non-dysjunction operator	U+22BD

symbol	in first-order logic	Unicode
$\forall$	universal quantifier	U+2200
$\exists$	existential quantifier	U+2203
$\exists!$	uniqueness quantifier	U+2203&U+0021
$\nexists$	negation of existential quantifier	U+2204

symbol	in set theory	Unicode
×	binary Cartesian product, or binary product	U+00D7
$\varnothing$	empty, or uninhabited set	U+2205
$\in$	membership relation	U+2208
$\notin$	negation of membership relation	U+2209
$\ni$	containment relation	U+220B
$\notni$	negation of containment relation	U+220C
$\prod$	n-ary Cartesian product, or product operator	U+220F
$\coprod$	n-ary disjoint union, or coproduct operator	U+2210
$\cap$	binary intersection operator	U+2229
$\cup$	binary union operator	U+222A
$\subset$	subset of relation	U+2282
$\supset$	superset of relation	U+2283
$\nsubset$	negation of subset relation	U+2284
$\nsupset$	negation of superset relation	U+2285
$\subseteq$	inclusion relation, or subset of, or equal to	U+2286
$\supseteq$	converse of inclusion relation, or superset of, or equal to	U+2287
$\sqcup$	binary disjoint union, or binary coproduct operator	U+2294
$\bigcap$	n-ary intersection operator	U+22C2
$\bigcup$	n-ary union operator	U+22C3

$\;$

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in linear logic$\phantom{-}$
$\phantom{A}$$\top$	$\phantom{A}$additive truth
$\phantom{A}$$\bot$	$\phantom{A}$additive falsehood
$\phantom{A}$$0$	$\phantom{A}$multiplicative falsehood
$\phantom{A}$$1$	$\phantom{A}$multiplicative truth
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$
$\phantom{A}$$\;?$$\phantom{A}$	$\phantom{A}$exponential disjunction$\phantom{A}$
$\phantom{A}$$^\bot$$\phantom{A}$	$\phantom{A}$negation$\phantom{A}$

$\;$

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in dependent type theory$\phantom{-}$	$\phantom{-}$propositions as types$\phantom{-}$
$\phantom{A}$$\to$	$\phantom{A}$function type	$\phantom{A}$implication
$\phantom{A}$$\times$	$\phantom{A}$product type	$\phantom{A}$conjunction
$\phantom{A}$$+$	$\phantom{A}$sum type	$\phantom{A}$disjunction
$\phantom{A}$$0$, $\emptyset$	$\phantom{A}$empty type	$\phantom{A}$false
$\phantom{A}$$1$	$\phantom{A}$unit type	$\phantom{A}$true
$\phantom{A}$$=$, $\mathrm{Id}$	$\phantom{A}$identity type	$\phantom{A}$propositional equality
$\phantom{A}$$\simeq$	$\phantom{A}$equivalence of types	$\phantom{A}$logical equivalence
$\phantom{A}$$\sum$, $\Sigma$, $\times$	$\phantom{A}$dependent sum type	$\phantom{A}$existential quantifier
$\phantom{A}$$\prod$, $\Pi$, $\to$	$\phantom{A}$dependent product type	$\phantom{A}$universal quantifier
$\phantom{A}$$\mathrm{isContr}$	$\phantom{A}$is contractible type	$\phantom{A}$unique proof
$\phantom{A}$$\mathrm{isContr}(A + B)$	$\phantom{A}$sum type is contractible type	$\phantom{A}$exclusive disjunction
$\phantom{A}$$\mathrm{isContr}\left(\sum_{x:A} B(x)\right)$	$\phantom{A}$dependent sum type is contractible type	$\phantom{A}$uniqueness quantifier
$\phantom{A}$$\mathrm{ua}$	$\phantom{A}$univalence axiom	$\phantom{A}$propositional extensionality