equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
Definitions
Transfors between 2-categories
Morphisms in 2-categories
Structures in 2-categories
Limits in 2-categories
Structures on 2-categories
homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
Often, by a natural equivalence is meant specifically an equivalence in a 2-category of 2-functors.
But more generally it is an equivalence between any kind of functors in higher category theory:
In 1-category theory it is a natural isomorphism.
In (∞,1)-category theory a natural equivalence is an equivalence in an (∞,1)-category in an (∞,1)-category of (∞,1)-functors.
The components of a natural equivalence are equivalences between the objects in the codomain of the functors. This is what the term “natural equivalence” refers to: its a collection of equivalences between objects which are compatible (“natural”) with the morphisms between these objects, and higher morphisms between those.
Last revised on April 22, 2021 at 23:49:51. See the history of this page for a list of all contributions to it.