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.
The identity natural transformation on a functor is the natural transformation that maps each object of to the identity morphism in .
The identity natural transformations are themselves the identity morphisms for vertical composition of natural transformations in the functor category and in the 2-category Cat.
One must be aware that when we say that a natural transformation is the identity, it doesn’t mean only that for every object but also that for every morphism ie. that the two functors and are equal.
Not taking care of this can lead to redundant definitions as for permutative categories.
Last revised on August 1, 2022 at 19:27:11. See the history of this page for a list of all contributions to it.