case nil => rfl
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorOplax F G [] ≫ mapF.compositorLax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor [])
no goals