Lemma. The identity morphism is unique [uniqueness-identity]