functor.comp as a functor

Stream: Is there code for X?

[Adam Topaz]

Do we have the following two sorry's in mathlib somewhere?

import category_theory.equivalence

namespace category_theory

variables {B C D : Type*} [category B] [category C] [category D]

def foo (F : C ⥤ D) : (B ⥤ C) ⥤ (B ⥤ D) := sorry

def bar (F : C ≌ D) : (B ⥤ C) ≌ (B ⥤ D) := sorry

end category_theory

[Adam Topaz]

Okay, I found the second one: docs#category_theory.equivalence.congr_right

[Adam Topaz]

Ah, and the first is just docs#category_theory.whiskering_right