Functor id / Seq id

Stream: mathlib4

[Xavier Roblot]

In mathlib4#1353, the following code (line 264)

theorem mul_map_seq (x y : FreeMagma α) :
    ((· * ·) <$> x <*> y : id (FreeMagma α)) = (x * y : FreeMagma α) := rfl
#align free_magma.mul_map_seq FreeMagma.mul_map_seq

fails with errors failed to synthesize instance Functor id and failed to synthesize instance Seq id.
I am really not an expert in this part of mathlib, but I have the feeling this should follow from the instance Traversable FreeMagma that is proved a few lines before. In any case, it fails here and I don't know what to do to fix it.

[Sky Wilshaw]

Id is the correct spelling for the Functor instance.

[Sky Wilshaw]

If you encounter id.mk, it should be translated to something like (pure : _ \to Id _).

[Xavier Roblot]

Thanks!