functor.comp is a wrapper around function.comp for types. It prevents Lean's type class resolution mechanism from trying a functor (comp F id) when functor F would do.