feat(Control/Functor): port file

[j-loreaux]

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

• depends on: [Merged by Bors] - feat: port Control.Basic #588

Notes:

1. There is a discrepancy between the Lean 3 and Lean 4 types of has_seq.seq and Seq.seq. I added an ₓ for alignment.
2. There were one or two places where the existing simp or rw calls didn't succeed, but I'm not entirely sure why.
3. In Functor.Comp.functor_comp_id and Functor.Comp.functor_id_comp I had to use Id instead of id, because only the former has the Monad instance.
4. I had to change the imports, but I think what is there now is minimal.

---

Note: this is a literal duplicate of #612 created in an attempt to circumvent build failures

[semorrison]

This PR/issue depends on:

• [Merged by Bors] - feat: port Control.Basic #588
  By Dependent Issues (🤖). Happy coding!