Equality and Equivalence
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence in homotopy type theory
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
natural equivalence, natural isomorphism
principle of equivalence
fiber product, pullback
linear equation, differential equation, ordinary differential equation, critical locus
Euler-Lagrange equation, Einstein equation, wave equation
Schrödinger equation, Knizhnik-Zamolodchikov equation, Maurer-Cartan equation, quantum master equation, Euler-Arnold equation, Fuchsian equation, Fokker-Planck equation, Lax equation
A natural isomorphism between two functors and
In this case, we say that and are naturally isomorphic.
If you want to speak of ‘the’ functor satisfying certain conditions, then it should be unique up to unique natural isomorphism.
A natural isomorphism from a functor to itself is also called a natural automorphism.
Revised on January 17, 2017 12:40:58
by Toby Bartels