no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
d : D
u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
f g : CostructuredArrow L d
⊢ L.map (↑(Adjunction.homEquiv adj f.left d) f.hom) ≫ u.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
d : D
u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
f g : CostructuredArrow L d
⊢ L.map (↑(Adjunction.homEquiv adj g.left d) g.hom) ≫ u.hom = g.hom
simp