no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
c : C
u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
f g : StructuredArrow c R
⊢ u.hom ≫ R.map (↑(Adjunction.homEquiv adj c f.right).symm f.hom) = f.hom
simp
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
c : C
u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
f g : StructuredArrow c R
⊢ u.hom ≫ R.map (↑(Adjunction.homEquiv adj c g.right).symm g.hom) = g.hom
simp