C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.unit
X Y : C
f g : X ⟶ Y
H : ↑(Adjunction.homEquiv h X (L.obj Y)) (L.map f) = ↑(Adjunction.homEquiv h X (L.obj Y)) (L.map g)
⊢ f = g
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.unit
X Y : C
f g : X ⟶ Y
H : L.map f = L.map g
⊢ f = g
rw [← (h.homEquiv X (L.obj Y)).apply_eq_iff_eq] at H
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.unit
X Y : C
f g : X ⟶ Y
H : ↑(Adjunction.homEquiv h X (L.obj Y)) (L.map f) = ↑(Adjunction.homEquiv h X (L.obj Y)) (L.map g)
⊢ f = g
simpa using H =≫ inv (h.unit.app Y)