## Stream: Is there code for X?

### Topic: functor.comp as a functor

#### Adam Topaz (Mar 03 2021 at 21:04):

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 (Mar 03 2021 at 21:06):

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

#### Adam Topaz (Mar 03 2021 at 21:06):

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

Last updated: May 07 2021 at 19:12 UTC