These are actually equal, of course, but not definitionally equal (the equality requires F.map (𝟙 _) = 𝟙 _). A natural isomorphism is more convenient than an equality between functors (compare id_to_iso).