C : Type u_1
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v
C : Type u_1
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ ↑(Adjunction.homEquiv adj A X) u ≫ F.map p = i ≫ ↑(Adjunction.homEquiv adj B Y) v
simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
no goals
C : Type u_1
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v
rw [F.map_comp, Adjunction.unit_naturality_assoc]