Commit 2022-11-28 17:28 f784a3c7

feat: port control.functor (#612) mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

• depends on: #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.